1186 \end{proof} |
1186 \end{proof} |
1187 |
1187 |
1188 |
1188 |
1189 %\endnote{ |
1189 %\endnote{ |
1190 |
1190 |
1191 In what follows we will describe properties of PIP that allow us to |
1191 %In what follows we will describe properties of PIP that allow us to |
1192 prove Theorem~\ref{mainthm} and, when instructive, briefly describe |
1192 % prove Theorem~\ref{mainthm} and, when instructive, briefly describe |
1193 our argument. Recall we want to prove that in state @ {term "s' @ s"} |
1193 % our argument. Recall we want to prove that in state @ {term "s' @ s"} |
1194 either @{term th} is either running or blocked by a thread @ |
1194 %either @{term th} is either running or blocked by a thread @ |
1195 {term "th'"} (@{term "th \<noteq> th'"}) which was alive in state |
1195 % {term "th'"} (@{term "th \<noteq> th'"}) which was alive in state |
1196 @{term s}. We can show that |
1196 % @{term s}. We can show that |
1197 |
1197 |
1198 |
1198 |
1199 \begin{lemma} |
1199 % \begin{lemma} |
1200 If @{thm (prem 2) eq_pv_blocked} |
1200 % If @{thm (prem 2) eq_pv_blocked} |
1201 then @{thm (concl) eq_pv_blocked} |
1201 % then @{thm (concl) eq_pv_blocked} |
1202 \end{lemma} |
1202 % \end{lemma} |
1203 |
1203 |
1204 \begin{lemma} |
1204 % \begin{lemma} |
1205 If @{thm (prem 2) eq_pv_persist} |
1205 % If @{thm (prem 2) eq_pv_persist} |
1206 then @{thm (concl) eq_pv_persist} |
1206 % then @{thm (concl) eq_pv_persist} |
1207 \end{lemma} |
1207 % \end{lemma} |
1208 %%%} |
1208 %%%} |
1209 |
1209 |
1210 % \endnote{{\bf OUTLINE} |
1210 % \endnote{{\bf OUTLINE} |
1211 |
1211 |
1212 Since @{term "th"} is the most urgent thread, if it is somehow |
1212 % Since @{term "th"} is the most urgent thread, if it is somehow |
1213 blocked, people want to know why and wether this blocking is |
1213 % blocked, people want to know why and wether this blocking is |
1214 reasonable. |
1214 % reasonable. |
1215 |
1215 |
1216 @{thm [source] th_blockedE} @{thm th_blockedE} |
1216 % @{thm [source] th_blockedE} @{thm th_blockedE} |
1217 |
1217 |
1218 if @{term "th"} is blocked, then there is a path leading from |
1218 % if @{term "th"} is blocked, then there is a path leading from |
1219 @{term "th"} to @{term "th'"}, which means: |
1219 % @{term "th"} to @{term "th'"}, which means: |
1220 there is a chain of demand leading from @{term th} to @{term th'}. |
1220 % there is a chain of demand leading from @{term th} to @{term th'}. |
1221 |
1221 |
1222 in other words |
1222 % in other words |
1223 th -> cs1 -> th1 -> cs2 -> th2 -> ... -> csn -> thn -> cs -> th'. |
1223 % th -> cs1 -> th1 -> cs2 -> th2 -> ... -> csn -> thn -> cs -> th'. |
1224 |
1224 |
1225 We says that th is blocked by @{text "th'"}. |
1225 % We says that th is blocked by @{text "th'"}. |
1226 |
1226 |
1227 THEN |
1227 % THEN |
1228 |
1228 |
1229 @{thm [source] vat_t.th_chain_to_ready} @{thm vat_t.th_chain_to_ready} |
1229 % @{thm [source] vat_t.th_chain_to_ready} @{thm vat_t.th_chain_to_ready} |
1230 |
1230 |
1231 It is basic propery with non-trival proof. |
1231 % It is basic propery with non-trival proof. |
1232 |
1232 |
1233 THEN |
1233 % THEN |
1234 |
1234 |
1235 @{thm [source] max_preced} @{thm max_preced} |
1235 % @{thm [source] max_preced} @{thm max_preced} |
1236 |
1236 |
1237 which says @{term "th"} holds the max precedence. |
1237 % which says @{term "th"} holds the max precedence. |
1238 |
1238 |
1239 THEN |
1239 % THEN |
1240 |
1240 |
1241 @{thm [source] th_cp_max th_cp_preced th_kept} |
1241 % @ {thm [source] th_cp_max th_cp_preced th_kept} |
1242 @{thm th_cp_max th_cp_preced th_kept} |
1242 % @ {thm th_cp_max th_cp_preced th_kept} |
1243 |
1243 |
1244 THEN |
1244 % THEN |
1245 |
1245 |
1246 ??? %%@ {thm [source] running_inversion_4} @ {thm running_inversion_4} |
1246 % ??? %%@ {thm [source] running_inversion_4} @ {thm running_inversion_4} |
1247 |
1247 |
1248 which explains what the @{term "th'"} looks like. Now, we have found the |
1248 % which explains what the @{term "th'"} looks like. Now, we have found the |
1249 @{term "th'"} which blocks @{term th}, we need to know more about it. |
1249 % @{term "th'"} which blocks @{term th}, we need to know more about it. |
1250 To see what kind of thread can block @{term th}. |
1250 % To see what kind of thread can block @{term th}. |
1251 |
1251 |
1252 From these two lemmas we can see the correctness of PIP, which is |
1252 % From these two lemmas we can see the correctness of PIP, which is |
1253 that: the blockage of th is reasonable and under control. |
1253 % that: the blockage of th is reasonable and under control. |
1254 |
1254 |
1255 Lemmas we want to describe: |
1255 % Lemmas we want to describe: |
1256 |
1256 |
1257 \begin{lemma} |
1257 % \begin{lemma} |
1258 @{thm running_cntP_cntV_inv} |
1258 % @{thm running_cntP_cntV_inv} |
1259 \end{lemma} |
1259 % \end{lemma} |
1260 |
1260 |
1261 \noindent |
1261 % \noindent |
1262 Remember we do not have the well-nestedness restriction in our |
1262 % Remember we do not have the well-nestedness restriction in our |
1263 proof, which means the difference between the counters @{const cntV} |
1263 % proof, which means the difference between the counters @{const cntV} |
1264 and @{const cntP} can be larger than @{term 1}. |
1264 % and @{const cntP} can be larger than @{term 1}. |
1265 |
1265 |
1266 \begin{lemma}\label{runninginversion} |
1266 % \begin{lemma}\label{runninginversion} |
1267 @{thm running_inversion} |
1267 % @ {thm running_inversion} |
1268 \end{lemma} |
1268 % \end{lemma} |
1269 |
1269 |
1270 explain tRAG |
1270 % explain tRAG |
1271 %} |
1271 %} |
1272 |
1272 |
1273 |
1273 |
1274 % Suppose the thread @ {term th} is \emph{not} running in state @ {term |
1274 % Suppose the thread @ {term th} is \emph{not} running in state @ {term |
1275 % "t @ s"}, meaning that it should be blocked by some other thread. |
1275 % "t @ s"}, meaning that it should be blocked by some other thread. |