--- 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 \<Rightarrow> thread list) \<Rightarrow> thread \<Rightarrow> thread set"
-where
- "dependants_raw wq th \<equiv> {th' . (Th th', Th th) \<in> (RAG_raw wq)^+}"
+ "tG_raw wq = {(th\<^sub>1, th\<^sub>2) | th\<^sub>1 th\<^sub>2.
+ \<exists> cs. (Th th\<^sub>1, Cs cs) \<in> RAG_raw wq \<and> (Cs cs, Th th\<^sub>2) \<in> 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 \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"
where
- "cpreced wq s th \<equiv> Max ({preced th s} \<union> 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 \<equiv> Max ((\<lambda>th'. preced th' s) ` ({th} \<union> 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 \<equiv> Max (preceds ({th} \<union> 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 \<equiv> Max (preceds (subtree (tG_raw wq) th) s)"
definition
cpreceds :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread set \<Rightarrow> 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 (\<lambda> cs. []) [] = (\<lambda>_. (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]: "\<forall> 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) \<equiv> RAG_raw (wq s)"
-definition
- s_dependants_abv:
- "dependants (s::state) \<equiv> 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 \<equiv> {th' . (Th th', Th th) \<in> (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) \<equiv> tG_raw (wq s)"
lemma tG_alt_def:
"tG s = {(th1, th2) | th1 th2.
\<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> 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) \<in> ?L"
- hence "(th1, th2) \<in> ?R" by (auto simp:tG_def tRAG_alt_def)
- } moreover {
- fix th1 th2
- assume "(th1, th2) \<in> ?R"
- then obtain cs where "(Th th1, Cs cs) \<in> RAG s" "(Cs cs, Th th2) \<in> RAG s" by auto
- hence "(Th th1, Th th2) \<in> (wRAG s O hRAG s)" by (auto simp:RAG_split wRAG_def hRAG_def)
- hence "(Th th1, Th th2) \<in> tRAG s" by (unfold tRAG_def, simp)
- hence "(th1, th2) \<in> ?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 \<circ> 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 = (\<lambda> 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" |