--- a/prio/Paper/Paper.thy	Thu May 03 00:43:57 2012 +0000
+++ b/prio/Paper/Paper.thy	Thu May 03 08:52:03 2012 +0000
@@ -1235,13 +1235,13 @@
   \end{center}
 
   \noindent
-  Our assumption that every event is an atomic operation is ensured by the architecture of 
+  Our implicit assumption that every event is an atomic operation is ensured by the architecture of 
   PINTOS. The case where an unlocked resource is given next to the waiting thread with the
   highest precedence is realised in our implementation by priority queues. We implemented
   them as \emph{Braun trees} \cite{Paulson96}, which provide efficient @{text "O(log n)"}-operations
-  for accessing and restructuring. Apart from having to implement complex datastructures in C
+  for accessing and updating. Apart from having to implement relatively complex data\-structures in C
   using pointers, our experience with the implementation has been very positive: our specification 
-  and formalisation of PIP translates smoothly to an efficent implementation. 
+  and formalisation of PIP translates smoothly to an efficent implementation in PINTOS. 
 *}
 
 section {* Conclusion *}
@@ -1272,10 +1272,11 @@
   programmer who wants to implement PIP (similarly Sha et al.~\cite{Sha90}).  
   That this is an issue in practice is illustrated by the
   email from Baker we cited in the Introduction. We achieved also this
-  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 simple instructional operating system for the x86 
-  architecture \cite{PINTOS}. A byproduct of our formalisation effort is that nearly all
+  goal: The formalisation allowed us to efficently implement our version
+  of PIP on top of PINTOS \cite{PINTOS}, a simple instructional operating system for the x86 
+  architecture. It also gives the first author enough data to enable
+  his undergraduate students to implement PIP (as part of their OS course).
+  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 establish the property that the choice of
   the next thread which takes over a lock is irrelevant for the correctness

Binary file prio/paper.pdf has changed