--- a/prio/Paper/Paper.thy	Mon Feb 13 22:03:36 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 13 22:17:26 2012 +0000
@@ -1167,24 +1167,29 @@
 
   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 nowadays beyond
-  teaching. Priority inversion certainly occurs also in
-  multi-processor systems.  The surprising answer, according to
+  arises whether PIP has any relevance in such a world beyond
+  teaching. Priority Inversion certainly occurs also in
+  multi-processor systems.  However, the surprising answer, according to
   \cite{Steinberg10}, is that except for one unsatisfactory proposal
-  nobody seems to have any good idea how PIP shoud be modified to work
-  correctly on multi-processor systems. The obstacles become clear
+  nobody has a good idea for how PIP should be modified to work
+  correctly on multi-processor systems. The difficulties become clear
   when considering that locking and releasing a resource always
-  requires some small time span. If processes are independent, then a
-  low priority process can always ``steal'' a the lock for such a
-  resource from a high-priority process that should have run next. In
-  effect, we have again the problem of Priority Inversions. It seems 
-  difficult to design an algorithm with a meaningful property from
-  PIP.  We can imagine PIP can be of use in a situation where
-  processes are not independent, but coordinated such that a master
-  process distributes the work over some slave processes. However a
+  requires a some small amount of time. If processes work independently, then a
+  low priority process can ``steal'' in this unguarded moment a lock for a
+  resource that was supposed allow a high-priority process to run next. Thus
+  the problem of Priority Inversion is not really prevented. It seems 
+  difficult to design a PIP-algorithm with a meaningful correctness 
+  property on independent multi-processor systems.  We can imagine PIP 
+  to be of use in a situation where
+  processes are not independent, but coordinated via a master
+  process that distributes work over some slave processes. However a
   formal investigation of this is beyond the scope of this paper.
-
+  We are not aware of any proofs in this area, not even informal ones.
  
+  Our formalisation consists of X lines of readable Isabelle/Isar code, with some
+  apply-scripts interspersed. The formal model is Y lines long; the 
+  formal correctness proof Z lines. The properties relevant for an
+  implementation are U lines long.
 
 *}