1091 the thread was not \emph{detached} in @{text s}. As we shall see |
1091 the thread was not \emph{detached} in @{text s}. As we shall see |
1092 shortly, that means there are only finitely many threads that can |
1092 shortly, that means there are only finitely many threads that can |
1093 block @{text th} in this way. |
1093 block @{text th} in this way. |
1094 |
1094 |
1095 |
1095 |
1096 %% HERE |
1096 %% HERE |
1097 |
1097 |
1098 Given our assumptions (on @{text th}), the first property we can |
1098 %Given our assumptions (on @{text th}), the first property we can |
1099 show is that any running thread, say @{text "th'"}, has the same |
1099 %show is that any running thread, say @{text "th'"}, has the same |
1100 precedence as @{text th}: |
1100 %precedence as @{text th}: |
1101 |
1101 |
1102 \begin{lemma}\label{runningpreced} |
1102 %\begin{lemma}\label{runningpreced} |
1103 @{thm [mode=IfThen] running_preced_inversion} |
1103 %@{thm [mode=IfThen] running_preced_inversion} |
1104 \end{lemma} |
1104 %\end{lemma} |
1105 |
1105 |
1106 \begin{proof} |
1106 %\begin{proof} |
1107 By definition, the running thread has as current precedence the maximum of |
1107 %By definition, the running thread has as current precedence the maximum of |
1108 all ready threads, that is |
1108 %all ready threads, that is |
1109 |
1109 |
1110 \begin{center} |
1110 %\begin{center} |
1111 @{term "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"} |
1111 %@{term "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"} |
1112 \end{center} |
1112 %\end{center} |
1113 |
1113 |
1114 \noindent |
1114 %\noindent |
1115 We also know that this is equal to the maximum of current precedences of all threads, |
1115 %We also know that this is equal to the maximum of current precedences of all threads, |
1116 that is |
1116 %that is |
1117 |
1117 |
1118 \begin{center} |
1118 %\begin{center} |
1119 @{term "cp (t @ s) th' = Max (cp (t @ s) ` threads (t @ s))"} |
1119 %@{term "cp (t @ s) th' = Max (cp (t @ s) ` threads (t @ s))"} |
1120 \end{center} |
1120 %\end{center} |
1121 |
1121 |
1122 \noindent |
1122 %\noindent |
1123 This is because each ready thread, say @{text "th\<^sub>r"}, has the maximum |
1123 %This is because each ready thread, say @{text "th\<^sub>r"}, has the maximum |
1124 current precedence of the subtree located at @{text "th\<^sub>r"}. All these |
1124 %current precedence of the subtree located at @{text "th\<^sub>r"}. All these |
1125 subtrees together form the set of threads. |
1125 %subtrees together form the set of threads. |
1126 But the maximum of all threads is the @{term "cp"} of @{text "th"}, |
1126 %But the maximum of all threads is the @{term "cp"} of @{text "th"}, |
1127 which is equal to the @{term preced} of @{text th}.\qed |
1127 %which is equal to the @{term preced} of @{text th}.\qed |
1128 \end{proof} |
1128 %\end{proof} |
1129 |
1129 |
1130 %\endnote{ |
1130 %\endnote{ |
1131 %@{thm "th_blockedE_pretty"} -- thm-blockedE?? |
1131 %@{thm "th_blockedE_pretty"} -- thm-blockedE?? |
1132 % |
1132 % |
1133 % @{text "th_kept"} shows that th is a thread in s'-s |
1133 % @{text "th_kept"} shows that th is a thread in s'-s |
1134 % } |
1134 % } |
1135 |
1135 |
1136 Next we show that a running thread @{text "th'"} must either wait for or |
1136 Given our assumptions (on @{text th}), the first property we show that a running thread @{text "th'"} must either wait for or |
1137 hold a resource in state @{text s}. |
1137 hold a resource in state @{text s}. |
1138 |
1138 |
1139 \begin{lemma}\label{notdetached} |
1139 \begin{lemma}\label{notdetached} |
1140 If @{term "th' \<in> running (s' @ s)"} and @{term "th \<noteq> th'"} then @{term "\<not>detached s th'"}. |
1140 If @{term "th' \<in> running (s' @ s)"} and @{term "th \<noteq> th'"} then @{term "\<not>detached s th'"}. |
1141 \end{lemma} |
1141 \end{lemma} |
1173 threads. This follows from the fact that the @{term "cpreced"}-value |
1173 threads. This follows from the fact that the @{term "cpreced"}-value |
1174 of any ready thread is the maximum of the precedences of all threads |
1174 of any ready thread is the maximum of the precedences of all threads |
1175 in its subtrees (with @{text "th"} having the highest of all threads |
1175 in its subtrees (with @{text "th"} having the highest of all threads |
1176 and being in the subtree of @{text "th'"}). We also have that @{term |
1176 and being in the subtree of @{text "th'"}). We also have that @{term |
1177 "th \<noteq> th'"} since we assumed @{text th} is not running. |
1177 "th \<noteq> th'"} since we assumed @{text th} is not running. |
1178 |
|
1179 By |
1178 By |
1180 Lem.~\ref{notdetached} we have that @{term "\<not>detached s th'"}. |
1179 Lem.~\ref{notdetached} we have that @{term "\<not>detached s th'"}. |
1181 If @{text "th'"} is not detached in @{text s}, that is either |
1180 If @{text "th'"} is not detached in @{text s}, that is either |
1182 holding or waiting for a resource, it must be that @{term "th' \<in> |
1181 holding or waiting for a resource, it must be that @{term "th' \<in> |
1183 threads s"}. By Lem.~\ref{runningpreced} we have |
1182 threads s"}.\medskip |
1184 |
1183 |
1185 \begin{center} |
|
1186 @{term "cp (t @ s) th' = preced th s"} |
|
1187 \end{center} |
|
1188 |
|
1189 \noindent |
1184 \noindent |
1190 This concludes the proof of Theorem 1.\qed |
1185 This concludes the proof of Theorem 1.\qed |
1191 \end{proof} |
1186 \end{proof} |
1192 |
1187 |
1193 |
1188 |