601   Sha et al.~\cite[Theorem 6]{Sha90} state their correctness criterion for PIP in terms

   601   Sha et al.~\cite[Theorem 6]{Sha90} state their correctness criterion

   602   of the number of critical resources: if there are @{text m} critical

   602   for PIP in terms of the number of critical resources: if there are

   603   resources, then a blocked job can only be blocked @{text m} times---that is

   603   @{text m} critical resources, then a blocked job with high priority

   604   a bounded number of times.

   604   can only be blocked @{text m} times---that is a bounded number of

   605   For their version of PIP, this property is \emph{not} true (as pointed out by 

   605   times. This, strictly speaking, does \emph{not} prevent Priority

   606   Yodaiken \cite{Yodaiken02}) as a high-priority thread can be

   606   Inversion, because if one low-priority thread does not give up its

   607   blocked an unbounded number of times by creating medium-priority

   607   resource the high-priority thread is waiting for, then the

   608   threads that block a thread, which in turn locks a critical resource and has

   608   high-priority thread can never run.  The argument of Sha et al.~is

   609   too low priority to make progress. In the way we have set up our formal model of PIP, 

   609   that \emph{if} threads release locked resources in a finite amount

   610   their proof idea, even when fixed, does not seem to go through.

   610   of time, then Priority Inversion cannot occur---the high-priority

   611   thread is guaranteed to run eventually. The assumption is that

   612   programmers always ensure that this is the case.  However, even

   613   taking this assumption into account, this

   614   property is \emph{not} true for their version of PIP (as pointed out by Yodaiken

   615   \cite{Yodaiken02}): A high-priority thread can be blocked an

   616   unbounded number of times by creating medium-priority threads that

   617   block a thread, which in turn locks a critical resource and has too

   618   low priority to make progress. In the way we have set up our formal

   619   model of PIP, their proof idea, even when fixed, does not seem to go

   620   through.