# HG changeset patch # User Christian Urban # Date 1530911919 -3600 # Node ID d62b19b641c53637416bf7814a4015e1074ba0da # Parent 3be0c4c034af5200f99b86ac13400118af1304d6 updated diff -r 3be0c4c034af -r d62b19b641c5 Journal/Paper.thy --- a/Journal/Paper.thy Fri Feb 23 21:10:49 2018 +0000 +++ b/Journal/Paper.thy Fri Jul 06 22:18:39 2018 +0100 @@ -84,8 +84,8 @@ therefore wait for $L$ to exit the critical section and release this lock. The problem is that $L$ might in turn be blocked by any thread with priority $M$, and so $H$ sits there potentially waiting - indefinitely (consider the case where threads with propority $M$ - continously need to be processed). Since $H$ is blocked by threads + indefinitely (consider the case where threads with priority $M$ + continuously need to be processed). Since $H$ is blocked by threads with lower priorities, the problem is called Priority Inversion. It was first described in \cite{Lampson80} in the context of the Mesa programming language designed for concurrent programming. @@ -94,9 +94,9 @@ can become unpredictable and resulting bugs can be hard to diagnose. The classic example where this happened is the software that controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}. On - Earth the software run mostly without any problem, but once the + Earth, the software ran mostly without any problem, but once the spacecraft landed on Mars, it shut down at irregular, but frequent, - intervals leading to loss of project time as normal operation of the + intervals. This led to loss of project time as normal operation of the craft could only resume the next day (the mission and data already collected were fortunately not lost, because of a clever system design). The reason for the shutdowns was that the scheduling @@ -190,7 +190,7 @@ remaining priority of the threads that it blocks. A similar error is made in the textbook \cite[Section 2.3.1]{book} which specifies for a process that inherited a higher priority and exits a critical - section ``{\it it resumes the priority it had at the point of entry + section that ``{\it it resumes the priority it had at the point of entry into the critical section}''. This error can also be found in the textbook \cite[Section 16.4.1]{LiYao03} where the authors write about this process: ``{\it its priority is immediately lowered to the level originally assigned}''; @@ -198,7 +198,7 @@ more recent textbook \cite[Page 119]{Laplante11} where the authors state: ``{\it when [the task] exits the critical section that caused the block, it reverts to the priority it had when it entered that - section}''. The textbook \cite[Page 286]{Liu00} contains a simlar + section}''. The textbook \cite[Page 286]{Liu00} contains a similar flawed specification and even goes on to develop pseudo-code based on this flawed specification. Accordingly, the operating system primitives for inheritance and restoration of priorities in @@ -208,7 +208,7 @@ how the thread inherited its current priority}'' \cite[Page 527]{Liu00}. Unfortunately, the important information about actually computing the priority to be restored solely from this log is not - explained in \cite{Liu00} but left as an ``{\it excercise}'' to the + explained in \cite{Liu00} but left as an ``{\it exercise}'' to the reader. As we shall see, a correct version of PIP does not need to maintain this (potentially expensive) log data structure at all. Surprisingly also the widely read and frequently updated @@ -222,7 +222,7 @@ incorrect behaviour, it seems also many informal descriptions of the PIP protocol overlook the possibility that another high-priority process might wait for a low-priority process to finish. A notable - exception is the texbook \cite{buttazzo}, which gives the correct + exception is the textbook \cite{buttazzo}, which gives the correct behaviour of resetting the priority of a thread to the highest remaining priority of the threads it blocks. This textbook also gives an informal proof for the correctness of PIP in the style of @@ -249,11 +249,11 @@ in PINTOS. This fact, however, is important for an efficient implementation of PIP, because we can give the lock to the thread with the highest priority so that it terminates more quickly. We - are also being able to generalise the scheduler of Sha et + are also able to generalise the scheduler of Sha et al.~\cite{Sha90} to the practically relevant case where critical sections can overlap; see Figure~\ref{overlap} \emph{a)} below for an example of this restriction. In the existing literature there is - no proof and also no proving method that cover this generalised + no proof and also no method for proving which covers this generalised case. \begin{figure} @@ -332,7 +332,8 @@ \noindent whereby threads, priorities and (critical) resources are represented - as natural numbers. The event @{term Set} models the situation that + as natural numbers. In what follows we shall use @{term cs} as a name for + critical resources. The event @{term Set} models the situation that a thread obtains a new priority given by the programmer or user (for example via the {\tt nice} utility under UNIX). For states we define the following type-synonym: @@ -787,7 +788,7 @@ \noindent where @{text "SOME"} stands for Hilbert's epsilon and implements an arbitrary choice for the next waiting list. It just - has to be a list of distinctive threads and contains the same + has to be a list of distinct threads and contains the same elements as @{text "qs"} (essentially @{text "qs'"} can be any reordering of the list @{text "qs"}). This gives for @{term V} the clause: @@ -802,7 +803,7 @@ Having the scheduler function @{term schs} at our disposal, we can ``lift'', or overload, the notions @{term waiting}, @{term holding}, - @{term RAG}, %%@ {term dependants} + @{term RAG}, @{term "TDG"}, %%@ {term dependants} and @{term cp} to operate on states only. \begin{isabelle}\ \ \ \ \ %%% @@ -1627,7 +1628,7 @@ \cite{ZhangUrbanWu12} to leave out this property and let the programmer take on the responsibility to program threads in such a benign manner (in addition to causing no circularity in the - RAG). This leave-it-to-the-programmer was also the approach taken by + RAG). This leave-it-to-the-programmer approach was also taken by Sha et al.~in their paper. However, in this paper we can make an improvement by establishing a finite bound on the duration of Priority Inversion measured by the number of events. The events can @@ -1662,10 +1663,10 @@ \[@{text "len (filter isCreate es) < BC"}\;\] - wherby @{text es} is a list of events. + whereby @{text es} is a list of events. \end{quote} - \noindent Note that it is not enough to just to state that there are + \noindent Note that it is not enough to just state that there are only finite number of threads created up until a single state @{text "s' @ s"} after @{text s}. Instead, we need to put this bound on the @{text "Create"} events for all valid states after @{text s}. @@ -1685,8 +1686,8 @@ \noindent This set contains all threads that are not detached in state @{text s}. According to our definiton of @{text "detached"}, this means a thread in @{text "blockers"} either holds or waits for - some resource in state @{text s} . Our Thm.~1 implies that any of - such threads can all potentially block @{text th} after state + some resource in state @{text s} . Our Thm.~1 implies that only + these threads can all potentially block @{text th} after state @{text s}. We need to make the following assumption about the threads in the @{text "blockers"}-set: @@ -1716,7 +1717,7 @@ created. To state our bound formally, we need to make a definition of what we mean by intermediate states between a state @{text s} and a future state after @{text s}; they will be the list of states - starting from @{text s} upto the state \mbox{@{text "es @ s"}}. For + starting from @{text s} up to the state \mbox{@{text "es @ s"}}. For example, suppose $\textit{es} = [\textit{e}_n, \textit{e}_{n-1}, \ldots, \textit{e}_2, \textit{e}_1]$, then the intermediate states from @{text s} upto @{text "es @ s"} are @@ -1952,8 +1953,8 @@ \noindent The first property is again telling us we do not need to change the @{text RAG}. The second shows that the @{term cp}-values of all threads other than @{text th} are unchanged. The reason for - this is more subtle: Since @{text th} must be running, that is does - not wait for any resource to be released, it cannot be in any + this is more subtle: Since @{text th} must be running, then it does + not wait for any resource to be released and it cannot be in any subtree of any other thread. So all current precedences of other threads are unchanged. @@ -2309,15 +2310,15 @@ area of this method is security protocols. The second goal of our formalisation is to provide a specification for actually - implementing PIP. Textbooks, for example \cite[Section 5.6.5]{Vahalia96}, + implementing PIP. Textbooks, for example Vahalia \cite[Section 5.6.5]{Vahalia96}, explain how to use various implementations of PIP and abstractly discuss their properties, but surprisingly lack most details important for a programmer who wants to implement PIP (similarly Sha et al.~\cite{Sha90}). That this is an issue in practice is illustrated by the email from Baker we cited in the Introduction. We achieved also this goal: The formalisation allowed us to efficently implement our version - of PIP on top of PINTOS \cite{PINTOS}, a simple instructional operating system for the x86 - architecture. It also gives the first author enough data to enable + of PIP on top of PINTOS, a simple instructional operating system for the x86 + architecture implemented by Pfaff \cite{PINTOS}. It also gives the first author enough data to enable his undergraduate students to implement PIP (as part of their OS course). A byproduct of our formalisation effort is that nearly all design choices for the implementation of PIP scheduler are backed up with a proved @@ -2337,13 +2338,13 @@ PIP is a scheduling algorithm for single-processor systems. We are now living in a multi-processor world. Priority Inversion certainly - occurs also there, see for example \cite{Brandenburg11,Davis11}. + occurs also there, see for example work by Brandenburg, and Davis and Burns \cite{Brandenburg11,Davis11}. However, there is very little ``foundational'' work about PIP-algorithms on multi-processor systems. We are not aware of any correctness proofs, not even informal ones. There is an implementation of a PIP-algorithm for multi-processors as part of the ``real-time'' effort in Linux, including an informal description of the implemented scheduling - algorithm given in \cite{LINUX}. We estimate that the formal + algorithm given by Rostedt in \cite{LINUX}. We estimate that the formal verification of this algorithm, involving more fine-grained events, is a magnitude harder than the one we presented here, but still within reach of current theorem proving technology. We leave this @@ -2353,12 +2354,11 @@ if done informally by ``pencil-and-paper''. We infer this from the flawed proof in the paper by Sha et al.~\cite{Sha90} and also from \cite{Regehr} where Regehr points out an error in a paper about Preemption - Threshold Scheduling \cite{ThreadX}. The use of a theorem prover was + Threshold Scheduling by Wang and Saksena \cite{ThreadX}. The use of a theorem prover was invaluable to us in order to be confident about the correctness of our reasoning (for example no corner case can be overlooked). The most closely related work to ours is the formal verification in - PVS of the Priority Ceiling Protocol done by Dutertre - \cite{dutertre99b}---another solution to the Priority Inversion + PVS of the Priority Ceiling Protocol done by Dutertre~\cite{dutertre99b}---another solution to the Priority Inversion problem, which however needs static analysis of programs in order to avoid it. There have been earlier formal investigations into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model diff -r 3be0c4c034af -r d62b19b641c5 journal.pdf Binary file journal.pdf has changed