185 "RAG_raw wq \<equiv> |
185 "RAG_raw wq \<equiv> |
186 {(Th th, Cs cs) | th cs. waiting_raw wq th cs} \<union> |
186 {(Th th, Cs cs) | th cs. waiting_raw wq th cs} \<union> |
187 {(Cs cs, Th th) | cs th. holding_raw wq th cs}" |
187 {(Cs cs, Th th) | cs th. holding_raw wq th cs}" |
188 |
188 |
189 text {* |
189 text {* |
190 |
190 The following notion of {\em Thread Graph}, denoted @{text "tG_raw"}, is |
191 \noindent The following @{text "dependants wq th"} represents the set of |
191 the graph derived from @{text "RAG_raw"} by hiding all resource nodes. |
192 threads which are waiting on thread @{text "th"} in Resource Allocation |
192 It is more concise to use in many contexts. |
193 Graph @{text "RAG wq"}. Here, "waiting" means waiting directly or |
193 *} |
194 indirectly on the critical resource. *} |
|
195 |
|
196 definition |
194 definition |
197 dependants_raw :: "(cs \<Rightarrow> thread list) \<Rightarrow> thread \<Rightarrow> thread set" |
195 "tG_raw wq = {(th\<^sub>1, th\<^sub>2) | th\<^sub>1 th\<^sub>2. |
198 where |
196 \<exists> cs. (Th th\<^sub>1, Cs cs) \<in> RAG_raw wq \<and> (Cs cs, Th th\<^sub>2) \<in> RAG_raw wq}" |
199 "dependants_raw wq th \<equiv> {th' . (Th th', Th th) \<in> (RAG_raw wq)^+}" |
|
200 |
197 |
201 text {* |
198 text {* |
202 |
199 |
203 \noindent The following @{text "cpreced s th"} gives the {\em current |
200 \noindent The following @{text "cpreced s th"} gives the {\em current |
204 precedence} of thread @{text "th"} under state @{text "s"}. The definition |
201 precedence} of thread @{text "th"} under state @{text "s"}. The definition |
205 of @{text "cpreced"} reflects the basic idea of Priority Inheritance that |
202 of @{text "cpreced"} reflects the basic idea of Priority Inheritance that |
206 the {\em current precedence} of a thread is the precedence inherited from |
203 the {\em current precedence} of a thread is the precedence inherited from |
207 the maximum of all its dependants, i.e. the threads which are waiting |
204 the maximum precedence of all threads in its sub-tree in @{text RAG} |
208 directly or indirectly waiting for some resources from it. If no such |
205 (or the @{text tG}). |
209 thread exits, @{text "th"}'s {\em current precedence} equals its original |
206 "}. |
210 precedence, i.e. @{text "preced th s"}. *} |
207 *} |
211 |
208 |
212 definition |
209 definition |
213 cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence" |
210 cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence" |
214 where |
211 where |
215 "cpreced wq s th \<equiv> Max ({preced th s} \<union> preceds (dependants_raw wq th) s)" |
212 "cpreced wq s th \<equiv> Max (preceds (subtree (tG_raw wq) th) s)" |
216 |
|
217 |
|
218 |
|
219 text {* |
|
220 |
|
221 Notice that the current precedence (@{text "cpreced"}) of one thread |
|
222 @{text "th"} can be boosted (increased) by those threads in the @{text |
|
223 "dependants wq th"}-set. If one thread gets boosted, we say it inherits |
|
224 the priority (or, more precisely, the precedence) of its dependants. This |
|
225 is whrere the word "Inheritance" in Priority Inheritance Protocol comes |
|
226 from. *} |
|
227 |
|
228 lemma cpreced_def2: |
|
229 "cpreced wq s th \<equiv> Max ((\<lambda>th'. preced th' s) ` ({th} \<union> dependants_raw wq th))" |
|
230 unfolding cpreced_def image_def |
|
231 apply(rule eq_reflection) |
|
232 apply(rule_tac f="Max" in arg_cong) |
|
233 by (auto) |
|
234 |
|
235 lemma cpreced_def3: |
|
236 "cpreced wq s th \<equiv> Max (preceds ({th} \<union> dependants_raw wq th) s)" |
|
237 unfolding cpreced_def2 image_def |
|
238 apply(rule eq_reflection) |
|
239 apply(rule_tac f="Max" in arg_cong) |
|
240 by (auto) |
|
241 |
213 |
242 definition |
214 definition |
243 cpreceds :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread set \<Rightarrow> precedence set" |
215 cpreceds :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread set \<Rightarrow> precedence set" |
244 where |
216 where |
245 "cpreceds wq s ths \<equiv> {cpreced wq s th | th. th \<in> ths}" |
217 "cpreceds wq s ths \<equiv> {cpreced wq s th | th. th \<in> ths}" |
379 | "schs (V th cs # s) = |
351 | "schs (V th cs # s) = |
380 (let wq = wq_fun (schs s) in |
352 (let wq = wq_fun (schs s) in |
381 let new_wq = wq(cs := release (wq cs)) in |
353 let new_wq = wq(cs := release (wq cs)) in |
382 (|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))" |
354 (|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))" |
383 |
355 |
|
356 |
384 lemma cpreced_initial: |
357 lemma cpreced_initial: |
385 "cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))" |
358 "cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))" |
386 apply(rule ext) |
359 proof - |
387 apply(simp add: cpreced_def) |
360 have [simp]: "(RAG_raw all_unlocked) = {}" |
388 apply(simp add: dependants_raw_def RAG_raw_def waiting_raw_def holding_raw_def) |
361 by (unfold RAG_raw_def, auto simp:waiting_raw_def holding_raw_def) |
389 apply(simp add: preced_def) |
362 have [simp]: "\<forall> x. (subtree {} x) = {x}" |
390 done |
363 by (unfold subtree_def, auto) |
391 |
364 show ?thesis by (rule ext, auto simp:cpreced_def tG_raw_def preced_def) |
392 text {* |
365 qed |
393 |
366 |
|
367 text {* |
394 \noindent The following @{text "wq"} is a shorthand for @{text "wq_fun"}. |
368 \noindent The following @{text "wq"} is a shorthand for @{text "wq_fun"}. |
395 *} |
369 *} |
396 |
370 |
397 definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list" |
371 definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list" |
398 where "wq s = wq_fun (schs s)" |
372 where "wq s = wq_fun (schs s)" |
406 where "cp s \<equiv> cprec_fun (schs s)" |
380 where "cp s \<equiv> cprec_fun (schs s)" |
407 |
381 |
408 text {* |
382 text {* |
409 |
383 |
410 \noindent Functions @{text "holding"}, @{text "waiting"}, @{text "RAG"} |
384 \noindent Functions @{text "holding"}, @{text "waiting"}, @{text "RAG"} |
411 and @{text "dependants"} still have the same meaning, but redefined so |
385 and @{text "tG"} still have the same meaning, but redefined so |
412 that they no longer RAG on the fictitious {\em waiting queue function} |
386 that they no longer RAG on the fictitious {\em waiting queue function} |
413 @{text "wq"}, but on system state @{text "s"}. *} |
387 @{text "wq"}, but on system state @{text "s"}. *} |
414 |
388 |
415 definition |
389 definition |
416 s_holding_abv: |
390 s_holding_abv: |
463 |
433 |
464 lemma eq_RAG: |
434 lemma eq_RAG: |
465 "RAG_raw (wq s) = RAG s" |
435 "RAG_raw (wq s) = RAG s" |
466 by (unfold RAG_raw_def s_RAG_def, auto) |
436 by (unfold RAG_raw_def s_RAG_def, auto) |
467 |
437 |
468 |
|
469 lemma s_dependants_def: |
|
470 shows "dependants (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (RAG s)^+}" |
|
471 using dependants_raw_def eq_RAG s_dependants_abv wq_def by auto |
|
472 |
|
473 text {* |
438 text {* |
474 |
439 |
475 The following function @{text "readys"} calculates the set of ready |
440 The following function @{text "readys"} calculates the set of ready |
476 threads. A thread is {\em ready} for running if it is a live thread and it |
441 threads. A thread is {\em ready} for running if it is a live thread and it |
477 is not waiting for any critical resource. *} |
442 is not waiting for any critical resource. *} |
707 text {* |
672 text {* |
708 A notion of {\em thread graph} (@{text tG}) is introduced to hide derivations using |
673 A notion of {\em thread graph} (@{text tG}) is introduced to hide derivations using |
709 tRAG, so that it is easier to understand. |
674 tRAG, so that it is easier to understand. |
710 *} |
675 *} |
711 |
676 |
712 |
677 definition |
713 definition "tG s = (map_prod the_thread the_thread) `(tRAG s)" |
678 s_tG_abv: |
|
679 "tG (s::state) \<equiv> tG_raw (wq s)" |
714 |
680 |
715 lemma tG_alt_def: |
681 lemma tG_alt_def: |
716 "tG s = {(th1, th2) | th1 th2. |
682 "tG s = {(th1, th2) | th1 th2. |
717 \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}" (is "?L = ?R") |
683 \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}" (is "?L = ?R") |
|
684 by (unfold s_tG_abv s_RAG_abv tG_raw_def, simp) |
|
685 |
|
686 lemma tRAG_def_tG: "tRAG s = (map_prod Th Th) ` (tG s)" |
|
687 by (unfold tRAG_alt_def tG_alt_def, auto) |
|
688 |
|
689 lemma tG_def_tRAG: "tG s = map_prod the_thread the_thread ` tRAG s" |
718 proof - |
690 proof - |
719 { fix th1 th2 |
691 have [simp]: "(map_prod the_thread the_thread \<circ> map_prod Th Th) = id" |
720 assume "(th1, th2) \<in> ?L" |
692 by (rule ext, auto) |
721 hence "(th1, th2) \<in> ?R" by (auto simp:tG_def tRAG_alt_def) |
693 show ?thesis by (unfold tRAG_def_tG image_comp, simp) |
722 } moreover { |
|
723 fix th1 th2 |
|
724 assume "(th1, th2) \<in> ?R" |
|
725 then obtain cs where "(Th th1, Cs cs) \<in> RAG s" "(Cs cs, Th th2) \<in> RAG s" by auto |
|
726 hence "(Th th1, Th th2) \<in> (wRAG s O hRAG s)" by (auto simp:RAG_split wRAG_def hRAG_def) |
|
727 hence "(Th th1, Th th2) \<in> tRAG s" by (unfold tRAG_def, simp) |
|
728 hence "(th1, th2) \<in> ?L" by (simp add: tG_def rev_image_eqI) |
|
729 } ultimately show ?thesis by (meson pred_equals_eq2) |
|
730 qed |
694 qed |
731 |
|
732 lemma tRAG_def_tG: "tRAG s = (map_prod Th Th) ` (tG s)" (is "?L = ?R") |
|
733 proof - |
|
734 have "?L = (\<lambda> x. x) ` ?L" by simp |
|
735 also have "... = ?R" |
|
736 proof(unfold tG_def image_comp, induct rule:image_cong) |
|
737 case (2 e) |
|
738 thus ?case by (unfold tRAG_alt_def, auto) |
|
739 qed auto |
|
740 finally show ?thesis . |
|
741 qed |
|
742 |
|
743 |
695 |
744 fun actor where |
696 fun actor where |
745 "actor (Exit th) = th" | |
697 "actor (Exit th) = th" | |
746 "actor (P th cs) = th" | |
698 "actor (P th cs) = th" | |
747 "actor (V th cs) = th" | |
699 "actor (V th cs) = th" | |