diff -r c37b387110d0 -r eee031cc9634 prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Mon Feb 13 23:50:37 2012 +0000
+++ b/prio/Paper/Paper.thy	Tue Feb 14 00:11:17 2012 +0000
@@ -601,34 +601,39 @@
   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
+  can only be blocked @{text m} times---that is a \emph{bounded} number of
+  times. This result on its own, 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
+  critical 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.
+  taking this assumption into account, ther correctness property is \emph{not}
+  true for their version of PIP. As Yodaiken
+  \cite{Yodaiken02} pointed out: If a low-priority thread possesses locks to two
+  resources for which two high-priority threads are waiting for, then
+  lowering the priority prematurely after giving up only one lock, can
+  cause Priority Inversion for one of the high-priority threads, invalidating
+  their bound.
 
-  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;
-  we show that in every future state (denoted by @{text "s' @ s"}) in which
-  @{text th} is still alive, either @{text th} is running or it is blocked by a 
-  thread that was alive in the state @{text s}. Since in @{text s}, as in every 
-  state, the set of alive threads is finite, @{text th} can only be blocked a
-  finite number of times. We will actually prove a stricter bound below. However,
-  this correctness criterion hinges upon a number of assumptions about the states
-  @{text s} and @{text "s' @ s"}, the thread @{text th} and the events happening
-  in @{text s'}. We list them next:
+  Even when fixed, their proof idea does not seem to go through for
+  us, because of the way we have set up our formal model of PIP.  The
+  reason is that we allow that critical sections can intersect
+  (something Sha et al.~explicitly exclude).  Therefore we have a 
+  different correctness criterion for PIP. The idea behind our
+  criterion is as follows: for all states @{text
+  s}, we know the corresponding thread @{text th} with the highest
+  precedence; we show that in every future state (denoted by @{text
+  "s' @ s"}) in which @{text th} is still alive, either @{text th} is
+  running or it is blocked by a thread that was alive in the state
+  @{text s}. Since in @{text s}, as in every state, the set of alive
+  threads is finite, @{text th} can only be blocked a finite number of
+  times. We will actually prove a stricter bound below. However, this
+  correctness criterion hinges upon a number of assumptions about the
+  states @{text s} and @{text "s' @ s"}, the thread @{text th} and the
+  events happening in @{text s'}. We list them next:
 
   \begin{quote}
   {\bf Assumptions on the states @{text s} and @{text "s' @ s"}:} In order to make