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 \emph{bounded} number of |
604 can only be blocked @{text m} times---that is a \emph{bounded} |
605 times. This result on its own, strictly speaking, does \emph{not} prevent Priority |
605 number of times. This result on its own, strictly speaking, does |
606 Inversion, because if one low-priority thread does not give up its |
606 \emph{not} prevent indefinite, or unbounded, Priority Inversion, |
607 critical resource (the high-priority thread is waiting for), then the |
607 because if one low-priority thread does not give up its critical |
|
608 resource (the one the high-priority thread is waiting for), then the |
608 high-priority thread can never run. The argument of Sha et al.~is |
609 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 |
610 that \emph{if} threads release locked resources in a finite amount |
610 of time, then Priority Inversion cannot occur---the high-priority |
611 of time, then indefinite Priority Inversion cannot occur---the high-priority |
611 thread is guaranteed to run eventually. The assumption is that |
612 thread is guaranteed to run eventually. The assumption is that |
612 programmers always ensure that this is the case. However, even |
613 programmers always ensure that this is the case. However, even |
613 taking this assumption into account, ther correctness property is \emph{not} |
614 taking this assumption into account, ther correctness property is |
614 true for their version of PIP. As Yodaiken |
615 \emph{not} true for their version of PIP. As Yodaiken |
615 \cite{Yodaiken02} pointed out: If a low-priority thread possesses locks to two |
616 \cite{Yodaiken02} pointed out: If a low-priority thread possesses |
616 resources for which two high-priority threads are waiting for, then |
617 locks to two resources for which two high-priority threads are |
617 lowering the priority prematurely after giving up only one lock, can |
618 waiting for, then lowering the priority prematurely after giving up |
618 cause Priority Inversion for one of the high-priority threads, invalidating |
619 only one lock, can cause indefinite Priority Inversion for one of the |
619 their bound. |
620 high-priority threads, invalidating their bound. |
620 |
621 |
621 Even when fixed, their proof idea does not seem to go through for |
622 Even when fixed, their proof idea does not seem to go through for |
622 us, because of the way we have set up our formal model of PIP. The |
623 us, because of the way we have set up our formal model of PIP. The |
623 reason is that we allow that critical sections can intersect |
624 reason is that we allow that critical sections can intersect |
624 (something Sha et al.~explicitly exclude). Therefore we have a |
625 (something Sha et al.~explicitly exclude). Therefore we have a |
686 if @{term "th' \<in> running (s' @ s)"} and @{text "th' \<noteq> th"} then |
687 if @{term "th' \<in> running (s' @ s)"} and @{text "th' \<noteq> th"} then |
687 @{text "th' \<in> threads s"}. |
688 @{text "th' \<in> threads s"}. |
688 \end{theorem} |
689 \end{theorem} |
689 |
690 |
690 \noindent |
691 \noindent |
691 This theorem ensures that the thread @{text th}, which has the highest |
692 This theorem ensures that the thread @{text th}, which has the |
692 precedence in the state @{text s}, can only be blocked in the state @{text "s' @ s"} |
693 highest precedence in the state @{text s}, can only be blocked in |
693 by a thread @{text th'} that already existed in @{text s}. As we shall see shortly, |
694 the state @{text "s' @ s"} by a thread @{text th'} that already |
694 that means by only finitely many threads. Consequently, indefinite wait of |
695 existed in @{text s}. As we shall see shortly, that means by only |
695 @{text th}---which would be Priority Inversion---cannot occur. |
696 finitely many threads. Like in the argument by Sha et al.~this |
|
697 finite bound does not guarantee absence of indefinite Priority |
|
698 Inversion. For this we further have to assume that every thread |
|
699 gives up its resources after a finite amount of time. We found that |
|
700 this assumption is awkward to formalise in our model. Therefore we |
|
701 leave it out and let the programmer assume the responsibility to |
|
702 program threads in such a benign manner. In this detail, we do not |
|
703 make any progress in comparison with the work by Sha et al. |
696 |
704 |
697 In what follows we will describe properties of PIP that allow us to prove |
705 In what follows we will describe properties of PIP that allow us to prove |
698 Theorem~\ref{mainthm}. It is relatively easily to see that |
706 Theorem~\ref{mainthm}. It is relatively easily to see that |
699 |
707 |
700 \begin{isabelle}\ \ \ \ \ %%% |
708 \begin{isabelle}\ \ \ \ \ %%% |