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 |
1072 |
|
1073 %% HERE |
|
1074 |
|
1075 Given our assumptions (on @{text th}), the first property we can |
|
1076 show is that any running thread, say @{text "th'"}, has the same |
|
1077 precedence of @{text th}: |
|
1078 |
|
1079 \begin{lemma}\label{runningpreced} |
|
1080 @{thm [mode=IfThen] running_preced_inversion} |
|
1081 \end{lemma} |
|
1082 |
|
1083 \begin{proof} |
|
1084 By definition the running thread has as precedence the maximum of |
|
1085 all ready threads, that is |
|
1086 |
|
1087 \begin{center} |
|
1088 @{term "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"} |
|
1089 \end{center} |
|
1090 \end{proof} |
|
1091 |
|
1092 @{thm "th_blockedE_pretty"} -- thm-blockedE?? |
|
1093 |
|
1094 |
1073 @{text "th_kept"} shows that th is a thread in s'-s |
1095 @{text "th_kept"} shows that th is a thread in s'-s |
|
1096 |
|
1097 |
|
1098 |
1074 |
1099 |
1075 \begin{proof}[of Theorem 1] |
1100 \begin{proof}[of Theorem 1] |
1076 If @{term "th \<in> running (s' @ s)"}, then there is nothing to show. So let us |
1101 If @{term "th \<in> running (s' @ s)"}, then there is nothing to show. So let us |
1077 assume otherwise. |
1102 assume otherwise. By Lem.~\ref{thblockedE} we know there exists a thread |
|
1103 @{text "th'"} that is an acestor of @{text th} in the @{text "RAG"} |
|
1104 and @{text "th'"} is running, that is we know |
|
1105 |
|
1106 \begin{center} |
|
1107 @{term "th' \<in> nancestors (tG (s' @ s)) th"} \quad and \quad |
|
1108 @{term "th' \<in> running (s' @ s)"} |
|
1109 \end{center} |
|
1110 |
|
1111 \noindent We have that @{term "th \<noteq> th'"} since we assumed |
|
1112 @{text th} is not running. By Lem.~\ref{thkept}, we know that |
|
1113 @{text "th'"} is also running in state @{text s} and by |
|
1114 Lem.~\ref{detached} that @{term "\<not>detached s th'"}. |
|
1115 By Lem.~\ref{runningpreced} we have |
|
1116 |
|
1117 \begin{center} |
|
1118 @{term "cp (t @ s) th' = preced th s"} |
|
1119 \end{center} |
|
1120 |
|
1121 \noindent |
|
1122 This concludes the proof of Theorem 1. |
1078 \end{proof} |
1123 \end{proof} |
|
1124 |
|
1125 |
|
1126 |
1079 |
1127 |
1080 In what follows we will describe properties of PIP that allow us to |
1128 In what follows we will describe properties of PIP that allow us to |
1081 prove Theorem~\ref{mainthm} and, when instructive, briefly describe |
1129 prove Theorem~\ref{mainthm} and, when instructive, briefly describe |
1082 our argument. Recall we want to prove that in state @{term "s' @ s"} |
1130 our argument. Recall we want to prove that in state @{term "s' @ s"} |
1083 either @{term th} is either running or blocked by a thread @{term |
1131 either @{term th} is either running or blocked by a thread @{term |
1159 \end{lemma} |
1207 \end{lemma} |
1160 |
1208 |
1161 explain tRAG |
1209 explain tRAG |
1162 \bigskip |
1210 \bigskip |
1163 |
1211 |
1164 |
1212 |
1165 Suppose the thread @{term th} is \emph{not} running in state @{term |
1213 Suppose the thread @{term th} is \emph{not} running in state @{term |
1166 "t @ s"}, meaning that it should be blocked by some other thread. |
1214 "t @ s"}, meaning that it should be blocked by some other thread. |
1167 It is first shown that there is a path in the RAG leading from node |
1215 It is first shown that there is a path in the RAG leading from node |
1168 @{term th} to another thread @{text "th'"}, which is also in the |
1216 @{term th} to another thread @{text "th'"}, which is also in the |
1169 @{term readys}-set. Since @{term readys}-set is non-empty, there |
1217 @{term readys}-set. Since @{term readys}-set is non-empty, there |
1171 by definition, is currently the @{term running}-thread. However, we |
1219 by definition, is currently the @{term running}-thread. However, we |
1172 are going to show in the next lemma slightly more: this running |
1220 are going to show in the next lemma slightly more: this running |
1173 thread is exactly @{term "th'"}. |
1221 thread is exactly @{term "th'"}. |
1174 |
1222 |
1175 \begin{lemma} |
1223 \begin{lemma} |
1176 If @{thm (prem 1) th_blockedE_pretty} then there exists a thread @{text "th'"} |
1224 There exists a thread @{text "th'"} |
1177 such that @{thm (no_quants) th_blockedE_pretty}. |
1225 such that @{thm (no_quants) th_blockedE_pretty}. |
1178 \end{lemma} |
1226 \end{lemma} |
1179 |
1227 |
1180 \begin{proof} |
1228 \begin{proof} |
1181 We know that @{term th} cannot be in @{term readys}, because it has |
1229 We know that @{term th} cannot be in @{term readys}, because it has |