--- 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' \<in> treads (s' @ s)"}, @{text "th' \<noteq> th"} and @{text "detached (s' @ s) th'"}\\
+ if @{term "th' \<in> threads (s' @ s)"}, @{text "th' \<noteq> th"} and @{text "detached (s' @ s) th'"}\\
then @{text "th' \<notin> 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}