# HG changeset patch # User zhangx # Date 1455028243 -28800 # Node ID 81c6ede5cd11a78bcb8cdd48793e5d410c8a2855 # Parent ce85c3c4e5bfdd3ebad1bed3dec5625e07f57a13 More refinements in PIPBasics.thy. diff -r ce85c3c4e5bf -r 81c6ede5cd11 PIPBasics.thy --- a/PIPBasics.thy Mon Feb 08 10:57:01 2016 +0800 +++ b/PIPBasics.thy Tue Feb 09 22:30:43 2016 +0800 @@ -2951,9 +2951,19 @@ section {* Chain to readys *} +text {* + In this section, a more complete view of @{term RAG} and @{term threads} + are given. +*} + context valid_trace begin +text {* + The first lemma is technical, which says out of any node in the domain + of @{term RAG}, there is a path leading to a ready thread. +*} + lemma chain_building: assumes "node \ Domain (RAG s)" obtains th' where "th' \ readys s" "(node, Th th') \ (RAG s)^+" @@ -2998,7 +3008,10 @@ qed text {* \noindent - The following lemma is proved easily by instantiating @{thm "chain_building"}. + The following lemma says for any living thread, + either it is ready or there is a path in @{term RAG} + leading from it to a ready thread. The lemma is proved easily + by instantiating @{thm "chain_building"}. *} lemma th_chain_to_ready: assumes th_in: "th \ threads s" @@ -3014,6 +3027,11 @@ show ?thesis by auto qed +text {* + The following lemma is a technical one to show + that the set of threads in the subtree of any thread + is finite. +*} lemma finite_subtree_threads: "finite {th'. Th th' \ subtree (RAG s) (Th th)}" (is "finite ?A") proof - @@ -3031,6 +3049,10 @@ ultimately show ?thesis by auto qed +text {* + The following two lemmas shows there is at most one running thread + in the system. +*} lemma runing_unique: assumes runing_1: "th1 \ runing s" and runing_2: "th2 \ runing s" @@ -3156,14 +3178,117 @@ thus ?thesis by auto qed +text {* + The following two lemmas show that the set of living threads + in the system can be partitioned into subtrees of those + threads in the @{term readys} set. The first lemma + @{text threads_alt_def} shows the union of + these subtrees equals to the set of living threads + and the second lemma @{text "readys_subtree_disjoint"} shows + subtrees of different threads in @{term readys}-set + are disjoint. +*} + +lemma threads_alt_def: + "(threads s) = (\ th \ readys s. {th'. Th th' \ subtree (RAG s) (Th th)})" + (is "?L = ?R") +proof - + { fix th1 + assume "th1 \ ?L" + from th_chain_to_ready[OF this] + have "th1 \ readys s \ (\th'. th' \ readys s \ (Th th1, Th th') \ (RAG s)\<^sup>+)" . + hence "th1 \ ?R" by (auto simp:subtree_def) + } moreover + { fix th' + assume "th' \ ?R" + then obtain th where h: "th \ readys s" " Th th' \ subtree (RAG s) (Th th)" + by auto + from this(2) + have "th' \ ?L" + proof(cases rule:subtreeE) + case 1 + with h(1) show ?thesis by (auto simp:readys_def) + next + case 2 + from tranclD[OF this(2)[unfolded ancestors_def, simplified]] + have "Th th' \ Domain (RAG s)" by auto + from dm_RAG_threads[OF this] + show ?thesis . + qed + } ultimately show ?thesis by auto +qed + +lemma readys_subtree_disjoint: + assumes "th1 \ readys s" + and "th2 \ readys s" + and "th1 \ th2" + shows "subtree (RAG s) (Th th1) \ subtree (RAG s) (Th th2) = {}" +proof - + { fix n + assume "n \ subtree (RAG s) (Th th1) \ subtree (RAG s) (Th th2)" + hence "(n, Th th1) \ (RAG s)^*" "(n, Th th2) \ (RAG s)^*" + by (auto simp:subtree_def) + from star_rpath[OF this(1)] star_rpath[OF this(2)] + obtain xs1 xs2 where "rpath (RAG s) n xs1 (Th th1)" + "rpath (RAG s) n xs2 (Th th2)" by metis + hence False + proof(cases rule:rtree_RAG.rpath_overlap') + case (less_1 xs3) + from rpath_star[OF this(3)] + have "Th th1 \ subtree (RAG s) (Th th2)" + by (auto simp:subtree_def) + thus ?thesis + proof(cases rule:subtreeE) + case 1 + with assms(3) show ?thesis by auto + next + case 2 + hence "(Th th1, Th th2) \ (RAG s)^+" by (auto simp:ancestors_def) + from tranclD[OF this] + obtain z where "(Th th1, z) \ RAG s" by auto + from this[unfolded s_RAG_def, folded wq_def] + obtain cs' where "waiting s th1 cs'" + by (auto simp:waiting_eq) + with assms(1) show False by (auto simp:readys_def) + qed + next + case (less_2 xs3) + from rpath_star[OF this(3)] + have "Th th2 \ subtree (RAG s) (Th th1)" + by (auto simp:subtree_def) + thus ?thesis + proof(cases rule:subtreeE) + case 1 + with assms(3) show ?thesis by auto + next + case 2 + hence "(Th th2, Th th1) \ (RAG s)^+" by (auto simp:ancestors_def) + from tranclD[OF this] + obtain z where "(Th th2, z) \ RAG s" by auto + from this[unfolded s_RAG_def, folded wq_def] + obtain cs' where "waiting s th2 cs'" + by (auto simp:waiting_eq) + with assms(2) show False by (auto simp:readys_def) + qed + qed + } thus ?thesis by auto +qed + end - +(* ccc *) section {* Relating @{term cp} and @{term the_preced} and @{term preced} *} context valid_trace begin +lemma finite_threads: + shows "finite (threads s)" + using vt by (induct) (auto elim: step.cases) + +lemma finite_readys: "finite (readys s)" + using finite_threads readys_threads rev_finite_subset by blast + lemma le_cp: shows "preced th s \ cp s th" proof(unfold cp_alt_def, rule Max_ge) @@ -3174,10 +3299,6 @@ by (simp add: subtree_def the_preced_def) qed -lemma finite_threads: - shows "finite (threads s)" - using vt by (induct) (auto elim: step.cases) - lemma cp_le: assumes th_in: "th \ threads s" shows "cp s th \ Max (the_preced s ` threads s)" @@ -3212,39 +3333,7 @@ ultimately show ?thesis by auto qed -lemma threads_alt_def: - "(threads s) = (\ th \ readys s. {th'. Th th' \ subtree (RAG s) (Th th)})" - (is "?L = ?R") -proof - - { fix th1 - assume "th1 \ ?L" - from th_chain_to_ready[OF this] - have "th1 \ readys s \ (\th'. th' \ readys s \ (Th th1, Th th') \ (RAG s)\<^sup>+)" . - hence "th1 \ ?R" by (auto simp:subtree_def) - } moreover - { fix th' - assume "th' \ ?R" - then obtain th where h: "th \ readys s" " Th th' \ subtree (RAG s) (Th th)" - by auto - from this(2) - have "th' \ ?L" - proof(cases rule:subtreeE) - case 1 - with h(1) show ?thesis by (auto simp:readys_def) - next - case 2 - from tranclD[OF this(2)[unfolded ancestors_def, simplified]] - have "Th th' \ Domain (RAG s)" by auto - from dm_RAG_threads[OF this] - show ?thesis . - qed - } ultimately show ?thesis by auto -qed - -lemma finite_readys: "finite (readys s)" - using finite_threads readys_threads rev_finite_subset by blast - -text {* (* ccc *) \noindent +text {* (* ddd *) \noindent Since the current precedence of the threads in ready queue will always be boosted, there must be one inside it has the maximum precedence of the whole system. *}