298 |
298 |
299 text {* \noindent |
299 text {* \noindent |
300 The following @{text "cp"} is a shorthand for @{text "cprec_fun"}. |
300 The following @{text "cp"} is a shorthand for @{text "cprec_fun"}. |
301 *} |
301 *} |
302 definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence" |
302 definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence" |
303 where "cp s = cprec_fun (schs s)" |
303 where "cp s \<equiv> cprec_fun (schs s)" |
304 |
304 |
305 text {* \noindent |
305 text {* \noindent |
306 Functions @{text "holding"}, @{text "waiting"}, @{text "depend"} and |
306 Functions @{text "holding"}, @{text "waiting"}, @{text "depend"} and |
307 @{text "dependents"} still have the |
307 @{text "dependents"} still have the |
308 same meaning, but redefined so that they no longer depend on the |
308 same meaning, but redefined so that they no longer depend on the |
309 fictitious {\em waiting queue function} |
309 fictitious {\em waiting queue function} |
310 @{text "wq"}, but on system state @{text "s"}. |
310 @{text "wq"}, but on system state @{text "s"}. |
311 *} |
311 *} |
312 defs (overloaded) |
312 defs (overloaded) |
313 s_holding_abv: |
313 s_holding_abv: |
314 "holding (s::state) \<equiv> holding (wq s)" |
314 "holding (s::state) \<equiv> holding (wq_fun (schs s))" |
315 s_waiting_abv: |
315 s_waiting_abv: |
316 "waiting (s::state) \<equiv> waiting (wq s)" |
316 "waiting (s::state) \<equiv> waiting (wq_fun (schs s))" |
317 s_depend_abv: |
317 s_depend_abv: |
318 "depend (s::state) \<equiv> depend (wq s)" |
318 "depend (s::state) \<equiv> depend (wq_fun (schs s))" |
319 s_dependents_abv: |
319 s_dependents_abv: |
320 "dependents (s::state) th \<equiv> dependents (wq s) th" |
320 "dependents (s::state) \<equiv> dependents (wq_fun (schs s))" |
321 |
321 |
322 |
322 |
323 text {* |
323 text {* |
324 The following lemma can be proved easily: |
324 The following lemma can be proved easily: |
325 *} |
325 *} |
326 lemma |
326 lemma |
327 s_holding_def: |
327 s_holding_def: |
328 "holding (s::state) thread cs = (thread \<in> set (wq s cs) \<and> thread = hd (wq s cs))" |
328 "holding (s::state) th cs \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th = hd (wq_fun (schs s) cs))" |
329 by (auto simp:s_holding_abv wq_def cs_holding_def) |
329 by (auto simp:s_holding_abv wq_def cs_holding_def) |
330 |
330 |
331 lemma s_waiting_def: |
331 lemma s_waiting_def: |
332 "waiting (s::state) thread cs = (thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs))" |
332 "waiting (s::state) th cs \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th \<noteq> hd (wq_fun (schs s) cs))" |
333 by (auto simp:s_waiting_abv wq_def cs_waiting_def) |
333 by (auto simp:s_waiting_abv wq_def cs_waiting_def) |
334 |
334 |
335 lemma s_depend_def: |
335 lemma s_depend_def: |
336 "depend (s::state) = |
336 "depend (s::state) = |
337 {(Th th, Cs cs) | th cs. waiting (wq s) th cs} \<union> {(Cs cs, Th th) | cs th. holding (wq s) th cs}" |
337 {(Th th, Cs cs) | th cs. waiting (wq s) th cs} \<union> {(Cs cs, Th th) | cs th. holding (wq s) th cs}" |
352 text {* \noindent |
352 text {* \noindent |
353 The following function @{text "runing"} calculates the set of running thread, which is the ready |
353 The following function @{text "runing"} calculates the set of running thread, which is the ready |
354 thread with the highest precedence. |
354 thread with the highest precedence. |
355 *} |
355 *} |
356 definition runing :: "state \<Rightarrow> thread set" |
356 definition runing :: "state \<Rightarrow> thread set" |
357 where "runing s = {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}" |
357 where "runing s \<equiv> {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}" |
358 |
358 |
359 text {* \noindent |
359 text {* \noindent |
360 The following function @{text "holdents s th"} returns the set of resources held by thread |
360 The following function @{text "holdents s th"} returns the set of resources held by thread |
361 @{text "th"} in state @{text "s"}. |
361 @{text "th"} in state @{text "s"}. |
362 *} |
362 *} |
363 definition holdents :: "state \<Rightarrow> thread \<Rightarrow> cs set" |
363 definition holdents :: "state \<Rightarrow> thread \<Rightarrow> cs set" |
364 where "holdents s th = {cs . (Cs cs, Th th) \<in> depend s}" |
364 where "holdents s th \<equiv> {cs . (Cs cs, Th th) \<in> depend s}" |
365 |
365 |
366 text {* \noindent |
366 text {* \noindent |
367 @{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in |
367 @{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in |
368 state @{text "s"}: |
368 state @{text "s"}: |
369 *} |
369 *} |
410 text {* \noindent |
410 text {* \noindent |
411 With predicate @{text "step"}, the fact that @{text "s"} is a legal state in |
411 With predicate @{text "step"}, the fact that @{text "s"} is a legal state in |
412 Priority Inheritance protocol can be expressed as: @{text "vt step s"}, where |
412 Priority Inheritance protocol can be expressed as: @{text "vt step s"}, where |
413 the predicate @{text "vt"} can be defined as the following: |
413 the predicate @{text "vt"} can be defined as the following: |
414 *} |
414 *} |
415 inductive vt :: "(state \<Rightarrow> event \<Rightarrow> bool) \<Rightarrow> state \<Rightarrow> bool" |
415 inductive vt :: "state \<Rightarrow> bool" |
416 for cs -- {* @{text "cs"} is an argument representing any step predicate. *} |
|
417 where |
416 where |
418 -- {* Empty list @{text "[]"} is a legal state in any protocol:*} |
417 -- {* Empty list @{text "[]"} is a legal state in any protocol:*} |
419 vt_nil[intro]: "vt cs []" | |
418 vt_nil[intro]: "vt []" | |
420 -- {* |
419 -- {* |
421 \begin{minipage}{0.9\textwidth} |
420 \begin{minipage}{0.9\textwidth} |
422 If @{text "s"} a legal state, and event @{text "e"} is eligible to happen |
421 If @{text "s"} a legal state, and event @{text "e"} is eligible to happen |
423 in state @{text "s"}, then @{text "e#s"} is a legal state as well: |
422 in state @{text "s"}, then @{text "e#s"} is a legal state as well: |
424 \end{minipage} |
423 \end{minipage} |
425 *} |
424 *} |
426 vt_cons[intro]: "\<lbrakk>vt cs s; cs s e\<rbrakk> \<Longrightarrow> vt cs (e#s)" |
425 vt_cons[intro]: "\<lbrakk>vt s; step s e\<rbrakk> \<Longrightarrow> vt (e#s)" |
427 |
426 |
428 text {* \noindent |
427 text {* \noindent |
429 It is easy to see that the definition of @{text "vt"} is generic. It can be applied to |
428 It is easy to see that the definition of @{text "vt"} is generic. It can be applied to |
430 any step predicate to get the set of legal states. |
429 any step predicate to get the set of legal states. |
431 *} |
430 *} |