--- a/prio/Paper/Paper.thy	Mon Feb 13 23:31:40 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 13 23:50:37 2012 +0000
@@ -598,16 +598,26 @@
 thm highest_gen_def
 (*>*)
 text {* 
-  Sha et al.~\cite[Theorem 6]{Sha90} state their correctness criterion for PIP in terms
-  of the number of critical resources: if there are @{text m} critical
-  resources, then a blocked job can only be blocked @{text m} times---that is
-  a bounded number of times.
-  For their version of PIP, this property is \emph{not} true (as pointed out by 
-  Yodaiken \cite{Yodaiken02}) as a high-priority thread can be
-  blocked an unbounded number of times by creating medium-priority
-  threads that block a thread, which in turn locks a critical resource and has
-  too low priority to make progress. In the way we have set up our formal model of PIP, 
-  their proof idea, even when fixed, does not seem to go through.
+  Sha et al.~\cite[Theorem 6]{Sha90} state their correctness criterion
+  for PIP in terms of the number of critical resources: if there are
+  @{text m} critical resources, then a blocked job with high priority
+  can only be blocked @{text m} times---that is a bounded number of
+  times. This, strictly speaking, does \emph{not} prevent Priority
+  Inversion, because if one low-priority thread does not give up its
+  resource the high-priority thread is waiting for, then the
+  high-priority thread can never run.  The argument of Sha et al.~is
+  that \emph{if} threads release locked resources in a finite amount
+  of time, then Priority Inversion cannot occur---the high-priority
+  thread is guaranteed to run eventually. The assumption is that
+  programmers always ensure that this is the case.  However, even
+  taking this assumption into account, this
+  property is \emph{not} true for their version of PIP (as pointed out by Yodaiken
+  \cite{Yodaiken02}): A high-priority thread can be blocked an
+  unbounded number of times by creating medium-priority threads that
+  block a thread, which in turn locks a critical resource and has too
+  low priority to make progress. In the way we have set up our formal
+  model of PIP, their proof idea, even when fixed, does not seem to go
+  through.
 
   The idea behind our correctness criterion of PIP is as follows: for all states
   @{text s}, we know the corresponding thread @{text th} with the highest precedence;