--- a/prio/Paper/Paper.thy	Tue Feb 14 00:11:17 2012 +0000
+++ b/prio/Paper/Paper.thy	Tue Feb 14 00:27:47 2012 +0000
@@ -601,22 +601,23 @@
   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 \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
-  critical resource (the high-priority thread is waiting for), then the
+  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 indefinite, or unbounded, Priority Inversion,
+  because if one low-priority thread does not give up its critical
+  resource (the one 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
+  of time, then indefinite 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, 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.
+  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 indefinite Priority Inversion for one of the
+  high-priority threads, invalidating their bound.
 
   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
@@ -688,11 +689,18 @@
   \end{theorem}
 
   \noindent
-  This theorem ensures that the thread @{text th}, which has the highest 
-  precedence in the state @{text s}, can only be blocked in the state @{text "s' @ s"} 
-  by a thread @{text th'} that already existed in @{text s}. As we shall see shortly,
-  that means by only finitely many threads. Consequently, indefinite wait of
-  @{text th}---which would be Priority Inversion---cannot occur.
+  This theorem ensures that the thread @{text th}, which has the
+  highest precedence in the state @{text s}, can only be blocked in
+  the state @{text "s' @ s"} by a thread @{text th'} that already
+  existed in @{text s}. As we shall see shortly, that means by only
+  finitely many threads. Like in the argument by Sha et al.~this
+  finite bound does not guarantee absence of indefinite Priority
+  Inversion. For this we further have to assume that every thread
+  gives up its resources after a finite amount of time. We found that
+  this assumption is awkward to formalise in our model. Therefore we
+  leave it out and let the programmer assume the responsibility to
+  program threads in such a benign manner. In this detail, we do not
+  make any progress in comparison with the work by Sha et al.
 
   In what follows we will describe properties of PIP that allow us to prove 
   Theorem~\ref{mainthm}. It is relatively easily to see that

Binary file prio/paper.pdf has changed