401 |
401 |
402 \noindent |
402 \noindent |
403 We also use the abbreviation |
403 We also use the abbreviation |
404 |
404 |
405 \begin{isabelle}\ \ \ \ \ %%% |
405 \begin{isabelle}\ \ \ \ \ %%% |
406 @{thm preceds_def} |
406 ???%%@ { thm preceds_def} |
407 \end{isabelle} |
407 \end{isabelle} |
408 |
408 |
409 \noindent |
409 \noindent |
410 for the set of precedences of threads @{text ths} in state @{text s}. |
410 for the set of precedences of threads @{text ths} in state @{text s}. |
411 The point of precedences is to schedule threads not according to priorities (because what should |
411 The point of precedences is to schedule threads not according to priorities (because what should |
1067 responsibility to program threads in such a benign manner (in |
1067 responsibility to program threads in such a benign manner (in |
1068 addition to causing no circularity in the RAG). In this detail, we |
1068 addition to causing no circularity in the RAG). In this detail, we |
1069 do not make any progress in comparison with the work by Sha et al. |
1069 do not make any progress in comparison with the work by Sha et al. |
1070 However, we are able to combine their two separate bounds into a |
1070 However, we are able to combine their two separate bounds into a |
1071 single theorem improving their bound. |
1071 single theorem improving their bound. |
|
1072 |
|
1073 @{text "th_kept"} shows that th is a thread in s'-s |
|
1074 |
|
1075 \begin{proof}[of Theorem 1] |
|
1076 If @{term "th \<in> running (s' @ s)"}, then there is nothing to show. So let us |
|
1077 assume otherwise. |
|
1078 \end{proof} |
1072 |
1079 |
1073 In what follows we will describe properties of PIP that allow us to |
1080 In what follows we will describe properties of PIP that allow us to |
1074 prove Theorem~\ref{mainthm} and, when instructive, briefly describe |
1081 prove Theorem~\ref{mainthm} and, when instructive, briefly describe |
1075 our argument. Recall we want to prove that in state @{term "s' @ s"} |
1082 our argument. Recall we want to prove that in state @{term "s' @ s"} |
1076 either @{term th} is either running or blocked by a thread @{term |
1083 either @{term th} is either running or blocked by a thread @{term |