--- a/prio/Paper/Paper.thy	Mon Jan 30 08:55:27 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Jan 30 09:33:39 2012 +0000
@@ -24,12 +24,12 @@
   indefinitely by processes with lower priorities. For this let $L$ be
   in the possession of a lock for a resource that also $H$ needs. $H$
   must therefore wait for $L$ to release this lock. The problem is
-  that $L$ might be in turn blocked by any process with priority $M$,
+  that $L$ might in turn be blocked by any process with priority $M$,
   and so $H$ sits there potentially waiting indefinitely. Since $H$ is
   blocked by processes with lower priorities, the problem is called
   Priority Inversion. It was first described in
   \cite{Lampson:Redell:cacm:1980} in the context of the Mesa
-  programming language designed to support concurrent programming.
+  programming language designed for concurrent programming.
 
   If the problem of Priority Inversion is ignored, realtime systems
   can become unpredictable and resulting bugs can be hard to diagnose.
@@ -38,18 +38,18 @@
   \cite{Reeves-Glenn-1998}.  Once the spacecraft landed, the software
   shut down at irregular intervals leading to loss of project time, as
   normal operation of the craft could only resume the next day (the
-  mission and data already collected was fortunately not lost, because
+  mission and data already collected were fortunately not lost, because
   of a clever system design).  The reason for the shutdowns was that
   the schedulling software fell victim of Priority Inversion: a low
   priority task locking a resource prevented a high priority process
-  from running leading to a system reset. Once the problem was found,
+  from running in time leading to a system reset. Once the problem was found,
   it was rectified by enabling the Priority Inheritance Protocol in
   the schedulling software.
 
   The idea behind the \emph{Priority Inheritance Protocol} (PIP) is to
   let the process $L$ temporarily inherit the high priority from $H$ 
   until $L$ releases the locked resource. This solves the problem of
-  $H$ having to wait indefinitely, because $L$ cannot be blocked by 
+  $H$ having to wait indefinitely, because $L$ cannot, for example, be blocked by 
   processes having priority $M$. This solution to the Priority
   Inversion problem has been known since \cite{Lampson:Redell:cacm:1980}
   but Lui et al give the first thourough analysis and present a correctness

Binary file prio/paper.pdf has changed