--- a/PIPBasics.thy Tue Aug 16 11:49:37 2016 +0100
+++ b/PIPBasics.thy Wed Aug 24 16:13:20 2016 +0200
@@ -920,6 +920,8 @@
"dependants s th = {th'. th \<in> ancestors (tG s) th'}"
by (unfold dependants_alt_tG ancestors_def, simp)
+
+
section {* Locales used to investigate the execution of PIP *}
text {*
@@ -3459,6 +3461,36 @@
qed
qed
+lemma root_readys:
+ assumes "th \<in> readys s"
+ shows "root (tRAG s) (Th th)"
+proof -
+ { assume "\<not> root (tRAG s) (Th th)"
+ then obtain n' where "(Th th, n') \<in> (tRAG s)^+"
+ unfolding root_def ancestors_def by auto
+ then obtain cs where "(Th th, Cs cs) \<in> RAG s"
+ unfolding tRAG_alt_def using tranclD by fastforce
+ then have "th \<notin> readys s"
+ unfolding readys_def using in_RAG_E by blast
+ with assms have False by simp
+ } then show "root (tRAG s) (Th th)" by auto
+qed
+
+lemma root_readys_tG:
+ assumes "th \<in> readys s"
+ shows "root (tG s) th"
+proof -
+ { assume "\<not> root (tG s) th"
+ then obtain th' where "(th, th') \<in> (tG s)^+"
+ unfolding root_def ancestors_def by auto
+ then have "(Th th, Th th') \<in> (tRAG s)^+"
+ using trancl_tG_tRAG by simp
+ with root_readys assms
+ have False
+ unfolding root_def ancestors_def by auto
+ } then show "root (tG s) th" by auto
+qed
+
lemma readys_indep:
assumes "th1 \<in> readys s"
and "th2 \<in> readys s"
@@ -3509,191 +3541,67 @@
The following two lemmas shows there is at most one running thread
in the system.
*}
+
+
lemma running_unique:
assumes running_1: "th1 \<in> running s"
and running_2: "th2 \<in> running s"
shows "th1 = th2"
proof -
- -- {* According to lemma @{thm thread_chain},
- each living threads is chained to a thread in its subtree, and this
- target thread holds the highest precedence of the subtree.
-
- The chains for @{term th1} and @{term th2} are established
- first in the following in @{text "h1"} and @{text "h2"}:
- *}
+ -- {*
+
+ According to lemma @{thm thread_chain}, each live thread is chained to a
+ thread in its subtree, who holds the highest precedence of the subtree.
+
+ The chains for @{term th1} and @{term th2} are established first in the
+ following in @{text "chain1"} and @{text "chain2"}. These chains start
+ with the threads @{text "th1'"} and @{text "th2'"} respectively. *}
+
have "th1 \<in> threads s" using assms
by (unfold running_def readys_def, auto)
- from thread_chain[OF this]
+ with thread_chain
obtain th1' where
- h1: "th1' \<in> subtree (tG s) th1"
+ chain1: "th1' \<in> subtree (tG s) th1"
"the_preced s th1' = Max (the_preced s ` subtree (tG s) th1)"
"th1' \<in> threads s"
by auto
have "th2 \<in> threads s" using assms
by (unfold running_def readys_def, auto)
- from thread_chain[OF this]
+ with thread_chain
obtain th2' where
- h2: "th2' \<in> subtree (tG s) th2"
+ chain2: "th2' \<in> subtree (tG s) th2"
"the_preced s th2' = Max (the_preced s ` subtree (tG s) th2)"
"th2' \<in> threads s"
by auto
- -- {* It can be proved that the chained thread for @{term th1} and @{term th2}
- must be equal:
+ -- {* From these two chains we can be prove that the threads
+ @{term th1} and @{term th2} must be equal. For this we first
+ show that the starting points of the chains are equal.
*}
have eq_th': "th1' = th2'"
proof -
- have "the_preced s th1' = the_preced s th2'"
- proof -
- from running_1 and running_2 have "cp s th1 = cp s th2"
- unfolding running_def by auto
- from this[unfolded cp_alt_def2]
- have eq_max: "Max (the_preced s ` subtree (tG s) th1) =
- Max (the_preced s ` subtree (tG s) th2)" .
- with h1(2) h2(2)
- show ?thesis by metis
- qed
- from preced_unique[OF this[unfolded the_preced_def] h1(3) h2(3)]
- show ?thesis .
- qed
- -- {* From this, it can be derived that the two sub-trees
- rooted by @{term th1} and @{term th2} must overlap: *}
- have overlapping: "th1' \<in> subtree (tG s) th1 \<inter> subtree (tG s) th2"
- using eq_th' h1(1) h2(1) by auto
- -- {* However, this would be in contradiction with the fact
- that two independent sub-trees can not overlap,
- if @{term "th1 \<noteq> th2"} (therefore, each roots an independent sub-trees).
- Therefore, @{term th1} and @{term th2} must be equal.
- *}
- { assume neq: "th1 \<noteq> th2"
- -- {* According to @{thm readys_indep_tG}, two different threads
- in ready queue must be independent with each other: *}
- have "indep (tG s) th1 th2"
- by (rule readys_indep_tG[OF _ _ neq], insert assms, auto simp:running_def)
- -- {* Therefore, according to lemma @{thm subtree_disjoint},
- the two sub-trees rooted by them can not overlap:
- *}
- from subtree_disjoint[OF this]
- have "subtree (tG s) th1 \<inter> subtree (tG s) th2 = {}" .
- -- {* In contradiction with @{thm overlapping}: *}
- with overlapping have False by auto
- } thus ?thesis by auto
-qed
-
-text {*
- The following two lemmas shows there is at most one running thread
- in the system.
-*}
-lemma running_unique_old:
- assumes running_1: "th1 \<in> running s"
- and running_2: "th2 \<in> running s"
- shows "th1 = th2"
-proof -
- from running_1 and running_2 have "cp s th1 = cp s th2"
- unfolding running_def by auto
- from this[unfolded cp_alt_def]
- have eq_max:
- "Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th1)}) =
- Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th2)})"
- (is "Max ?L = Max ?R") .
- have "Max ?L \<in> ?L"
- proof(rule Max_in)
- show "finite ?L" by (simp add: finite_subtree_threads)
- next
- show "?L \<noteq> {}" using subtree_def by fastforce
- qed
- then obtain th1' where
- h_1: "Th th1' \<in> subtree (RAG s) (Th th1)" "the_preced s th1' = Max ?L"
- by auto
- have "Max ?R \<in> ?R"
- proof(rule Max_in)
- show "finite ?R" by (simp add: finite_subtree_threads)
- next
- show "?R \<noteq> {}" using subtree_def by fastforce
+ -- {* from @{text th1} and @{text th2} running, we know their
+ cp-value is the same *}
+ from running_1 and running_2 have "cp s th1 = cp s th2"
+ unfolding running_def by auto
+ -- {* that means the preced of @{text th1'} and @{text th2'}
+ must be the same *}
+ then
+ have eq_max: "Max (the_preced s ` subtree (tG s) th1) =
+ Max (the_preced s ` subtree (tG s) th2)"
+ unfolding cp_alt_def2 .
+ with chain1(2) chain2(2)
+ have "the_preced s th1' = the_preced s th2'" by simp
+ -- {* since the precedences are the same, we can conclude
+ that @{text th1'} and @{text th2'} are the same *}
+ with preced_unique chain1(3) chain2(3)
+ show "th1' = th2'" unfolding the_preced_def by auto
qed
- then obtain th2' where
- h_2: "Th th2' \<in> subtree (RAG s) (Th th2)" "the_preced s th2' = Max ?R"
- by auto
- have "th1' = th2'"
- proof(rule preced_unique)
- from h_1(1)
- show "th1' \<in> threads s"
- proof(cases rule:subtreeE)
- case 1
- hence "th1' = th1" by simp
- with running_1 show ?thesis by (auto simp:running_def readys_def)
- next
- case 2
- from this(2)
- have "(Th th1', Th th1) \<in> (RAG s)^+" by (auto simp:ancestors_def)
- from tranclD[OF this]
- have "(Th th1') \<in> Domain (RAG s)" by auto
- from dm_RAG_threads[OF this] show ?thesis .
- qed
- next
- from h_2(1)
- show "th2' \<in> threads s"
- proof(cases rule:subtreeE)
- case 1
- hence "th2' = th2" by simp
- with running_2 show ?thesis by (auto simp:running_def readys_def)
- next
- case 2
- from this(2)
- have "(Th th2', Th th2) \<in> (RAG s)^+" by (auto simp:ancestors_def)
- from tranclD[OF this]
- have "(Th th2') \<in> Domain (RAG s)" by auto
- from dm_RAG_threads[OF this] show ?thesis .
- qed
- next
- have "the_preced s th1' = the_preced s th2'"
- using eq_max h_1(2) h_2(2) by metis
- thus "preced th1' s = preced th2' s" by (simp add:the_preced_def)
- qed
- from h_1(1)[unfolded this]
- have star1: "(Th th2', Th th1) \<in> (RAG s)^*" by (auto simp:subtree_def)
- from h_2(1)[unfolded this]
- have star2: "(Th th2', Th th2) \<in> (RAG s)^*" by (auto simp:subtree_def)
- from star_rpath[OF star1] obtain xs1
- where rp1: "rpath (RAG s) (Th th2') xs1 (Th th1)"
- by auto
- from star_rpath[OF star2] obtain xs2
- where rp2: "rpath (RAG s) (Th th2') xs2 (Th th2)"
- by auto
- from rp1 rp2
- show ?thesis
- proof(cases)
- case (less_1 xs')
- moreover have "xs' = []"
- proof(rule ccontr)
- assume otherwise: "xs' \<noteq> []"
- from rpath_plus[OF less_1(3) this]
- have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+" .
- from tranclD[OF this]
- obtain cs where "waiting s th1 cs"
- by (unfold s_RAG_def, fold s_waiting_abv, auto)
- with running_1 show False
- by (unfold running_def readys_def, auto)
- qed
- ultimately have "xs2 = xs1" by simp
- from rpath_dest_eq[OF rp1 rp2[unfolded this]]
- show ?thesis by simp
- next
- case (less_2 xs')
- moreover have "xs' = []"
- proof(rule ccontr)
- assume otherwise: "xs' \<noteq> []"
- from rpath_plus[OF less_2(3) this]
- have "(Th th2, Th th1) \<in> (RAG s)\<^sup>+" .
- from tranclD[OF this]
- obtain cs where "waiting s th2 cs"
- by (unfold s_RAG_def, fold s_waiting_abv, auto)
- with running_2 show False
- by (unfold running_def readys_def, auto)
- qed
- ultimately have "xs2 = xs1" by simp
- from rpath_dest_eq[OF rp1 rp2[unfolded this]]
- show ?thesis by simp
- qed
+ moreover
+ have "root (tG s) th1" "root (tG s) th2" using assms
+ using assms root_readys_tG
+ unfolding running_def by auto
+ ultimately show "th1 = th2" using root_unique chain1(1) chain2(1)
+ by fastforce
qed
lemma card_running: