--- a/prio/Paper/Paper.thy	Wed May 02 13:13:47 2012 +0000
+++ b/prio/Paper/Paper.thy	Thu May 03 00:43:57 2012 +0000
@@ -1282,18 +1282,17 @@
   of PIP. 
 
   PIP is a scheduling algorithm for single-processor systems. We are
-  now living in a multi-processor world. So the question naturally
-  arises whether PIP has any relevance in such a world beyond
-  teaching. Priority Inversion certainly occurs also in
-  multi-processor systems.  However, the answer is that
-  there is very little work about PIP and multi-processors in the literature. 
-  We are not aware of any proofs in this area, not even informal ones. There
-  is an implementation of PIP on multi-processors in Linux as part of the ``real-time'' effort,
-  with an informal description given in \cite{LINUX}.
-  We estimate that the formal verification of this algorithm, involving more
-  fine-grained events, is a magnitude harder than the one we presented here, but 
-  still within reach of current theorem proving technology. We leave this for future 
-  work. 
+  now living in a multi-processor world. Priority Inversion certainly
+  occurs also there.  However, there is very little ``foundational''
+  work about PIP-algorithms on multi-processor systems.  We are not
+  aware of any correctness proofs, not even informal ones. There is an
+  implementation of a PIP-algorithm for multi-processors as part of the
+  ``real-time'' effort in Linux, including an informal description of the implemented scheduling
+  algorithm given in \cite{LINUX}.  We estimate that the formal
+  verification of this algorithm, involving more fine-grained events,
+  is a magnitude harder than the one we presented here, but still
+  within reach of current theorem proving technology. We leave this
+  for future work.
 
   The most closely related work to ours is the formal verification in
   PVS of the Priority Ceiling Protocol done by Dutertre