
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' \<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}




