557 the responsibility of the programmer. In our formal |
557 the responsibility of the programmer. In our formal |
558 model we brush aside these problematic cases in order to be able to make |
558 model we brush aside these problematic cases in order to be able to make |
559 some meaningful statements about PIP.\footnote{This situation is |
559 some meaningful statements about PIP.\footnote{This situation is |
560 similar to the infamous occurs check in Prolog: In order to say |
560 similar to the infamous occurs check in Prolog: In order to say |
561 anything meaningful about unification, one needs to perform an occurs |
561 anything meaningful about unification, one needs to perform an occurs |
562 check. But in practice the occurs check is ommited and the |
562 check. But in practice the occurs check is omitted and the |
563 responsibility for avoiding problems rests with the programmer.} |
563 responsibility for avoiding problems rests with the programmer.} |
564 |
564 |
565 \begin{center} |
565 \begin{center} |
566 @{thm[mode=Rule] thread_P[where thread=th]} |
566 @{thm[mode=Rule] thread_P[where thread=th]} |
567 \end{center} |
567 \end{center} |
631 precedence; we show that in every future state (denoted by @{text |
631 precedence; we show that in every future state (denoted by @{text |
632 "s' @ s"}) in which @{text th} is still alive, either @{text th} is |
632 "s' @ s"}) in which @{text th} is still alive, either @{text th} is |
633 running or it is blocked by a thread that was alive in the state |
633 running or it is blocked by a thread that was alive in the state |
634 @{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 |
634 @{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 |
635 threads is finite, @{text th} can only be blocked a finite number of |
635 threads is finite, @{text th} can only be blocked a finite number of |
636 times. We will actually prove astronger statement where we also provide |
636 times. We will actually prove a stronger statement where we also provide |
637 the current precedence of the blocking thread. However, this |
637 the current precedence of the blocking thread. However, this |
638 correctness criterion hinges upon a number of assumptions about the |
638 correctness criterion hinges upon a number of assumptions about the |
639 states @{text s} and @{text "s' @ s"}, the thread @{text th} and the |
639 states @{text s} and @{text "s' @ s"}, the thread @{text th} and the |
640 events happening in @{text s'}. We list them next: |
640 events happening in @{text s'}. We list them next: |
641 |
641 |
665 \end{quote} |
665 \end{quote} |
666 |
666 |
667 \begin{quote} |
667 \begin{quote} |
668 {\bf Assumptions on the events in @{text "s'"}:} We want to prove that @{text th} cannot |
668 {\bf Assumptions on the events in @{text "s'"}:} We want to prove that @{text th} cannot |
669 be blocked indefinitely. Of course this can happen if threads with higher priority |
669 be blocked indefinitely. Of course this can happen if threads with higher priority |
670 than @{text th} are continously created in @{text s'}. Therefore we have to assume that |
670 than @{text th} are continuously created in @{text s'}. Therefore we have to assume that |
671 events in @{text s'} can only create (respectively set) threads with equal or lower |
671 events in @{text s'} can only create (respectively set) threads with equal or lower |
672 priority than @{text prio} of @{text th}. We also need to assume that the |
672 priority than @{text prio} of @{text th}. We also need to assume that the |
673 priority of @{text "th"} does not get reset and also that @{text th} does |
673 priority of @{text "th"} does not get reset and also that @{text th} does |
674 not get ``exited'' in @{text "s'"}. This can be ensured by assuming the following three implications. |
674 not get ``exited'' in @{text "s'"}. This can be ensured by assuming the following three implications. |
675 \begin{isabelle}\ \ \ \ \ %%% |
675 \begin{isabelle}\ \ \ \ \ %%% |
703 with the same current precedence as @{text th}. |
703 with the same current precedence as @{text th}. |
704 |
704 |
705 Like in the argument by Sha et al.~our |
705 Like in the argument by Sha et al.~our |
706 finite bound does not guarantee absence of indefinite Priority |
706 finite bound does not guarantee absence of indefinite Priority |
707 Inversion. For this we further have to assume that every thread |
707 Inversion. For this we further have to assume that every thread |
708 gives up its resources after a finite amount of time. We found that |
708 gives up its resources (that means get detached) after a finite amount of time. We found that |
709 this assumption is awkward to formalise in our model. Therefore we |
709 this assumption is awkward to formalise in our model. Therefore we |
710 leave it out and let the programmer assume the responsibility to |
710 leave it out and let the programmer assume the responsibility to |
711 program threads in such a benign manner (in addition to causeing no |
711 program threads in such a benign manner (in addition to causing no |
712 circularity in the @{text RAG}). In this detail, we do not |
712 circularity in the @{text RAG}). In this detail, we do not |
713 make any progress in comparison with the work by Sha et al. |
713 make any progress in comparison with the work by Sha et al. |
714 However, we are able to combine their two separate bounds into a |
714 However, we are able to combine their two separate bounds into a |
715 single theorem. |
715 single theorem. |
716 |
716 |
1107 @{thm[mode=IfThen] cp_kept} |
1107 @{thm[mode=IfThen] cp_kept} |
1108 \end{isabelle} |
1108 \end{isabelle} |
1109 |
1109 |
1110 \noindent |
1110 \noindent |
1111 For @{text th} and @{text th'} we need to use Lemma~\ref{childrenlem} to |
1111 For @{text th} and @{text th'} we need to use Lemma~\ref{childrenlem} to |
1112 recalculate their current prcedence since their children have changed. *}(*<*)end context step_v_cps_nnt begin (*>*)text {* |
1112 recalculate their current precedence since their children have changed. *}(*<*)end context step_v_cps_nnt begin (*>*)text {* |
1113 \noindent |
1113 \noindent |
1114 In the other case where there is no thread that takes over @{text cs}, we can show how |
1114 In the other case where there is no thread that takes over @{text cs}, we can show how |
1115 to recalculate the @{text RAG} and also show that no current precedence needs |
1115 to recalculate the @{text RAG} and also show that no current precedence needs |
1116 to be recalculated. |
1116 to be recalculated. |
1117 |
1117 |
1144 |
1144 |
1145 \noindent |
1145 \noindent |
1146 This means we do not need to add a holding edge to the @{text RAG} and no |
1146 This means we do not need to add a holding edge to the @{text RAG} and no |
1147 current precedence needs to be recalculated.*}(*<*)end context step_P_cps_ne begin(*>*) text {* |
1147 current precedence needs to be recalculated.*}(*<*)end context step_P_cps_ne begin(*>*) text {* |
1148 \noindent |
1148 \noindent |
1149 In the second case we know that resouce @{text cs} is locked. We can show that |
1149 In the second case we know that resource @{text cs} is locked. We can show that |
1150 |
1150 |
1151 \begin{isabelle}\ \ \ \ \ %%% |
1151 \begin{isabelle}\ \ \ \ \ %%% |
1152 \begin{tabular}{@ {}l} |
1152 \begin{tabular}{@ {}l} |
1153 @{thm depend_s}\\ |
1153 @{thm depend_s}\\ |
1154 @{thm[mode=IfThen] eq_cp} |
1154 @{thm[mode=IfThen] eq_cp} |