diff -r fb3f52fe99d1 -r 785c0f6b8184 PIPBasics.thy --- 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 \ 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 \ readys s" + shows "root (tRAG s) (Th th)" +proof - + { assume "\ root (tRAG s) (Th th)" + then obtain n' where "(Th th, n') \ (tRAG s)^+" + unfolding root_def ancestors_def by auto + then obtain cs where "(Th th, Cs cs) \ RAG s" + unfolding tRAG_alt_def using tranclD by fastforce + then have "th \ 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 \ readys s" + shows "root (tG s) th" +proof - + { assume "\ root (tG s) th" + then obtain th' where "(th, th') \ (tG s)^+" + unfolding root_def ancestors_def by auto + then have "(Th th, Th th') \ (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 \ readys s" and "th2 \ 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 \ running s" and running_2: "th2 \ 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 \ threads s" using assms by (unfold running_def readys_def, auto) - from thread_chain[OF this] + with thread_chain obtain th1' where - h1: "th1' \ subtree (tG s) th1" + chain1: "th1' \ subtree (tG s) th1" "the_preced s th1' = Max (the_preced s ` subtree (tG s) th1)" "th1' \ threads s" by auto have "th2 \ threads s" using assms by (unfold running_def readys_def, auto) - from thread_chain[OF this] + with thread_chain obtain th2' where - h2: "th2' \ subtree (tG s) th2" + chain2: "th2' \ subtree (tG s) th2" "the_preced s th2' = Max (the_preced s ` subtree (tG s) th2)" "th2' \ 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' \ subtree (tG s) th1 \ 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 \ th2"} (therefore, each roots an independent sub-trees). - Therefore, @{term th1} and @{term th2} must be equal. - *} - { assume neq: "th1 \ 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 \ 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 \ running s" - and running_2: "th2 \ 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' \ subtree (RAG s) (Th th1)}) = - Max (the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th2)})" - (is "Max ?L = Max ?R") . - have "Max ?L \ ?L" - proof(rule Max_in) - show "finite ?L" by (simp add: finite_subtree_threads) - next - show "?L \ {}" using subtree_def by fastforce - qed - then obtain th1' where - h_1: "Th th1' \ subtree (RAG s) (Th th1)" "the_preced s th1' = Max ?L" - by auto - have "Max ?R \ ?R" - proof(rule Max_in) - show "finite ?R" by (simp add: finite_subtree_threads) - next - show "?R \ {}" 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' \ 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' \ 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) \ (RAG s)^+" by (auto simp:ancestors_def) - from tranclD[OF this] - have "(Th th1') \ Domain (RAG s)" by auto - from dm_RAG_threads[OF this] show ?thesis . - qed - next - from h_2(1) - show "th2' \ 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) \ (RAG s)^+" by (auto simp:ancestors_def) - from tranclD[OF this] - have "(Th th2') \ 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) \ (RAG s)^*" by (auto simp:subtree_def) - from h_2(1)[unfolded this] - have star2: "(Th th2', Th th2) \ (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' \ []" - from rpath_plus[OF less_1(3) this] - have "(Th th1, Th th2) \ (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' \ []" - from rpath_plus[OF less_2(3) this] - have "(Th th2, Th th1) \ (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: