pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:3be0c4c034af
+:d62b19b641c5
 priorities, this property can be violated. For this let $L$ be in the
 possession of a lock for a resource that $H$ also needs. $H$ must
 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$
+indefinitely (consider the case where threads with priority $M$
-continously need to be processed). Since $H$ is blocked by threads
+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.
 If the problem of Priority Inversion is ignored, real-time systems
 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
 software fell victim to Priority Inversion: a low priority thread
 locking a resource prevented a high priority thread from running in
 still have Priority Inversion with $H'$ (which waits for the other
 resource). The correct behaviour for $L$ is to switch to the highest
 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}'';
 and also in the
 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
 \cite{Liu00} depend on maintaining a data structure called
 \emph{inheritance log}. This log is maintained for every thread and
 broadly specified as containing ``{\it [h]istorical information on
 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
 textbook \cite{Silberschatz13} gives the wrong specification. On Page 254 the authors write: ``{\it Upon releasing the
 lock, the [low-priority] thread will revert to its original
 While \cite{Laplante11,LiYao03,Liu00,book,Sha90,Silberschatz13} are
 the only formal publications we have found that specify the
 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
 Sha et al. Unfortunately, this informal proof is too vague to be
 useful for formalising the correctness of PIP and the specification
 for PIP being correct---a fact that has not been mentioned in the
 literature and not been used in the reference implementation of PIP
 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}
 \begin{center}
 \begin{tikzpicture}[scale=1]
 \end{tabular}}
 \end{isabelle}
 \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:
 \begin{isabelle}\ \ \ \ \ %%%
 \end{tabular}
 \end{isabelle}
 \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:
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 \end{tabular}
 \end{isabelle}
 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}\ \ \ \ \ %%%
 \begin{tabular}{@ {}rcl}
 @{thm (lhs) s_holding_abv}  & @{text "\<equiv>"} & @{thm (rhs) s_holding_abv[simplified wq_def]}\\
 Because of these problems, we decided in our earlier paper
 \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
 be seen as a \textit{rough(!)} abstraction of the ``runtime
 behaviour'' of threads and also as an abstract notion of
 require that the number of created threads is less than
 a bound @{text "BC"}, that is
 \[@{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}.
 This ensures that no matter which ``future'' state is reached, the
 number of @{text "Create"}-events is finite. This bound @{text BC} is assumed
 \end{isabelle}
 \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
+some resource in state @{text s} . Our Thm.~1 implies that only
-such threads can all potentially block @{text th} after state
+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:
 \begin{quote}
 {\bf Assumptions on the threads {\boldmath{@{term "th' \<in> blockers"}}}:}
 can be bounded by the number of actions the threads in @{text
 blockers} perform (i.e.~events) and how many threads are newly
 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
 \begin{center}
 \end{isabelle}
 \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
+this is more subtle: Since @{text th} must be running, then it does
-not wait for any resource to be released, it cannot be in any
+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.
 %The second
 %however states that only threads that are \emph{not} dependants of @{text th} have their
 inductive method for protocol verification~\cite{Paulson98} is quite
 suitable for our formal model and proof. The traditional application
 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
+of PIP on top of PINTOS, a simple instructional operating system for the x86
-architecture. It also gives the first author enough data to enable
+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
 lemma. We were also able to establish the property that the choice of
 the next thread which takes over a lock is irrelevant for the correctness
 (the informal specification by Sha et al.~did not).
 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
 for future work.
 To us, it seems sound reasoning about scheduling algorithms is fiendishly difficult
 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
+PVS of the Priority Ceiling Protocol done by Dutertre~\cite{dutertre99b}---another solution to the Priority Inversion
-\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
 checking techniques. The results obtained by them apply,
 however, only to systems with a fixed size, such as a fixed number of

changeset 207	d62b19b641c5
parent 206	3be0c4c034af
child 208	a5afc26b1d62