539 @{thm[mode=Rule] thread_exit[where thread=th]} |
539 @{thm[mode=Rule] thread_exit[where thread=th]} |
540 \end{tabular} |
540 \end{tabular} |
541 \end{center} |
541 \end{center} |
542 |
542 |
543 \noindent |
543 \noindent |
544 The first rule states that a thread can only be created, if it does not yet exists. |
544 The first rule states that a thread can only be created, if it is not alive yet. |
545 Similarly, the second rule states that a thread can only be terminated if it was |
545 Similarly, the second rule states that a thread can only be terminated if it was |
546 running and does not lock any resources anymore (this simplifies slightly our model; |
546 running and does not lock any resources anymore (this simplifies slightly our model; |
547 in practice we would expect the operating system releases all locks held by a |
547 in practice we would expect the operating system releases all locks held by a |
548 thread that is about to exit). The event @{text Set} can happen |
548 thread that is about to exit). The event @{text Set} can happen |
549 if the corresponding thread is running. |
549 if the corresponding thread is running. |
557 running and also we have to make sure that the resource lock does |
557 running and also we have to make sure that the resource lock does |
558 not lead to a cycle in the RAG. In practice, ensuring the latter is |
558 not lead to a cycle in the RAG. In practice, ensuring the latter is |
559 the responsibility of the programmer. In our formal |
559 the responsibility of the programmer. In our formal |
560 model we brush aside these problematic cases in order to be able to make |
560 model we brush aside these problematic cases in order to be able to make |
561 some meaningful statements about PIP.\footnote{This situation is |
561 some meaningful statements about PIP.\footnote{This situation is |
562 similar to the infamous occurs check in Prolog: In order to say |
562 similar to the infamous \emph{occurs check} in Prolog: In order to say |
563 anything meaningful about unification, one needs to perform an occurs |
563 anything meaningful about unification, one needs to perform an occurs |
564 check. But in practice the occurs check is omitted and the |
564 check. But in practice the occurs check is omitted and the |
565 responsibility for avoiding problems rests with the programmer.} |
565 responsibility for avoiding problems rests with the programmer.} |
566 |
566 |
567 \begin{center} |
567 \begin{center} |
600 (*>*) |
600 (*>*) |
601 text {* |
601 text {* |
602 Sha et al.~state their first correctness criterion for PIP in terms |
602 Sha et al.~state their first correctness criterion for PIP in terms |
603 of the number of low-priority threads \cite[Theorem 3]{Sha90}: if |
603 of the number of low-priority threads \cite[Theorem 3]{Sha90}: if |
604 there are @{text n} low-priority threads, then a blocked job with |
604 there are @{text n} low-priority threads, then a blocked job with |
605 high priority can only be blocked @{text n} times. |
605 high priority can only be blocked a maximum of @{text n} times. |
606 Their second correctness criterion is given |
606 Their second correctness criterion is given |
607 in terms of the number of critical resources \cite[Theorem 6]{Sha90}: if there are |
607 in terms of the number of critical resources \cite[Theorem 6]{Sha90}: if there are |
608 @{text m} critical resources, then a blocked job with high priority |
608 @{text m} critical resources, then a blocked job with high priority |
609 can only be blocked @{text m} times. Both results on their own, strictly speaking, do |
609 can only be blocked a maximum of @{text m} times. Both results on their own, strictly speaking, do |
610 \emph{not} prevent indefinite, or unbounded, Priority Inversion, |
610 \emph{not} prevent indefinite, or unbounded, Priority Inversion, |
611 because if a low-priority thread does not give up its critical |
611 because if a low-priority thread does not give up its critical |
612 resource (the one the high-priority thread is waiting for), then the |
612 resource (the one the high-priority thread is waiting for), then the |
613 high-priority thread can never run. The argument of Sha et al.~is |
613 high-priority thread can never run. The argument of Sha et al.~is |
614 that \emph{if} threads release locked resources in a finite amount |
614 that \emph{if} threads release locked resources in a finite amount |
625 high-priority threads, invalidating their two bounds. |
625 high-priority threads, invalidating their two bounds. |
626 |
626 |
627 Even when fixed, their proof idea does not seem to go through for |
627 Even when fixed, their proof idea does not seem to go through for |
628 us, because of the way we have set up our formal model of PIP. One |
628 us, because of the way we have set up our formal model of PIP. One |
629 reason is that we allow that critical sections can intersect |
629 reason is that we allow that critical sections can intersect |
630 (something Sha et al.~explicitly exclude). Therefore we have designed a |
630 (something Sha et al.~explicitly exclude). Therefore we have |
631 different correctness criterion for PIP. The idea behind our |
631 designed a different correctness criterion for PIP. The idea behind |
632 criterion is as follows: for all states @{text |
632 our criterion is as follows: for all states @{text s}, we know the |
633 s}, we know the corresponding thread @{text th} with the highest |
633 corresponding thread @{text th} with the highest precedence; we show |
634 precedence; we show that in every future state (denoted by @{text |
634 that in every future state (denoted by @{text "s' @ s"}) in which |
635 "s' @ s"}) in which @{text th} is still alive, either @{text th} is |
635 @{text th} is still alive, either @{text th} is running or it is |
636 running or it is blocked by a thread that was alive in the state |
636 blocked by a thread that was alive in the state @{text s} and was in |
637 @{text s} and was in the possession of a lock in @{text s}. Since in @{text s}, as in every state, the set of alive |
637 the possession of a lock in @{text s}. Since in @{text s}, as in |
638 threads is finite, @{text th} can only be blocked a finite number of |
638 every state, the set of alive threads is finite, @{text th} can only |
639 times. We will actually prove a stronger statement where we also provide |
639 be blocked a finite number of times. This is independent of how many |
640 the current precedence of the blocking thread. However, this |
640 threads of lower priority are created in @{text "s'"}. We will actually prove a |
641 correctness criterion hinges upon a number of assumptions about the |
641 stronger statement where we also provide the current precedence of |
642 states @{text s} and @{text "s' @ s"}, the thread @{text th} and the |
642 the blocking thread. However, this correctness criterion hinges upon |
643 events happening in @{text s'}. We list them next: |
643 a number of assumptions about the states @{text s} and @{text "s' @ |
|
644 s"}, the thread @{text th} and the events happening in @{text |
|
645 s'}. We list them next: |
644 |
646 |
645 \begin{quote} |
647 \begin{quote} |
646 {\bf Assumptions on the states @{text s} and @{text "s' @ s"}:} In order to make |
648 {\bf Assumptions on the states {\boldmath@{text s}} and |
|
649 {\boldmath@{text "s' @ s"}:}} In order to make |
647 any meaningful statement, we need to require that @{text "s"} and |
650 any meaningful statement, we need to require that @{text "s"} and |
648 @{text "s' @ s"} are valid states, namely |
651 @{text "s' @ s"} are valid states, namely |
649 \begin{isabelle}\ \ \ \ \ %%% |
652 \begin{isabelle}\ \ \ \ \ %%% |
650 \begin{tabular}{l} |
653 \begin{tabular}{l} |
651 @{term "vt s"}\\ |
654 @{term "vt s"}\\ |
666 \end{tabular} |
670 \end{tabular} |
667 \end{isabelle} |
671 \end{isabelle} |
668 \end{quote} |
672 \end{quote} |
669 |
673 |
670 \begin{quote} |
674 \begin{quote} |
671 {\bf Assumptions on the events in @{text "s'"}:} We want to prove that @{text th} cannot |
675 {\bf Assumptions on the events in {\boldmath@{text "s'"}:}} We want to prove that @{text th} cannot |
672 be blocked indefinitely. Of course this can happen if threads with higher priority |
676 be blocked indefinitely. Of course this can happen if threads with higher priority |
673 than @{text th} are continuously created in @{text s'}. Therefore we have to assume that |
677 than @{text th} are continuously created in @{text s'}. Therefore we have to assume that |
674 events in @{text s'} can only create (respectively set) threads with equal or lower |
678 events in @{text s'} can only create (respectively set) threads with equal or lower |
675 priority than @{text prio} of @{text th}. We also need to assume that the |
679 priority than @{text prio} of @{text th}. We also need to assume that the |
676 priority of @{text "th"} does not get reset and also that @{text th} does |
680 priority of @{text "th"} does not get reset and also that @{text th} does |
684 \end{isabelle} |
688 \end{isabelle} |
685 \end{quote} |
689 \end{quote} |
686 |
690 |
687 \noindent |
691 \noindent |
688 The locale mechanism of Isabelle helps us to manage conveniently such assumptions~\cite{Haftmann08}. |
692 The locale mechanism of Isabelle helps us to manage conveniently such assumptions~\cite{Haftmann08}. |
689 Under these assumptions we will prove the following correctness property: |
693 Under these assumptions we shall prove the following correctness property: |
690 |
694 |
691 \begin{theorem}\label{mainthm} |
695 \begin{theorem}\label{mainthm} |
692 Given the assumptions about states @{text "s"} and @{text "s' @ s"}, |
696 Given the assumptions about states @{text "s"} and @{text "s' @ s"}, |
693 the thread @{text th} and the events in @{text "s'"}, |
697 the thread @{text th} and the events in @{text "s'"}, |
694 if @{term "th' \<in> running (s' @ s)"} and @{text "th' \<noteq> th"} then |
698 if @{term "th' \<in> running (s' @ s)"} and @{text "th' \<noteq> th"} then |
806 blocked by a thread @{text th'} that |
810 blocked by a thread @{text th'} that |
807 held some resource in state @{text s} (that is not @{text "detached"}). And furthermore |
811 held some resource in state @{text s} (that is not @{text "detached"}). And furthermore |
808 that the current precedence of @{text th'} in state @{text "(s' @ s)"} must be equal to the |
812 that the current precedence of @{text th'} in state @{text "(s' @ s)"} must be equal to the |
809 precedence of @{text th} in @{text "s"}. |
813 precedence of @{text th} in @{text "s"}. |
810 We show this theorem by induction on @{text "s'"} using Lemma~\ref{mainlem}. |
814 We show this theorem by induction on @{text "s'"} using Lemma~\ref{mainlem}. |
811 This theorem gives a stricter bound on the processes that can block @{text th} than the |
815 This theorem gives a stricter bound on the threads that can block @{text th} than the |
812 one obtained by Sha et al.~\cite{Sha90}: |
816 one obtained by Sha et al.~\cite{Sha90}: |
813 only threads that were alive in state @{text s} and moreover held a resource. |
817 only threads that were alive in state @{text s} and moreover held a resource. |
814 This means our bound is in terms of both---alive threads in state @{text s} |
818 This means our bound is in terms of both---alive threads in state @{text s} |
815 and number of critical resources. Finally, the theorem establishes that the blocking threads have the |
819 and number of critical resources. Finally, the theorem establishes that the blocking threads have the |
816 current precedence raised to the precedence of @{text th}. |
820 current precedence raised to the precedence of @{text th}. |
1227 teaching. Priority Inversion certainly occurs also in |
1231 teaching. Priority Inversion certainly occurs also in |
1228 multi-processor systems. However, the surprising answer, according |
1232 multi-processor systems. However, the surprising answer, according |
1229 to \cite{Steinberg10}, is that except for one unsatisfactory |
1233 to \cite{Steinberg10}, is that except for one unsatisfactory |
1230 proposal nobody has a good idea for how PIP should be modified to |
1234 proposal nobody has a good idea for how PIP should be modified to |
1231 work correctly on multi-processor systems. The difficulties become |
1235 work correctly on multi-processor systems. The difficulties become |
1232 clear when considering the fact that locking and releasing a resource always |
1236 clear when considering the fact that releasing and re-locking a resource always |
1233 requires a small amount of time. If processes work independently, |
1237 requires a small amount of time. If processes work independently, |
1234 then a low priority process can ``steal'' in such an unguarded |
1238 then a low priority process can ``steal'' in such an unguarded |
1235 moment a lock for a resource that was supposed to allow a high-priority |
1239 moment a lock for a resource that was supposed to allow a high-priority |
1236 process to run next. Thus the problem of Priority Inversion is not |
1240 process to run next. Thus the problem of Priority Inversion is not |
1237 really prevented by the classic PIP. It seems difficult to design a PIP-algorithm with |
1241 really prevented by the classic PIP. It seems difficult to design a PIP-algorithm with |