--- a/prio/Paper/Paper.thy	Mon Feb 13 21:34:19 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 13 22:03:36 2012 +0000
@@ -1130,14 +1130,14 @@
   The Priority Inheritance Protocol (PIP) is a classic textbook
   algorithm used in real-time operating systems in order to avoid the problem of
   Priority Inversion.  Although classic and widely used, PIP does have
-  its faults: for example it does not prevent deadlocks where threads
+  its faults: for example it does not prevent deadlocks in cases where threads
   have circular lock dependencies.
 
-  We had two aims in mind with our formalisation of PIP: One is to
+  We had two goals in mind with our formalisation of PIP: One is to
   make the notions in the correctness proof by Sha et al.~\cite{Sha90}
-  precise so that they can be processed by a theorem prover, because a
-  mechanically checked proof avoids the flaws that crept into their
-  informal reasoning. We achieved this aim: The correctness of PIP now
+  precise so that they can be processed by a theorem prover. The reason is
+  that a mechanically checked proof avoids the flaws that crept into their
+  informal reasoning. We achieved this goal: The correctness of PIP now
   only hinges on the assumptions behind our formal model. The reasoning, which is
   sometimes quite intricate and tedious, has been checked beyond any
   reasonable doubt by Isabelle/HOL. We can also confirm that Paulson's
@@ -1147,22 +1147,23 @@
   application of Paulson's method we know of outside this area is
   \cite{Wang09}.
 
-  The second aim is to provide a specification for actually
-  implementing PIP. Textbooks, like \cite[Section 5.6.5]{Vahalia96},
+  The second goal of our formalisation is to provide a specification for actually
+  implementing PIP. Textbooks, for example \cite[Section 5.6.5]{Vahalia96},
   explain how to use various implementations of PIP and abstractly
-  discuss its properties, but surprisingly lack most details for a
-  programmer.  That this is an issue in practice is illustrated by the
+  discuss their properties, but surprisingly lack most details for a
+  programmer who wants to implement PIP.  That this is an issue in practice is illustrated by the
   email from Baker we cited in the Introduction. We achieved also this
-  aim: The formalisation gives the first author enough data to enable
-  his undergraduate students to implement as part of their OS course
-  PIP on top of PINTOS, a small operating system for teaching
+  goal: The formalisation gives the first author enough data to enable
+  his undergraduate students to implement PIP (as part of their OS course)
+  on top of PINTOS, a small operating system for teaching
   purposes. A byproduct of our formalisation effort is that nearly all
   design choices for the PIP scheduler are backed up with a proved
-  lemma. We were also able to prove the property that the choice of
-  the next thread taking over a lock is irrelevant for the correctness
-  of PIP. Earlier model checking approaches to verifying the
-  correctness of PIP \cite{Faria08,Jahier09,Wellings07} were not able
-  to provide this kind of ``deep understanding'' about PIP.
+  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
+  of PIP. Earlier model checking approaches which verified implementations
+  of PIP \cite{Faria08,Jahier09,Wellings07} cannot
+  provide this kind of ``deep understanding'' about the principles behind 
+  PIP and its correctness.
 
   PIP is a scheduling algorithm for single-processor systems. We are
   now living in a multi-processor world. So the question naturally

Binary file prio/paper.pdf has changed