diff -r e7504bfdbd50 -r b3add51e2e0f prio/Paper/Paper.thy --- a/prio/Paper/Paper.thy Fri Apr 13 13:12:43 2012 +0000 +++ b/prio/Paper/Paper.thy Sun Apr 15 21:53:12 2012 +0000 @@ -55,10 +55,10 @@ $H$(igh), $M$(edium) and $L$(ow). We would expect that the thread $H$ blocks any other thread with lower priority and itself cannot be blocked by any thread with lower priority. Alas, in a naive - implementation of resource looking and priorities this property can + implementation of resource locking and priorities this property can be violated. Even worse, $H$ can be delayed indefinitely by threads with lower priorities. For this let $L$ be in the - possession of a lock for a resource that also $H$ needs. $H$ must + 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 @@ -76,9 +76,9 @@ 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 of Priority Inversion: a low priority thread + software fell victim to Priority Inversion: a low priority thread locking a resource prevented a high priority thread from running in - time leading to a system reset. Once the problem was found, it was + time, leading to a system reset. Once the problem was found, it was rectified by enabling the \emph{Priority Inheritance Protocol} (PIP) \cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority Inheritance Protocol} \cite{Sha90} and others sometimes also call it @@ -114,7 +114,7 @@ \end{quote} \noindent - He suggests to avoid PIP altogether by not allowing critical + He suggests avoiding PIP altogether by not allowing critical sections to be preempted. Unfortunately, this solution does not help in real-time systems with hard deadlines for high-priority threads. @@ -136,10 +136,10 @@ \end{quote} \noindent - The criticism by Yodaiken, Baker and others suggests to us to look - again at PIP from a more abstract level (but still concrete enough - to inform an implementation), and makes PIP an ideal candidate for a - formal verification. One reason, of course, is that the original + The criticism by Yodaiken, Baker and others suggests another look + at PIP from a more abstract level (but still concrete enough + to inform an implementation), and makes PIP a good candidate for a + formal verification. An additional reason is that the original presentation of PIP~\cite{Sha90}, despite being informally ``proved'' correct, is actually \emph{flawed}. @@ -155,7 +155,7 @@ $H'$ each wait for one of them. If $L$ releases one resource so that $H$, say, can proceed, then we still have Priority Inversion with $H'$ (which waits for the other resource). The correct - behaviour for $L$ is to revert to the highest remaining priority of + behaviour for $L$ is to switch to the highest remaining priority of the threads that it blocks. The advantage of formalising the correctness of a high-level specification of PIP in a theorem prover is that such issues clearly show up and cannot be overlooked as in @@ -173,8 +173,8 @@ to prove stronger properties that, as we will show, can inform an efficient implementation. For example, we found by ``playing'' with the formalisation that the choice of the next thread to take over a lock when a - resource is released is irrelevant for PIP being correct. Something - which has not been mentioned in the relevant literature. + resource is released is irrelevant for PIP being correct---a fact + that has not been mentioned in the relevant literature. *} section {* Formal Model of the Priority Inheritance Protocol *} @@ -512,7 +512,7 @@ \noindent With these abbreviations in place we can introduce - the notion of threads being @{term readys} in a state (i.e.~threads + the notion of a thread being @{term ready} in a state (i.e.~threads that do not wait for any resource) and the running thread. \begin{isabelle}\ \ \ \ \ %%% @@ -538,7 +538,7 @@ Finally we can define what a \emph{valid state} is in our model of PIP. For example we cannot expect to be able to exit a thread, if it was not - created yet. This would cause havoc in any scheduler. + created yet. These validity constraints on states are characterised by the inductive predicate @{term "step"} and @{term vt}. We first give five inference rules for @{term step} relating a state and an event that can happen next. @@ -627,7 +627,7 @@ programmers must ensure that threads are programmed in this way. However, even taking this assumption into account, the correctness properties of Sha et al.~are - \emph{not} true for their version of PIP---despide being ``proved''. As Yodaiken + \emph{not} true for their version of PIP---despite being ``proved''. As Yodaiken \cite{Yodaiken02} pointed out: If a low-priority thread possesses locks to two resources for which two high-priority threads are waiting for, then lowering the priority prematurely after giving up @@ -734,7 +734,7 @@ In what follows we will describe properties of PIP that allow us to prove Theorem~\ref{mainthm} and, when instructive, briefly describe our argument. - It is relatively easily to see that + It is relatively easy to see that \begin{isabelle}\ \ \ \ \ %%% \begin{tabular}{@ {}l} @@ -776,7 +776,7 @@ \end{isabelle} \noindent - The acyclicity property follow from how we restricted the events in + The acyclicity property follows from how we restricted the events in @{text step}; similarly the finiteness and well-foundedness property. The last two properties establish that every thread in a @{text "RAG"} (either holding or waiting for a resource) is a live thread. @@ -786,7 +786,7 @@ \begin{lemma}\label{mainlem} Given the assumptions about states @{text "s"} and @{text "s' @ s"}, the thread @{text th} and the events in @{text "s'"}, - if @{term "th' \ treads (s' @ s)"}, @{text "th' \ th"} and @{text "detached (s' @ s) th'"}\\ + if @{term "th' \ threads (s' @ s)"}, @{text "th' \ th"} and @{text "detached (s' @ s) th'"}\\ then @{text "th' \ running (s' @ s)"}. \end{lemma} @@ -978,7 +978,7 @@ \end{isabelle} \noindent - where a child is a thread that is only one ``hop'' away from the tread + where a child is a thread that is only one ``hop'' away from the thread @{text th} in the @{term RAG} (and waiting for @{text th} to release a resource). We can prove the following lemma. @@ -1190,7 +1190,7 @@ As can be seen, a pleasing byproduct of our formalisation is that the properties in this section closely inform an implementation of PIP, namely whether the @{text RAG} needs to be reconfigured or current precedences need to - by recalculated for an event. This information is provided by the lemmas we proved. + be recalculated for an event. This information is provided by the lemmas we proved. *} section {* Conclusion *} @@ -1269,7 +1269,7 @@ definitions and proofs span over 770 lines of code. The properties relevant for an implementation require 2000 lines. The code of our formalisation can be downloaded from - \url{http://www.dcs.kcl.ac.uk/staff/urbanc/pip.html}. + \url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}. \bibliographystyle{plain} \bibliography{root}