--- a/CpsG.thy Fri Oct 30 20:40:11 2015 +0800
+++ b/CpsG.thy Thu Dec 03 14:34:00 2015 +0800
@@ -3,9 +3,47 @@
after every system call (or system operation)
*}
theory CpsG
-imports PrioG Max
+imports PrioG Max RTree
+begin
+
+locale pip =
+ fixes s
+ assumes vt: "vt s"
+
+context pip
begin
+interpretation rtree_RAG: rtree "RAG s"
+proof
+ show "single_valued (RAG s)"
+ apply (intro_locales)
+ by (unfold single_valued_def, auto intro: unique_RAG[OF vt])
+
+ show "acyclic (RAG s)"
+ by (rule acyclic_RAG[OF vt])
+qed
+
+end
+
+
+
+definition "the_preced s th = preced th s"
+
+lemma cp_alt_def:
+ "cp s th =
+ Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
+proof -
+ have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) =
+ Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})"
+ (is "Max (_ ` ?L) = Max (_ ` ?R)")
+ proof -
+ have "?L = ?R"
+ by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def)
+ thus ?thesis by simp
+ qed
+ thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)
+qed
+
lemma eq_dependants: "dependants (wq s) = dependants s"
by (simp add: s_dependants_abv wq_def)
@@ -575,9 +613,11 @@
qed
qed
+-- {* A useless definition *}
definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
where "cps s = {(th, cp s th) | th . th \<in> threads s}"
+
text {* (* ddd *)
One beauty of our modelling is that we follow the definitional extension tradition of HOL.
The benefit of such a concise and miniature model is that large number of intuitively
@@ -620,6 +660,27 @@
context step_set_cps
begin
+interpretation rtree_RAGs: rtree "RAG s"
+proof
+ show "single_valued (RAG s)"
+ apply (intro_locales)
+ by (unfold single_valued_def, auto intro: unique_RAG[OF vt_s])
+
+ show "acyclic (RAG s)"
+ by (rule acyclic_RAG[OF vt_s])
+qed
+
+interpretation rtree_RAGs': rtree "RAG s'"
+proof
+ show "single_valued (RAG s')"
+ apply (intro_locales)
+ by (unfold single_valued_def,
+ auto intro: unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
+
+ show "acyclic (RAG s')"
+ by (rule acyclic_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
+qed
+
text {* (* ddd *)
The following lemma confirms that @{text "Set"}-operating only changes the precedence
of initiating thread.
@@ -732,305 +793,73 @@
shows "cp s th' = cp s' th'"
by (rule eq_cp_pre[OF assms no_dependants])
-
-text {* (* ddd *) \noindent
- The following @{text "eq_up"} was originally designed to save the recalculations
- of current precedence going upstream from thread @{text "th"} can stop earlier.
- If at a certain point along way, the recalculation results in the same
- result, the recalculation can stop there.
- This lemma is obsolete because we found that @{text "th"} is not contained in
- any thread's dependants set.
+end
- The foregoing lemma says only those threads which
-*}
-lemma eq_up:
- fixes th' th''
- assumes dp1: "th \<in> dependants s th'"
- and dp2: "th' \<in> dependants s th''"
- and eq_cps: "cp s th' = cp s' th'"
- shows "cp s th'' = cp s' th''"
-proof -
- from dp2
- have "(Th th', Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def)
- from RAG_child[OF vt_s this[unfolded eq_RAG]]
- have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .
- moreover { fix n th''
- have "\<lbrakk>(Th th', n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
- (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
- proof(erule trancl_induct, auto)
- fix y th''
- assume y_ch: "(y, Th th'') \<in> child s"
- and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
- and ch': "(Th th', y) \<in> (child s)\<^sup>+"
- from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
- with ih have eq_cpy:"cp s thy = cp s' thy" by blast
- from dp1 have "(Th th, Th th') \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)
- moreover from child_RAG_p[OF ch'] and eq_y
- have "(Th th', Th thy) \<in> (RAG s)^+" by simp
- ultimately have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by auto
- show "cp s th'' = cp s' th''"
- apply (subst cp_rec[OF vt_s])
- proof -
- have "preced th'' s = preced th'' s'"
- proof(rule eq_preced)
- show "th'' \<noteq> th"
- proof
- assume "th'' = th"
- with dp_thy y_ch[unfolded eq_y]
- have "(Th th, Th th) \<in> (RAG s)^+"
- by (auto simp:child_def)
- with wf_trancl[OF wf_RAG[OF vt_s]]
- show False by auto
- qed
- qed
- moreover {
- fix th1
- assume th1_in: "th1 \<in> children s th''"
- have "cp s th1 = cp s' th1"
- proof(cases "th1 = thy")
- case True
- with eq_cpy show ?thesis by simp
- next
- case False
- have neq_th1: "th1 \<noteq> th"
- proof
- assume eq_th1: "th1 = th"
- with dp_thy have "(Th th1, Th thy) \<in> (RAG s)^+" by simp
- from children_no_dep[OF vt_s _ _ this] and
- th1_in y_ch eq_y show False by (auto simp:children_def)
- qed
- have "th \<notin> dependants s th1"
- proof
- assume h:"th \<in> dependants s th1"
- from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG)
- from dependants_child_unique[OF vt_s _ _ h this]
- th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
- with False show False by auto
- qed
- from eq_cp_pre[OF neq_th1 this]
- show ?thesis .
- qed
- }
- ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
- {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
- moreover have "children s th'' = children s' th''"
- by (unfold children_def child_def s_def RAG_set_unchanged, simp)
- ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
- by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
- qed
- next
- fix th''
- assume dp': "(Th th', Th th'') \<in> child s"
- show "cp s th'' = cp s' th''"
- apply (subst cp_rec[OF vt_s])
- proof -
- have "preced th'' s = preced th'' s'"
- proof(rule eq_preced)
- show "th'' \<noteq> th"
- proof
- assume "th'' = th"
- with dp1 dp'
- have "(Th th, Th th) \<in> (RAG s)^+"
- by (auto simp:child_def s_dependants_def eq_RAG)
- with wf_trancl[OF wf_RAG[OF vt_s]]
- show False by auto
- qed
- qed
- moreover {
- fix th1
- assume th1_in: "th1 \<in> children s th''"
- have "cp s th1 = cp s' th1"
- proof(cases "th1 = th'")
- case True
- with eq_cps show ?thesis by simp
- next
- case False
- have neq_th1: "th1 \<noteq> th"
- proof
- assume eq_th1: "th1 = th"
- with dp1 have "(Th th1, Th th') \<in> (RAG s)^+"
- by (auto simp:s_dependants_def eq_RAG)
- from children_no_dep[OF vt_s _ _ this]
- th1_in dp'
- show False by (auto simp:children_def)
- qed
- thus ?thesis
- proof(rule eq_cp_pre)
- show "th \<notin> dependants s th1"
- proof
- assume "th \<in> dependants s th1"
- from dependants_child_unique[OF vt_s _ _ this dp1]
- th1_in dp' have "th1 = th'"
- by (auto simp:children_def)
- with False show False by auto
- qed
- qed
- qed
- }
- ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
- {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
- moreover have "children s th'' = children s' th''"
- by (unfold children_def child_def s_def RAG_set_unchanged, simp)
- ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
- by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
- qed
- qed
- }
- ultimately show ?thesis by auto
-qed
-
-text {* (* ddd *)
- For those @{text "th''"}, @{text "th \<in> dependants s th''"} means that
- the current precedence of such @{text "th''"} might possibly be boosted if the
- current precedence of @{text "th"} somehow get raised. The following lemma
- says that if the resetting of its own priority by thread @{text "th"} does not
- change its current precedence, then the current precedence of such @{text "th''"}
- will remain unchanged. The situation such that @{text "th"}'s current
- precedence does not change with the resetting of its priority might happen in many
- different cases. For example, if the current precedence of @{text "th"} is already an inherited one,
- the lowering of its priority will not change its current precedence, and the increasing
- of its priority will not change its current precedence neither, if
- incidental rising of its own precedence is not large enough to surpass the inherited precedence.
+text {*
+ The following @{text "step_v_cps"} is the locale for @{text "V"}-operation.
*}
-lemma eq_up_self:
- fixes th' th''
- assumes dp: "th \<in> dependants s th''"
- and eq_cps: "cp s th = cp s' th"
- shows "cp s th'' = cp s' th''"
-proof -
- from dp
- have "(Th th, Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def)
- from RAG_child[OF vt_s this[unfolded eq_RAG]]
- have ch_th': "(Th th, Th th'') \<in> (child s)\<^sup>+" .
- moreover { fix n th''
- have "\<lbrakk>(Th th, n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
- (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
- proof(erule trancl_induct, auto)
- fix y th''
- assume y_ch: "(y, Th th'') \<in> child s"
- and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
- and ch': "(Th th, y) \<in> (child s)\<^sup>+"
- from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
- with ih have eq_cpy:"cp s thy = cp s' thy" by blast
- from child_RAG_p[OF ch'] and eq_y
- have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by simp
- show "cp s th'' = cp s' th''"
- apply (subst cp_rec[OF vt_s])
- proof -
- have "preced th'' s = preced th'' s'"
- proof(rule eq_preced)
- show "th'' \<noteq> th"
- proof
- assume "th'' = th"
- with dp_thy y_ch[unfolded eq_y]
- have "(Th th, Th th) \<in> (RAG s)^+"
- by (auto simp:child_def)
- with wf_trancl[OF wf_RAG[OF vt_s]]
- show False by auto
- qed
- qed
- moreover {
- fix th1
- assume th1_in: "th1 \<in> children s th''"
- have "cp s th1 = cp s' th1"
- proof(cases "th1 = thy")
- case True
- with eq_cpy show ?thesis by simp
- next
- case False
- have neq_th1: "th1 \<noteq> th"
- proof
- assume eq_th1: "th1 = th"
- with dp_thy have "(Th th1, Th thy) \<in> (RAG s)^+" by simp
- from children_no_dep[OF vt_s _ _ this] and
- th1_in y_ch eq_y show False by (auto simp:children_def)
- qed
- have "th \<notin> dependants s th1"
- proof
- assume h:"th \<in> dependants s th1"
- from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG)
- from dependants_child_unique[OF vt_s _ _ h this]
- th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
- with False show False by auto
- qed
- from eq_cp_pre[OF neq_th1 this]
- show ?thesis .
- qed
- }
- ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
- {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
- moreover have "children s th'' = children s' th''"
- by (unfold children_def child_def s_def RAG_set_unchanged, simp)
- ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
- by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
- qed
- next
- fix th''
- assume dp': "(Th th, Th th'') \<in> child s"
- show "cp s th'' = cp s' th''"
- apply (subst cp_rec[OF vt_s])
- proof -
- have "preced th'' s = preced th'' s'"
- proof(rule eq_preced)
- show "th'' \<noteq> th"
- proof
- assume "th'' = th"
- with dp dp'
- have "(Th th, Th th) \<in> (RAG s)^+"
- by (auto simp:child_def s_dependants_def eq_RAG)
- with wf_trancl[OF wf_RAG[OF vt_s]]
- show False by auto
- qed
- qed
- moreover {
- fix th1
- assume th1_in: "th1 \<in> children s th''"
- have "cp s th1 = cp s' th1"
- proof(cases "th1 = th")
- case True
- with eq_cps show ?thesis by simp
- next
- case False
- assume neq_th1: "th1 \<noteq> th"
- thus ?thesis
- proof(rule eq_cp_pre)
- show "th \<notin> dependants s th1"
- proof
- assume "th \<in> dependants s th1"
- hence "(Th th, Th th1) \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)
- from children_no_dep[OF vt_s _ _ this]
- and th1_in dp' show False
- by (auto simp:children_def)
- qed
- qed
- qed
- }
- ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
- {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
- moreover have "children s th'' = children s' th''"
- by (unfold children_def child_def s_def RAG_set_unchanged, simp)
- ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
- by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
- qed
- qed
- }
- ultimately show ?thesis by auto
-qed
-end
-
locale step_v_cps =
- fixes s' th cs s
- defines s_def : "s \<equiv> (V th cs#s')"
+ -- {* @{text "th"} is the initiating thread *}
+ -- {* @{text "cs"} is the critical resource release by the @{text "V"}-operation *}
+ fixes s' th cs s -- {* @{text "s'"} is the state before operation*}
+ defines s_def : "s \<equiv> (V th cs#s')" -- {* @{text "s"} is the state after operation*}
+ -- {* @{text "s"} is assumed to be valid, which implies the validity of @{text "s'"} *}
assumes vt_s: "vt s"
+text {*
+ The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation,
+ which represents the case when there is another thread @{text "th'"}
+ to take over the critical resource released by the initiating thread @{text "th"}.
+*}
locale step_v_cps_nt = step_v_cps +
fixes th'
- assumes nt: "next_th s' th cs th'"
+ -- {* @{text "th'"} is assumed to take over @{text "cs"} *}
+ assumes nt: "next_th s' th cs th'"
context step_v_cps_nt
begin
+text {*
+ Lemma @{text "RAG_s"} confirms the change of RAG:
+ two edges removed and one added, as shown by the following diagram.
+*}
+
+(*
+ RAG before the V-operation
+ th1 ----|
+ |
+ th' ----|
+ |----> cs -----|
+ th2 ----| |
+ | |
+ th3 ----| |
+ |------> th
+ th4 ----| |
+ | |
+ th5 ----| |
+ |----> cs'-----|
+ th6 ----|
+ |
+ th7 ----|
+
+ RAG after the V-operation
+ th1 ----|
+ |
+ |----> cs ----> th'
+ th2 ----|
+ |
+ th3 ----|
+
+ th4 ----|
+ |
+ th5 ----|
+ |----> cs'----> th
+ th6 ----|
+ |
+ th7 ----|
+*)
+
lemma RAG_s:
"RAG s = (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union>
{(Cs cs, Th th')}"
@@ -1039,12 +868,16 @@
and nt show ?thesis by (auto intro:next_th_unique)
qed
+text {*
+ Lemma @{text "dependants_kept"} shows only @{text "th"} and @{text "th'"}
+ have their dependants changed.
+*}
lemma dependants_kept:
fixes th''
assumes neq1: "th'' \<noteq> th"
and neq2: "th'' \<noteq> th'"
shows "dependants (wq s) th'' = dependants (wq s') th''"
-proof(auto)
+proof(auto) (* ccc *)
fix x
assume "x \<in> dependants (wq s) th''"
hence dp: "(Th x, Th th'') \<in> (RAG s)^+"
@@ -1529,6 +1362,7 @@
show ?thesis by (simp add:s_def)
qed
+
lemma eq_child_left:
assumes nd: "(Th th, Th th') \<notin> (child s)^+"
shows "(n1, Th th') \<in> (child s)^+ \<Longrightarrow> (n1, Th th') \<in> (child s')^+"