256 same meaning, but redefined so that they no longer depend on the |
256 same meaning, but redefined so that they no longer depend on the |
257 fictitious {\em waiting queue function} |
257 fictitious {\em waiting queue function} |
258 @{text "wq"}, but on system state @{text "s"}. |
258 @{text "wq"}, but on system state @{text "s"}. |
259 *} |
259 *} |
260 defs (overloaded) |
260 defs (overloaded) |
|
261 s_holding_abv: |
|
262 "holding (s::state) \<equiv> holding (wq s)" |
|
263 s_waiting_abv: |
|
264 "waiting (s::state) \<equiv> waiting (wq s)" |
|
265 s_depend_abv: |
|
266 "depend (s::state) \<equiv> depend (wq s)" |
|
267 s_dependents_abv: |
|
268 "dependents (s::state) th \<equiv> dependents (wq s) th" |
|
269 |
|
270 |
|
271 text {* |
|
272 The following lemma can be proved easily: |
|
273 *} |
|
274 lemma |
261 s_holding_def: |
275 s_holding_def: |
262 "holding (s::state) thread cs \<equiv> (thread \<in> set (wq s cs) \<and> thread = hd (wq s cs))" |
276 "holding (s::state) thread cs = (thread \<in> set (wq s cs) \<and> thread = hd (wq s cs))" |
263 s_waiting_def: |
277 by (auto simp:s_holding_abv wq_def cs_holding_def) |
264 "waiting (s::state) thread cs \<equiv> (thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs))" |
278 |
265 s_depend_def: |
279 lemma s_waiting_def: |
266 "depend (s::state) \<equiv> |
280 "waiting (s::state) thread cs = (thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs))" |
|
281 by (auto simp:s_waiting_abv wq_def cs_waiting_def) |
|
282 |
|
283 lemma s_depend_def: |
|
284 "depend (s::state) = |
267 {(Th th, Cs cs) | th cs. waiting (wq s) th cs} \<union> {(Cs cs, Th th) | cs th. holding (wq s) th cs}" |
285 {(Th th, Cs cs) | th cs. waiting (wq s) th cs} \<union> {(Cs cs, Th th) | cs th. holding (wq s) th cs}" |
|
286 by (auto simp:s_depend_abv wq_def cs_depend_def) |
|
287 |
|
288 lemma |
268 s_dependents_def: |
289 s_dependents_def: |
269 "dependents (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}" |
290 "dependents (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}" |
|
291 by (auto simp:s_dependents_abv wq_def cs_dependents_def) |
270 |
292 |
271 text {* |
293 text {* |
272 The following function @{text "readys"} calculates the set of ready threads. A thread is {\em ready} |
294 The following function @{text "readys"} calculates the set of ready threads. A thread is {\em ready} |
273 for running if it is a live thread and it is not waiting for any critical resource. |
295 for running if it is a live thread and it is not waiting for any critical resource. |
274 *} |
296 *} |