599 (*>*) |
599 (*>*) |
600 text {* |
600 text {* |
601 Sha et al.~\cite[Theorem 6]{Sha90} state their correctness criterion |
601 Sha et al.~\cite[Theorem 6]{Sha90} state their correctness criterion |
602 for PIP in terms of the number of critical resources: if there are |
602 for PIP in terms of the number of critical resources: if there are |
603 @{text m} critical resources, then a blocked job with high priority |
603 @{text m} critical resources, then a blocked job with high priority |
604 can only be blocked @{text m} times---that is a bounded number of |
604 can only be blocked @{text m} times---that is a \emph{bounded} number of |
605 times. This, strictly speaking, does \emph{not} prevent Priority |
605 times. This result on its own, strictly speaking, does \emph{not} prevent Priority |
606 Inversion, because if one low-priority thread does not give up its |
606 Inversion, because if one low-priority thread does not give up its |
607 resource the high-priority thread is waiting for, then the |
607 critical resource (the high-priority thread is waiting for), then the |
608 high-priority thread can never run. The argument of Sha et al.~is |
608 high-priority thread can never run. The argument of Sha et al.~is |
609 that \emph{if} threads release locked resources in a finite amount |
609 that \emph{if} threads release locked resources in a finite amount |
610 of time, then Priority Inversion cannot occur---the high-priority |
610 of time, then Priority Inversion cannot occur---the high-priority |
611 thread is guaranteed to run eventually. The assumption is that |
611 thread is guaranteed to run eventually. The assumption is that |
612 programmers always ensure that this is the case. However, even |
612 programmers always ensure that this is the case. However, even |
613 taking this assumption into account, this |
613 taking this assumption into account, ther correctness property is \emph{not} |
614 property is \emph{not} true for their version of PIP (as pointed out by Yodaiken |
614 true for their version of PIP. As Yodaiken |
615 \cite{Yodaiken02}): A high-priority thread can be blocked an |
615 \cite{Yodaiken02} pointed out: If a low-priority thread possesses locks to two |
616 unbounded number of times by creating medium-priority threads that |
616 resources for which two high-priority threads are waiting for, then |
617 block a thread, which in turn locks a critical resource and has too |
617 lowering the priority prematurely after giving up only one lock, can |
618 low priority to make progress. In the way we have set up our formal |
618 cause Priority Inversion for one of the high-priority threads, invalidating |
619 model of PIP, their proof idea, even when fixed, does not seem to go |
619 their bound. |
620 through. |
620 |
621 |
621 Even when fixed, their proof idea does not seem to go through for |
622 The idea behind our correctness criterion of PIP is as follows: for all states |
622 us, because of the way we have set up our formal model of PIP. The |
623 @{text s}, we know the corresponding thread @{text th} with the highest precedence; |
623 reason is that we allow that critical sections can intersect |
624 we show that in every future state (denoted by @{text "s' @ s"}) in which |
624 (something Sha et al.~explicitly exclude). Therefore we have a |
625 @{text th} is still alive, either @{text th} is running or it is blocked by a |
625 different correctness criterion for PIP. The idea behind our |
626 thread that was alive in the state @{text s}. Since in @{text s}, as in every |
626 criterion is as follows: for all states @{text |
627 state, the set of alive threads is finite, @{text th} can only be blocked a |
627 s}, we know the corresponding thread @{text th} with the highest |
628 finite number of times. We will actually prove a stricter bound below. However, |
628 precedence; we show that in every future state (denoted by @{text |
629 this correctness criterion hinges upon a number of assumptions about the states |
629 "s' @ s"}) in which @{text th} is still alive, either @{text th} is |
630 @{text s} and @{text "s' @ s"}, the thread @{text th} and the events happening |
630 running or it is blocked by a thread that was alive in the state |
631 in @{text s'}. We list them next: |
631 @{text s}. Since in @{text s}, as in every state, the set of alive |
|
632 threads is finite, @{text th} can only be blocked a finite number of |
|
633 times. We will actually prove a stricter bound below. However, this |
|
634 correctness criterion hinges upon a number of assumptions about the |
|
635 states @{text s} and @{text "s' @ s"}, the thread @{text th} and the |
|
636 events happening in @{text s'}. We list them next: |
632 |
637 |
633 \begin{quote} |
638 \begin{quote} |
634 {\bf Assumptions on the states @{text s} and @{text "s' @ s"}:} In order to make |
639 {\bf Assumptions on the states @{text s} and @{text "s' @ s"}:} In order to make |
635 any meaningful statement, we need to require that @{text "s"} and |
640 any meaningful statement, we need to require that @{text "s"} and |
636 @{text "s' @ s"} are valid states, namely |
641 @{text "s' @ s"} are valid states, namely |