665 of @{text th} in the state @{text s}. Since the notion @{term |
665 of @{text th} in the state @{text s}. Since the notion @{term |
666 "dependants"} is defined as the transitive closure of all dependent |
666 "dependants"} is defined as the transitive closure of all dependent |
667 threads, we deal correctly with the problem in the informal |
667 threads, we deal correctly with the problem in the informal |
668 algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is |
668 algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is |
669 lowered prematurely (see Introduction). We again introduce an abbreviation for current |
669 lowered prematurely (see Introduction). We again introduce an abbreviation for current |
670 precedeces of a set of threads, written @{term "cprecs wq s ths"}. |
670 precedeces of a set of threads, written @{text "cpreceds wq s ths"}. |
671 |
671 |
672 \begin{isabelle}\ \ \ \ \ %%% |
672 \begin{isabelle}\ \ \ \ \ %%% |
673 @{thm cpreceds_def} |
673 @{thm cpreceds_def} |
674 \end{isabelle} |
674 \end{isabelle} |
675 |
675 |
1010 @{text "s' @ s"}) in which @{text th} is still alive, either @{text |
1010 @{text "s' @ s"}) in which @{text th} is still alive, either @{text |
1011 th} is running or it is blocked by a thread that was alive in the |
1011 th} is running or it is blocked by a thread that was alive in the |
1012 state @{text s} and was waiting for or in the possession of a lock |
1012 state @{text s} and was waiting for or in the possession of a lock |
1013 in @{text s}. Since in @{text s}, as in every state, the set of |
1013 in @{text s}. Since in @{text s}, as in every state, the set of |
1014 alive threads is finite, @{text th} can only be blocked a finite |
1014 alive threads is finite, @{text th} can only be blocked a finite |
1015 number of threads. This is independent of how many threads of lower |
1015 number of threads. We will actually prove a |
1016 priority are created in @{text "s'"}. We will actually prove a |
|
1017 stronger statement where we also provide the current precedence of |
1016 stronger statement where we also provide the current precedence of |
1018 the blocking thread. |
1017 the blocking thread. |
1019 |
1018 |
1020 However, this correctness criterion hinges upon a number of |
1019 However, this correctness criterion hinges upon a number of |
1021 natural assumptions about the states @{text s} and @{text "s' @ s"}, the |
1020 natural assumptions about the states @{text s} and @{text "s' @ s"}, the |