1157 |
1157 |
1158 \begin{proof}[of Theorem 1] If @{term "th \<in> running (s' @ s)"}, |
1158 \begin{proof}[of Theorem 1] If @{term "th \<in> running (s' @ s)"}, |
1159 then there is nothing to show. So let us assume otherwise. Since the |
1159 then there is nothing to show. So let us assume otherwise. Since the |
1160 @{text "RAG"} is well-founded, we know there exists an ancestor of |
1160 @{text "RAG"} is well-founded, we know there exists an ancestor of |
1161 @{text "th"} that is the root of the corrsponding subtree and |
1161 @{text "th"} that is the root of the corrsponding subtree and |
1162 therefore is ready. Let us call this thread @{text "th'"}. We know |
1162 therefore is ready (it does not request any resources). Let us call |
1163 that @{text "th'"} has the highest precedence of all ready threads. |
1163 this thread @{text "th'"}. Since in PIP the @{term "cpreced"}-value |
1164 Therefore it is running. We have that @{term "th \<noteq> th'"} |
1164 of any thread equals the maximum precedence of all threads in its |
1165 since we assumed @{text th} is not running. By |
1165 @{term "RAG"}-subtree, and @{text "th"} is in the subtree of @{text |
|
1166 "th'"}, the @{term "cpreced"}-value of @{text "th'"} cannot be lower |
|
1167 than the precedence of @{text "th"}. But, it can also not be higher, |
|
1168 because the precedence of @{text "th"} is the maximum among all |
|
1169 threads. Therefore we know that the @{term "cpreced"}-value of |
|
1170 @{text "th'"} is the same as the precedence of @{text "th"}. The |
|
1171 result is that @{text "th'"} must be running. This is because @{term |
|
1172 "cpreced"}-value of @{text "th'"} is the highest of all ready |
|
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 |
|
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 |
|
1177 "th \<noteq> th'"} since we assumed @{text th} is not running. |
|
1178 |
|
1179 By |
1166 Lem.~\ref{notdetached} we have that @{term "\<not>detached s th'"}. |
1180 Lem.~\ref{notdetached} we have that @{term "\<not>detached s th'"}. |
1167 If @{text "th'"} is not detached in @{text s}, that is either |
1181 If @{text "th'"} is not detached in @{text s}, that is either |
1168 holding or waiting for a resource, it must be that @{term "th' \<in> |
1182 holding or waiting for a resource, it must be that @{term "th' \<in> |
1169 threads s"}. By Lem.~\ref{runningpreced} we have |
1183 threads s"}. By Lem.~\ref{runningpreced} we have |
1170 |
1184 |