diff -r da27bece9575 -r f9e6c4166476 PIPDefs.thy --- a/PIPDefs.thy Fri Jun 23 00:27:16 2017 +0100 +++ b/PIPDefs.thy Tue Jun 27 14:49:42 2017 +0100 @@ -1,6 +1,6 @@ (*<*) theory PIPDefs -imports Precedence_ord Max +imports Precedence_ord Max RTree begin (*>*) @@ -187,16 +187,13 @@ {(Cs cs, Th th) | cs th. holding_raw wq th cs}" text {* - - \noindent The following @{text "dependants wq th"} represents the set of - threads which are waiting on thread @{text "th"} in Resource Allocation - Graph @{text "RAG wq"}. Here, "waiting" means waiting directly or - indirectly on the critical resource. *} - + The following notion of {\em Thread Graph}, denoted @{text "tG_raw"}, is + the graph derived from @{text "RAG_raw"} by hiding all resource nodes. + It is more concise to use in many contexts. +*} definition - dependants_raw :: "(cs \ thread list) \ thread \ thread set" -where - "dependants_raw wq th \ {th' . (Th th', Th th) \ (RAG_raw wq)^+}" + "tG_raw wq = {(th\<^sub>1, th\<^sub>2) | th\<^sub>1 th\<^sub>2. + \ cs. (Th th\<^sub>1, Cs cs) \ RAG_raw wq \ (Cs cs, Th th\<^sub>2) \ RAG_raw wq}" text {* @@ -204,40 +201,15 @@ precedence} of thread @{text "th"} under state @{text "s"}. The definition of @{text "cpreced"} reflects the basic idea of Priority Inheritance that the {\em current precedence} of a thread is the precedence inherited from - the maximum of all its dependants, i.e. the threads which are waiting - directly or indirectly waiting for some resources from it. If no such - thread exits, @{text "th"}'s {\em current precedence} equals its original - precedence, i.e. @{text "preced th s"}. *} + the maximum precedence of all threads in its sub-tree in @{text RAG} + (or the @{text tG}). +"}. +*} definition cpreced :: "(cs \ thread list) \ state \ thread \ precedence" where - "cpreced wq s th \ Max ({preced th s} \ preceds (dependants_raw wq th) s)" - - - -text {* - - Notice that the current precedence (@{text "cpreced"}) of one thread - @{text "th"} can be boosted (increased) by those threads in the @{text - "dependants wq th"}-set. If one thread gets boosted, we say it inherits - the priority (or, more precisely, the precedence) of its dependants. This - is whrere the word "Inheritance" in Priority Inheritance Protocol comes - from. *} - -lemma cpreced_def2: - "cpreced wq s th \ Max ((\th'. preced th' s) ` ({th} \ dependants_raw wq th))" - unfolding cpreced_def image_def - apply(rule eq_reflection) - apply(rule_tac f="Max" in arg_cong) - by (auto) - -lemma cpreced_def3: - "cpreced wq s th \ Max (preceds ({th} \ dependants_raw wq th) s)" - unfolding cpreced_def2 image_def - apply(rule eq_reflection) - apply(rule_tac f="Max" in arg_cong) - by (auto) + "cpreced wq s th \ Max (preceds (subtree (tG_raw wq) th) s)" definition cpreceds :: "(cs \ thread list) \ state \ thread set \ precedence set" @@ -381,16 +353,18 @@ let new_wq = wq(cs := release (wq cs)) in (|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))" + lemma cpreced_initial: "cpreced (\ cs. []) [] = (\_. (Prc 0 0))" -apply(rule ext) -apply(simp add: cpreced_def) -apply(simp add: dependants_raw_def RAG_raw_def waiting_raw_def holding_raw_def) -apply(simp add: preced_def) -done +proof - + have [simp]: "(RAG_raw all_unlocked) = {}" + by (unfold RAG_raw_def, auto simp:waiting_raw_def holding_raw_def) + have [simp]: "\ x. (subtree {} x) = {x}" + by (unfold subtree_def, auto) + show ?thesis by (rule ext, auto simp:cpreced_def tG_raw_def preced_def) +qed text {* - \noindent The following @{text "wq"} is a shorthand for @{text "wq_fun"}. *} @@ -408,7 +382,7 @@ text {* \noindent Functions @{text "holding"}, @{text "waiting"}, @{text "RAG"} - and @{text "dependants"} still have the same meaning, but redefined so + and @{text "tG"} still have the same meaning, but redefined so that they no longer RAG on the fictitious {\em waiting queue function} @{text "wq"}, but on system state @{text "s"}. *} @@ -424,10 +398,6 @@ s_RAG_abv: "RAG (s::state) \ RAG_raw (wq s)" -definition - s_dependants_abv: - "dependants (s::state) \ dependants_raw (wq s)" - lemma cp_eq: shows "cp s th = cpreced (wq s) s th" unfolding cp_def wq_def @@ -465,11 +435,6 @@ "RAG_raw (wq s) = RAG s" by (unfold RAG_raw_def s_RAG_def, auto) - -lemma s_dependants_def: - shows "dependants (s::state) th \ {th' . (Th th', Th th) \ (RAG s)^+}" -using dependants_raw_def eq_RAG s_dependants_abv wq_def by auto - text {* The following function @{text "readys"} calculates the set of ready @@ -709,38 +674,25 @@ tRAG, so that it is easier to understand. *} - -definition "tG s = (map_prod the_thread the_thread) `(tRAG s)" +definition + s_tG_abv: + "tG (s::state) \ tG_raw (wq s)" lemma tG_alt_def: "tG s = {(th1, th2) | th1 th2. \ cs. (Th th1, Cs cs) \ RAG s \ (Cs cs, Th th2) \ RAG s}" (is "?L = ?R") + by (unfold s_tG_abv s_RAG_abv tG_raw_def, simp) + +lemma tRAG_def_tG: "tRAG s = (map_prod Th Th) ` (tG s)" + by (unfold tRAG_alt_def tG_alt_def, auto) + +lemma tG_def_tRAG: "tG s = map_prod the_thread the_thread ` tRAG s" proof - - { fix th1 th2 - assume "(th1, th2) \ ?L" - hence "(th1, th2) \ ?R" by (auto simp:tG_def tRAG_alt_def) - } moreover { - fix th1 th2 - assume "(th1, th2) \ ?R" - then obtain cs where "(Th th1, Cs cs) \ RAG s" "(Cs cs, Th th2) \ RAG s" by auto - hence "(Th th1, Th th2) \ (wRAG s O hRAG s)" by (auto simp:RAG_split wRAG_def hRAG_def) - hence "(Th th1, Th th2) \ tRAG s" by (unfold tRAG_def, simp) - hence "(th1, th2) \ ?L" by (simp add: tG_def rev_image_eqI) - } ultimately show ?thesis by (meson pred_equals_eq2) + have [simp]: "(map_prod the_thread the_thread \ map_prod Th Th) = id" + by (rule ext, auto) + show ?thesis by (unfold tRAG_def_tG image_comp, simp) qed -lemma tRAG_def_tG: "tRAG s = (map_prod Th Th) ` (tG s)" (is "?L = ?R") -proof - - have "?L = (\ x. x) ` ?L" by simp - also have "... = ?R" - proof(unfold tG_def image_comp, induct rule:image_cong) - case (2 e) - thus ?case by (unfold tRAG_alt_def, auto) - qed auto - finally show ?thesis . -qed - - fun actor where "actor (Exit th) = th" | "actor (P th cs) = th" |