# HG changeset patch # User zhangx # Date 1453986857 -28800 # Node ID ed938e2246b9bacb4ce92250a483329605635c5c # Parent 2056d9f481e215cafb42d476eb184f58e8af49ff Retrofiting of: CpsG.thy (the parallel copy of PIPBasics.thy), ExtGG.thy (The paralell copy of Implemenation.thy), PrioG.thy (The paralell copy of Correctness.thy) has completed. The next step is to overwite original copies with the paralell ones. diff -r 2056d9f481e2 -r ed938e2246b9 CpsG.thy --- a/CpsG.thy Thu Jan 28 16:36:46 2016 +0800 +++ b/CpsG.thy Thu Jan 28 21:14:17 2016 +0800 @@ -84,6 +84,30 @@ finally show ?thesis by simp qed +lemma birth_time_lt: + assumes "s \ []" + shows "last_set th s < length s" + using assms +proof(induct s) + case (Cons a s) + show ?case + proof(cases "s \ []") + case False + thus ?thesis + by (cases a, auto) + next + case True + show ?thesis using Cons(1)[OF True] + by (cases a, auto) + qed +qed simp + +lemma th_in_ne: "th \ threads s \ s \ []" + by (induct s, auto) + +lemma preced_tm_lt: "th \ threads s \ preced th s = Prc x y \ y < length s" + by (drule_tac th_in_ne, unfold preced_def, auto intro: birth_time_lt) + lemma eq_RAG: "RAG (wq s) = RAG s" by (unfold cs_RAG_def s_RAG_def, auto) @@ -2245,10 +2269,6 @@ ultimately show ?thesis by auto qed -lemma max_cp_eq_the_preced: - shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)" - using max_cp_eq using the_preced_def by presburger - lemma wf_RAG_converse: shows "wf ((RAG s)^-1)" proof(rule finite_acyclic_wf_converse) @@ -4444,5 +4464,85 @@ shows "th1 = th2" using assms by (unfold next_th_def, auto) +context valid_trace +begin + +thm th_chain_to_ready + +find_theorems subtree Th RAG + +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 [simp]: "finite (readys s)" + using finite_threads readys_threads rev_finite_subset by blast + +text {* (* ccc *) \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. +*} +lemma max_cp_readys_threads: + shows "Max (cp s ` readys s) = Max (cp s ` threads s)" (is "?L = ?R") +proof(cases "readys s = {}") + case False + have "?R = Max (the_preced s ` threads s)" by (unfold max_cp_eq, simp) + also have "... = + Max (the_preced s ` (\th\readys s. {th'. Th th' \ subtree (RAG s) (Th th)}))" + by (unfold threads_alt_def, simp) + also have "... = + Max ((\th\readys s. the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)}))" + by (unfold image_UN, simp) + also have "... = + Max (Max ` (\th. the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)}) ` readys s)" + proof(rule Max_UNION) + show "\M\(\x. the_preced s ` + {th'. Th th' \ subtree (RAG s) (Th x)}) ` readys s. finite M" + using finite_subtree_threads by auto + qed (auto simp:False subtree_def) + also have "... = + Max ((Max \ (\th. the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)})) ` readys s)" + by (unfold image_comp, simp) + also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)") + proof - + have "(?f ` ?A) = (?g ` ?A)" + proof(rule f_image_eq) + fix th1 + assume "th1 \ ?A" + thus "?f th1 = ?g th1" + by (unfold cp_alt_def, simp) + qed + thus ?thesis by simp + qed + finally show ?thesis by simp +qed (auto simp:threads_alt_def) + end +end + diff -r 2056d9f481e2 -r ed938e2246b9 CpsG.thy~ --- a/CpsG.thy~ Thu Jan 28 16:36:46 2016 +0800 +++ b/CpsG.thy~ Thu Jan 28 21:14:17 2016 +0800 @@ -2,6 +2,17 @@ imports PIPDefs begin +lemma f_image_eq: + assumes h: "\ a. a \ A \ f a = g a" + shows "f ` A = g ` A" +proof + show "f ` A \ g ` A" + by(rule image_subsetI, auto intro:h) +next + show "g ` A \ f ` A" + by (rule image_subsetI, auto intro:h[symmetric]) +qed + lemma Max_fg_mono: assumes "finite A" and "\ a \ A. f a \ g a" @@ -46,6 +57,57 @@ from fnt and seq show "finite (f ` B)" by auto qed +lemma Max_UNION: + assumes "finite A" + and "A \ {}" + and "\ M \ f ` A. finite M" + and "\ M \ f ` A. M \ {}" + shows "Max (\x\ A. f x) = Max (Max ` f ` A)" (is "?L = ?R") + using assms[simp] +proof - + have "?L = Max (\(f ` A))" + by (fold Union_image_eq, simp) + also have "... = ?R" + by (subst Max_Union, simp+) + finally show ?thesis . +qed + +lemma max_Max_eq: + assumes "finite A" + and "A \ {}" + and "x = y" + shows "max x (Max A) = Max ({y} \ A)" (is "?L = ?R") +proof - + have "?R = Max (insert y A)" by simp + also from assms have "... = ?L" + by (subst Max.insert, simp+) + finally show ?thesis by simp +qed + +lemma birth_time_lt: + assumes "s \ []" + shows "last_set th s < length s" + using assms +proof(induct s) + case (Cons a s) + show ?case + proof(cases "s \ []") + case False + thus ?thesis + by (cases a, auto) + next + case True + show ?thesis using Cons(1)[OF True] + by (cases a, auto) + qed +qed simp + +lemma th_in_ne: "th \ threads s \ s \ []" + by (induct s, auto) + +lemma preced_tm_lt: "th \ threads s \ preced th s = Prc x y \ y < length s" + by (drule_tac th_in_ne, unfold preced_def, auto intro: birth_time_lt) + lemma eq_RAG: "RAG (wq s) = RAG s" by (unfold cs_RAG_def s_RAG_def, auto) @@ -1475,16 +1537,16 @@ by (unfold s_RAG_def cs_waiting_def cs_holding_def, auto intro:wq_threads) +lemma RAG_threads: + assumes "(Th th) \ Field (RAG s)" + shows "th \ threads s" + using assms + by (metis Field_def UnE dm_RAG_threads rg_RAG_threads) + end - - - -lemma preced_v [simp]: "preced th' (V th cs#s) = preced th' s" - by (unfold preced_def, simp) - lemma (in valid_trace_v) - preced_es: "preced th (e#s) = preced th s" + preced_es [simp]: "preced th (e#s) = preced th s" by (unfold is_v preced_def, simp) lemma the_preced_v[simp]: "the_preced (V th cs#s) = the_preced s" @@ -2105,6 +2167,44 @@ qed qed +lemma tRAG_alt_def: + "tRAG s = {(Th th1, Th th2) | th1 th2. + \ cs. (Th th1, Cs cs) \ RAG s \ (Cs cs, Th th2) \ RAG s}" + by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def) + +sublocale valid_trace < fsbttRAGs: fsubtree "tRAG s" +proof - + have "fsubtree (tRAG s)" + proof - + have "fbranch (tRAG s)" + proof(unfold tRAG_def, rule fbranch_compose) + show "fbranch (wRAG s)" + proof(rule finite_fbranchI) + from finite_RAG show "finite (wRAG s)" + by (unfold RAG_split, auto) + qed + next + show "fbranch (hRAG s)" + proof(rule finite_fbranchI) + from finite_RAG + show "finite (hRAG s)" by (unfold RAG_split, auto) + qed + qed + moreover have "wf (tRAG s)" + proof(rule wf_subset) + show "wf (RAG s O RAG s)" using wf_RAG + by (fold wf_comp_self, simp) + next + show "tRAG s \ (RAG s O RAG s)" + by (unfold tRAG_alt_def, auto) + qed + ultimately show ?thesis + by (unfold fsubtree_def fsubtree_axioms_def,auto) + qed + from this[folded tRAG_def] show "fsubtree (tRAG s)" . +qed + + context valid_trace begin @@ -2119,7 +2219,7 @@ have "?B = (subtree (RAG s) (Th th)) \ {Th th' | th'. True}" by auto moreover have "... \ (subtree (RAG s) (Th th))" by auto - moreover have "finite ..." by (simp add: finite_subtree) + moreover have "finite ..." by (simp add: fsbtRAGs.finite_subtree) ultimately show ?thesis by auto qed ultimately show ?thesis by auto @@ -2169,10 +2269,6 @@ ultimately show ?thesis by auto qed -lemma max_cp_eq_the_preced: - shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)" - using max_cp_eq using the_preced_def by presburger - lemma wf_RAG_converse: shows "wf ((RAG s)^-1)" proof(rule finite_acyclic_wf_converse) @@ -2317,9 +2413,6 @@ "children (RAG (s::state)) (Th th) = Cs ` {cs. holding s th cs}" by (unfold s_RAG_def, auto simp:children_def holding_eq) -fun the_cs :: "node \ cs" where - "the_cs (Cs cs) = cs" - lemma holdents_alt_def: "holdents s th = the_cs ` (children (RAG (s::state)) (Th th))" by (unfold children_RAG_alt_def holdents_def, simp add: image_image) @@ -2333,7 +2426,7 @@ begin lemma finite_holdents: "finite (holdents s th)" - by (unfold holdents_alt_def, insert finite_children, auto) + by (unfold holdents_alt_def, insert fsbtRAGs.finite_children, auto) end @@ -2577,7 +2670,7 @@ using readys_kept1[OF assms] readys_kept2[OF assms] by metis -lemma cnp_cnv_cncs_kept: +lemma cnp_cnv_cncs_kept: (* ddd *) assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'" shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'" proof(cases "th' = th") @@ -3643,29 +3736,921 @@ 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 rule:rtree_RAG.rpath_overlap[OF rp1 rp2]) - case (1 xs') + proof(cases) + case (less_1 xs') moreover have "xs' = []" proof(rule ccontr) assume otherwise: "xs' \ []" - find_theorems rpath "_@_" + 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 waiting_eq, auto) + with runing_1 show False + by (unfold runing_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 (2 xs') - moreover have "xs' = []" sorry + 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 waiting_eq, auto) + with runing_2 show False + by (unfold runing_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 qed +lemma card_runing: "card (runing s) \ 1" +proof(cases "runing s = {}") + case True + thus ?thesis by auto +next + case False + then obtain th where [simp]: "th \ runing s" by auto + from runing_unique[OF this] + have "runing s = {th}" by auto + thus ?thesis by auto +qed + +lemma create_pre: + assumes stp: "step s e" + and not_in: "th \ threads s" + and is_in: "th \ threads (e#s)" + obtains prio where "e = Create th prio" +proof - + from assms + show ?thesis + proof(cases) + case (thread_create thread prio) + with is_in not_in have "e = Create th prio" by simp + from that[OF this] show ?thesis . + next + case (thread_exit thread) + with assms show ?thesis by (auto intro!:that) + next + case (thread_P thread) + with assms show ?thesis by (auto intro!:that) + next + case (thread_V thread) + with assms show ?thesis by (auto intro!:that) + next + case (thread_set thread) + with assms show ?thesis by (auto intro!:that) + qed +qed + +lemma eq_pv_children: + assumes eq_pv: "cntP s th = cntV s th" + shows "children (RAG s) (Th th) = {}" +proof - + from cnp_cnv_cncs and eq_pv + have "cntCS s th = 0" + by (auto split:if_splits) + from this[unfolded cntCS_def holdents_alt_def] + have card_0: "card (the_cs ` children (RAG s) (Th th)) = 0" . + have "finite (the_cs ` children (RAG s) (Th th))" + by (simp add: fsbtRAGs.finite_children) + from card_0[unfolded card_0_eq[OF this]] + show ?thesis by auto +qed + +lemma eq_pv_holdents: + assumes eq_pv: "cntP s th = cntV s th" + shows "holdents s th = {}" + by (unfold holdents_alt_def eq_pv_children[OF assms], simp) + +lemma eq_pv_subtree: + assumes eq_pv: "cntP s th = cntV s th" + shows "subtree (RAG s) (Th th) = {Th th}" + using eq_pv_children[OF assms] + by (unfold subtree_children, simp) + end - +lemma cp_gen_alt_def: + "cp_gen s = (Max \ (\x. (the_preced s \ the_thread) ` subtree (tRAG s) x))" + by (auto simp:cp_gen_def) + +lemma tRAG_nodeE: + assumes "(n1, n2) \ tRAG s" + obtains th1 th2 where "n1 = Th th1" "n2 = Th th2" + using assms + by (auto simp: tRAG_def wRAG_def hRAG_def tRAG_def) + +lemma subtree_nodeE: + assumes "n \ subtree (tRAG s) (Th th)" + obtains th1 where "n = Th th1" +proof - + show ?thesis + proof(rule subtreeE[OF assms]) + assume "n = Th th" + from that[OF this] show ?thesis . + next + assume "Th th \ ancestors (tRAG s) n" + hence "(n, Th th) \ (tRAG s)^+" by (auto simp:ancestors_def) + hence "\ th1. n = Th th1" + proof(induct) + case (base y) + from tRAG_nodeE[OF this] show ?case by metis + next + case (step y z) + thus ?case by auto + qed + with that show ?thesis by auto + qed +qed + +lemma tRAG_star_RAG: "(tRAG s)^* \ (RAG s)^*" +proof - + have "(wRAG s O hRAG s)^* \ (RAG s O RAG s)^*" + by (rule rtrancl_mono, auto simp:RAG_split) + also have "... \ ((RAG s)^*)^*" + by (rule rtrancl_mono, auto) + also have "... = (RAG s)^*" by simp + finally show ?thesis by (unfold tRAG_def, simp) +qed + +lemma tRAG_subtree_RAG: "subtree (tRAG s) x \ subtree (RAG s) x" +proof - + { fix a + assume "a \ subtree (tRAG s) x" + hence "(a, x) \ (tRAG s)^*" by (auto simp:subtree_def) + with tRAG_star_RAG + have "(a, x) \ (RAG s)^*" by auto + hence "a \ subtree (RAG s) x" by (auto simp:subtree_def) + } thus ?thesis by auto +qed + +lemma tRAG_trancl_eq: + "{th'. (Th th', Th th) \ (tRAG s)^+} = + {th'. (Th th', Th th) \ (RAG s)^+}" + (is "?L = ?R") +proof - + { fix th' + assume "th' \ ?L" + hence "(Th th', Th th) \ (tRAG s)^+" by auto + from tranclD[OF this] + obtain z where h: "(Th th', z) \ tRAG s" "(z, Th th) \ (tRAG s)\<^sup>*" by auto + from tRAG_subtree_RAG and this(2) + have "(z, Th th) \ (RAG s)^*" by (meson subsetCE tRAG_star_RAG) + moreover from h(1) have "(Th th', z) \ (RAG s)^+" using tRAG_alt_def by auto + ultimately have "th' \ ?R" by auto + } moreover + { fix th' + assume "th' \ ?R" + hence "(Th th', Th th) \ (RAG s)^+" by (auto) + from plus_rpath[OF this] + obtain xs where rp: "rpath (RAG s) (Th th') xs (Th th)" "xs \ []" by auto + hence "(Th th', Th th) \ (tRAG s)^+" + proof(induct xs arbitrary:th' th rule:length_induct) + case (1 xs th' th) + then obtain x1 xs1 where Cons1: "xs = x1#xs1" by (cases xs, auto) + show ?case + proof(cases "xs1") + case Nil + from 1(2)[unfolded Cons1 Nil] + have rp: "rpath (RAG s) (Th th') [x1] (Th th)" . + hence "(Th th', x1) \ (RAG s)" + by (cases, auto) + then obtain cs where "x1 = Cs cs" + by (unfold s_RAG_def, auto) + from rpath_nnl_lastE[OF rp[unfolded this]] + show ?thesis by auto + next + case (Cons x2 xs2) + from 1(2)[unfolded Cons1[unfolded this]] + have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" . + from rpath_edges_on[OF this] + have eds: "edges_on (Th th' # x1 # x2 # xs2) \ RAG s" . + have "(Th th', x1) \ edges_on (Th th' # x1 # x2 # xs2)" + by (simp add: edges_on_unfold) + with eds have rg1: "(Th th', x1) \ RAG s" by auto + then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto) + have "(x1, x2) \ edges_on (Th th' # x1 # x2 # xs2)" + by (simp add: edges_on_unfold) + from this eds + have rg2: "(x1, x2) \ RAG s" by auto + from this[unfolded eq_x1] + obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto) + from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2] + have rt1: "(Th th', Th th1) \ tRAG s" by (unfold tRAG_alt_def, auto) + from rp have "rpath (RAG s) x2 xs2 (Th th)" + by (elim rpath_ConsE, simp) + from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" . + show ?thesis + proof(cases "xs2 = []") + case True + from rpath_nilE[OF rp'[unfolded this]] + have "th1 = th" by auto + from rt1[unfolded this] show ?thesis by auto + next + case False + from 1(1)[rule_format, OF _ rp' this, unfolded Cons1 Cons] + have "(Th th1, Th th) \ (tRAG s)\<^sup>+" by simp + with rt1 show ?thesis by auto + qed + qed + qed + hence "th' \ ?L" by auto + } ultimately show ?thesis by blast +qed + +lemma tRAG_trancl_eq_Th: + "{Th th' | th'. (Th th', Th th) \ (tRAG s)^+} = + {Th th' | th'. (Th th', Th th) \ (RAG s)^+}" + using tRAG_trancl_eq by auto + +lemma dependants_alt_def: + "dependants s th = {th'. (Th th', Th th) \ (tRAG s)^+}" + by (metis eq_RAG s_dependants_def tRAG_trancl_eq) + +lemma dependants_alt_def1: + "dependants (s::state) th = {th'. (Th th', Th th) \ (RAG s)^+}" + using dependants_alt_def tRAG_trancl_eq by auto + +context valid_trace +begin +lemma count_eq_RAG_plus: + assumes "cntP s th = cntV s th" + shows "{th'. (Th th', Th th) \ (RAG s)^+} = {}" +proof(rule ccontr) + assume otherwise: "{th'. (Th th', Th th) \ (RAG s)\<^sup>+} \ {}" + then obtain th' where "(Th th', Th th) \ (RAG s)^+" by auto + from tranclD2[OF this] + obtain z where "z \ children (RAG s) (Th th)" + by (auto simp:children_def) + with eq_pv_children[OF assms] + show False by simp +qed + +lemma eq_pv_dependants: + assumes eq_pv: "cntP s th = cntV s th" + shows "dependants s th = {}" +proof - + from count_eq_RAG_plus[OF assms, folded dependants_alt_def1] + show ?thesis . +qed + +end + +lemma eq_dependants: "dependants (wq s) = dependants s" + by (simp add: s_dependants_abv wq_def) + +context valid_trace +begin + +lemma count_eq_tRAG_plus: + assumes "cntP s th = cntV s th" + shows "{th'. (Th th', Th th) \ (tRAG s)^+} = {}" + using assms eq_pv_dependants dependants_alt_def eq_dependants by auto + +lemma count_eq_RAG_plus_Th: + assumes "cntP s th = cntV s th" + shows "{Th th' | th'. (Th th', Th th) \ (RAG s)^+} = {}" + using count_eq_RAG_plus[OF assms] by auto + +lemma count_eq_tRAG_plus_Th: + assumes "cntP s th = cntV s th" + shows "{Th th' | th'. (Th th', Th th) \ (tRAG s)^+} = {}" + using count_eq_tRAG_plus[OF assms] by auto +end + +lemma inj_the_preced: + "inj_on (the_preced s) (threads s)" + by (metis inj_onI preced_unique the_preced_def) + +lemma tRAG_Field: + "Field (tRAG s) \ Field (RAG s)" + by (unfold tRAG_alt_def Field_def, auto) + +lemma tRAG_ancestorsE: + assumes "x \ ancestors (tRAG s) u" + obtains th where "x = Th th" +proof - + from assms have "(u, x) \ (tRAG s)^+" + by (unfold ancestors_def, auto) + from tranclE[OF this] obtain c where "(c, x) \ tRAG s" by auto + then obtain th where "x = Th th" + by (unfold tRAG_alt_def, auto) + from that[OF this] show ?thesis . +qed + +lemma tRAG_mono: + assumes "RAG s' \ RAG s" + shows "tRAG s' \ tRAG s" + using assms + by (unfold tRAG_alt_def, auto) + +lemma holding_next_thI: + assumes "holding s th cs" + and "length (wq s cs) > 1" + obtains th' where "next_th s th cs th'" +proof - + from assms(1)[folded holding_eq, unfolded cs_holding_def] + have " th \ set (wq s cs) \ th = hd (wq s cs)" + by (unfold s_holding_def, fold wq_def, auto) + then obtain rest where h1: "wq s cs = th#rest" + by (cases "wq s cs", auto) + with assms(2) have h2: "rest \ []" by auto + let ?th' = "hd (SOME q. distinct q \ set q = set rest)" + have "next_th s th cs ?th'" using h1(1) h2 + by (unfold next_th_def, auto) + from that[OF this] show ?thesis . +qed + +lemma RAG_tRAG_transfer: + assumes "vt s'" + assumes "RAG s = RAG s' \ {(Th th, Cs cs)}" + and "(Cs cs, Th th'') \ RAG s'" + shows "tRAG s = tRAG s' \ {(Th th, Th th'')}" (is "?L = ?R") +proof - + interpret vt_s': valid_trace "s'" using assms(1) + by (unfold_locales, simp) + { fix n1 n2 + assume "(n1, n2) \ ?L" + from this[unfolded tRAG_alt_def] + obtain th1 th2 cs' where + h: "n1 = Th th1" "n2 = Th th2" + "(Th th1, Cs cs') \ RAG s" + "(Cs cs', Th th2) \ RAG s" by auto + from h(4) and assms(2) have cs_in: "(Cs cs', Th th2) \ RAG s'" by auto + from h(3) and assms(2) + have "(Th th1, Cs cs') = (Th th, Cs cs) \ + (Th th1, Cs cs') \ RAG s'" by auto + hence "(n1, n2) \ ?R" + proof + assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)" + hence eq_th1: "th1 = th" by simp + moreover have "th2 = th''" + proof - + from h1 have "cs' = cs" by simp + from assms(3) cs_in[unfolded this] + show ?thesis using vt_s'.unique_RAG by auto + qed + ultimately show ?thesis using h(1,2) by auto + next + assume "(Th th1, Cs cs') \ RAG s'" + with cs_in have "(Th th1, Th th2) \ tRAG s'" + by (unfold tRAG_alt_def, auto) + from this[folded h(1, 2)] show ?thesis by auto + qed + } moreover { + fix n1 n2 + assume "(n1, n2) \ ?R" + hence "(n1, n2) \tRAG s' \ (n1, n2) = (Th th, Th th'')" by auto + hence "(n1, n2) \ ?L" + proof + assume "(n1, n2) \ tRAG s'" + moreover have "... \ ?L" + proof(rule tRAG_mono) + show "RAG s' \ RAG s" by (unfold assms(2), auto) + qed + ultimately show ?thesis by auto + next + assume eq_n: "(n1, n2) = (Th th, Th th'')" + from assms(2, 3) have "(Cs cs, Th th'') \ RAG s" by auto + moreover have "(Th th, Cs cs) \ RAG s" using assms(2) by auto + ultimately show ?thesis + by (unfold eq_n tRAG_alt_def, auto) + qed + } ultimately show ?thesis by auto +qed + +context valid_trace +begin + +lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt] end +lemma tRAG_subtree_eq: + "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th' \ (subtree (RAG s) (Th th))}" + (is "?L = ?R") +proof - + { fix n + assume h: "n \ ?L" + hence "n \ ?R" + by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) + } moreover { + fix n + assume "n \ ?R" + then obtain th' where h: "n = Th th'" "(Th th', Th th) \ (RAG s)^*" + by (auto simp:subtree_def) + from rtranclD[OF this(2)] + have "n \ ?L" + proof + assume "Th th' \ Th th \ (Th th', Th th) \ (RAG s)\<^sup>+" + with h have "n \ {Th th' | th'. (Th th', Th th) \ (RAG s)^+}" by auto + thus ?thesis using subtree_def tRAG_trancl_eq by fastforce + qed (insert h, auto simp:subtree_def) + } ultimately show ?thesis by auto +qed + +lemma threads_set_eq: + "the_thread ` (subtree (tRAG s) (Th th)) = + {th'. Th th' \ (subtree (RAG s) (Th th))}" (is "?L = ?R") + by (auto intro:rev_image_eqI simp:tRAG_subtree_eq) + +lemma cp_alt_def1: + "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))" +proof - + have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) = + ((the_preced s \ the_thread) ` subtree (tRAG s) (Th th))" + by auto + thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto) +qed + +lemma cp_gen_def_cond: + assumes "x = Th th" + shows "cp s th = cp_gen s (Th th)" +by (unfold cp_alt_def1 cp_gen_def, simp) + +lemma cp_gen_over_set: + assumes "\ x \ A. \ th. x = Th th" + shows "cp_gen s ` A = (cp s \ the_thread) ` A" +proof(rule f_image_eq) + fix a + assume "a \ A" + from assms[rule_format, OF this] + obtain th where eq_a: "a = Th th" by auto + show "cp_gen s a = (cp s \ the_thread) a" + by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp) +qed + +context valid_trace +begin + +lemma subtree_tRAG_thread: + assumes "th \ threads s" + shows "subtree (tRAG s) (Th th) \ Th ` threads s" (is "?L \ ?R") +proof - + have "?L = {Th th' |th'. Th th' \ subtree (RAG s) (Th th)}" + by (unfold tRAG_subtree_eq, simp) + also have "... \ ?R" + proof + fix x + assume "x \ {Th th' |th'. Th th' \ subtree (RAG s) (Th th)}" + then obtain th' where h: "x = Th th'" "Th th' \ subtree (RAG s) (Th th)" by auto + from this(2) + show "x \ ?R" + proof(cases rule:subtreeE) + case 1 + thus ?thesis by (simp add: assms h(1)) + next + case 2 + thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) + qed + qed + finally show ?thesis . +qed + +lemma readys_root: + assumes "th \ readys s" + shows "root (RAG s) (Th th)" +proof - + { fix x + assume "x \ ancestors (RAG s) (Th th)" + hence h: "(Th th, x) \ (RAG s)^+" by (auto simp:ancestors_def) + from tranclD[OF this] + obtain z where "(Th th, z) \ RAG s" by auto + with assms(1) have False + apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def) + by (fold wq_def, blast) + } thus ?thesis by (unfold root_def, auto) +qed + +lemma readys_in_no_subtree: + assumes "th \ readys s" + and "th' \ th" + shows "Th th \ subtree (RAG s) (Th th')" +proof + assume "Th th \ subtree (RAG s) (Th th')" + thus False + proof(cases rule:subtreeE) + case 1 + with assms show ?thesis by auto + next + case 2 + with readys_root[OF assms(1)] + show ?thesis by (auto simp:root_def) + qed +qed + +lemma not_in_thread_isolated: + assumes "th \ threads s" + shows "(Th th) \ Field (RAG s)" +proof + assume "(Th th) \ Field (RAG s)" + with dm_RAG_threads and rg_RAG_threads assms + show False by (unfold Field_def, blast) +qed + +end + +definition detached :: "state \ thread \ bool" + where "detached s th \ (\(\ cs. holding s th cs)) \ (\(\cs. waiting s th cs))" + + +lemma detached_test: + shows "detached s th = (Th th \ Field (RAG s))" +apply(simp add: detached_def Field_def) +apply(simp add: s_RAG_def) +apply(simp add: s_holding_abv s_waiting_abv) +apply(simp add: Domain_iff Range_iff) +apply(simp add: wq_def) +apply(auto) +done + +context valid_trace +begin + +lemma detached_intro: + assumes eq_pv: "cntP s th = cntV s th" + shows "detached s th" +proof - + from eq_pv cnp_cnv_cncs + have "th \ readys s \ th \ threads s" by (auto simp:pvD_def) + thus ?thesis + proof + assume "th \ threads s" + with rg_RAG_threads dm_RAG_threads + show ?thesis + by (auto simp add: detached_def s_RAG_def s_waiting_abv + s_holding_abv wq_def Domain_iff Range_iff) + next + assume "th \ readys s" + moreover have "Th th \ Range (RAG s)" + proof - + from eq_pv_children[OF assms] + have "children (RAG s) (Th th) = {}" . + thus ?thesis + by (unfold children_def, auto) + qed + ultimately show ?thesis + by (auto simp add: detached_def s_RAG_def s_waiting_abv + s_holding_abv wq_def readys_def) + qed +qed + +lemma detached_elim: + assumes dtc: "detached s th" + shows "cntP s th = cntV s th" +proof - + have cncs_z: "cntCS s th = 0" + proof - + from dtc have "holdents s th = {}" + unfolding detached_def holdents_test s_RAG_def + by (simp add: s_waiting_abv wq_def s_holding_abv Domain_iff Range_iff) + thus ?thesis by (auto simp:cntCS_def) + qed + show ?thesis + proof(cases "th \ threads s") + case True + with dtc + have "th \ readys s" + by (unfold readys_def detached_def Field_def Domain_def Range_def, + auto simp:waiting_eq s_RAG_def) + with cncs_z show ?thesis using cnp_cnv_cncs by (simp add:pvD_def) + next + case False + with cncs_z and cnp_cnv_cncs show ?thesis by (simp add:pvD_def) + qed +qed + +lemma detached_eq: + shows "(detached s th) = (cntP s th = cntV s th)" + by (insert vt, auto intro:detached_intro detached_elim) + +end + +context valid_trace +begin +(* ddd *) +lemma cp_gen_rec: + assumes "x = Th th" + shows "cp_gen s x = Max ({the_preced s th} \ (cp_gen s) ` children (tRAG s) x)" +proof(cases "children (tRAG s) x = {}") + case True + show ?thesis + by (unfold True cp_gen_def subtree_children, simp add:assms) +next + case False + hence [simp]: "children (tRAG s) x \ {}" by auto + note fsbttRAGs.finite_subtree[simp] + have [simp]: "finite (children (tRAG s) x)" + by (intro rev_finite_subset[OF fsbttRAGs.finite_subtree], + rule children_subtree) + { fix r x + have "subtree r x \ {}" by (auto simp:subtree_def) + } note this[simp] + have [simp]: "\x\children (tRAG s) x. subtree (tRAG s) x \ {}" + proof - + from False obtain q where "q \ children (tRAG s) x" by blast + moreover have "subtree (tRAG s) q \ {}" by simp + ultimately show ?thesis by blast + qed + have h: "Max ((the_preced s \ the_thread) ` + ({x} \ \(subtree (tRAG s) ` children (tRAG s) x))) = + Max ({the_preced s th} \ cp_gen s ` children (tRAG s) x)" + (is "?L = ?R") + proof - + let "Max (?f ` (?A \ \ (?g ` ?B)))" = ?L + let "Max (_ \ (?h ` ?B))" = ?R + let ?L1 = "?f ` \(?g ` ?B)" + have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)" + proof - + have "?L1 = ?f ` (\ x \ ?B.(?g x))" by simp + also have "... = (\ x \ ?B. ?f ` (?g x))" by auto + finally have "Max ?L1 = Max ..." by simp + also have "... = Max (Max ` (\x. ?f ` subtree (tRAG s) x) ` ?B)" + by (subst Max_UNION, simp+) + also have "... = Max (cp_gen s ` children (tRAG s) x)" + by (unfold image_comp cp_gen_alt_def, simp) + finally show ?thesis . + qed + show ?thesis + proof - + have "?L = Max (?f ` ?A \ ?L1)" by simp + also have "... = max (the_preced s (the_thread x)) (Max ?L1)" + by (subst Max_Un, simp+) + also have "... = max (?f x) (Max (?h ` ?B))" + by (unfold eq_Max_L1, simp) + also have "... =?R" + by (rule max_Max_eq, (simp)+, unfold assms, simp) + finally show ?thesis . + qed + qed thus ?thesis + by (fold h subtree_children, unfold cp_gen_def, simp) +qed + +lemma cp_rec: + "cp s th = Max ({the_preced s th} \ + (cp s o the_thread) ` children (tRAG s) (Th th))" +proof - + have "Th th = Th th" by simp + note h = cp_gen_def_cond[OF this] cp_gen_rec[OF this] + show ?thesis + proof - + have "cp_gen s ` children (tRAG s) (Th th) = + (cp s \ the_thread) ` children (tRAG s) (Th th)" + proof(rule cp_gen_over_set) + show " \x\children (tRAG s) (Th th). \th. x = Th th" + by (unfold tRAG_alt_def, auto simp:children_def) + qed + thus ?thesis by (subst (1) h(1), unfold h(2), simp) + qed +qed + +lemma next_th_holding: + assumes nxt: "next_th s th cs th'" + shows "holding (wq s) th cs" +proof - + from nxt[unfolded next_th_def] + obtain rest where h: "wq s cs = th # rest" + "rest \ []" + "th' = hd (SOME q. distinct q \ set q = set rest)" by auto + thus ?thesis + by (unfold cs_holding_def, auto) +qed + +lemma next_th_waiting: + assumes nxt: "next_th s th cs th'" + shows "waiting (wq s) th' cs" +proof - + from nxt[unfolded next_th_def] + obtain rest where h: "wq s cs = th # rest" + "rest \ []" + "th' = hd (SOME q. distinct q \ set q = set rest)" by auto + from wq_distinct[of cs, unfolded h] + have dst: "distinct (th # rest)" . + have in_rest: "th' \ set rest" + proof(unfold h, rule someI2) + show "distinct rest \ set rest = set rest" using dst by auto + next + fix x assume "distinct x \ set x = set rest" + with h(2) + show "hd x \ set (rest)" by (cases x, auto) + qed + hence "th' \ set (wq s cs)" by (unfold h(1), auto) + moreover have "th' \ hd (wq s cs)" + by (unfold h(1), insert in_rest dst, auto) + ultimately show ?thesis by (auto simp:cs_waiting_def) +qed + +lemma next_th_RAG: + assumes nxt: "next_th (s::event list) th cs th'" + shows "{(Cs cs, Th th), (Th th', Cs cs)} \ RAG s" + using vt assms next_th_holding next_th_waiting + by (unfold s_RAG_def, simp) + +end + +lemma next_th_unique: + assumes nt1: "next_th s th cs th1" + and nt2: "next_th s th cs th2" + shows "th1 = th2" +using assms by (unfold next_th_def, auto) + +context valid_trace +begin + +thm th_chain_to_ready + +find_theorems subtree Th RAG + +lemma "(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'a. th'a \ readys s \ (Th th1, Th th'a) \ (RAG s)\<^sup>+)" . + hence "th1 \ ?R" + proof + assume "th1 \ readys s" + thus ?thesis by (auto simp:subtree_def) + next + assume "\th'a. th'a \ readys s \ (Th th1, Th th'a) \ (RAG s)\<^sup>+" + thus ?thesis + qed + } moreover + { fix th' + assume "th' \ ?R" + have "th' \ ?L" sorry + } ultimately show ?thesis by auto +qed + +lemma max_cp_readys_threads_pre: (* ccc *) + assumes np: "threads s \ {}" + shows "Max (cp s ` readys s) = Max (cp s ` threads s)" +proof(unfold max_cp_eq) + show "Max (cp s ` readys s) = Max (the_preced s ` threads s)" + proof - + let ?p = "Max (the_preced s ` threads s)" + let ?f = "the_preced s" + have "?p \ (?f ` threads s)" + proof(rule Max_in) + from finite_threads show "finite (?f ` threads s)" by simp + next + from np show "?f ` threads s \ {}" by simp + qed + then obtain tm where tm_max: "?f tm = ?p" and tm_in: "tm \ threads s" + by (auto simp:Image_def) + from th_chain_to_ready [OF tm_in] + have "tm \ readys s \ (\th'. th' \ readys s \ (Th tm, Th th') \ (RAG s)\<^sup>+)" . + thus ?thesis + proof + assume "\th'. th' \ readys s \ (Th tm, Th th') \ (RAG s)\<^sup>+ " + then obtain th' where th'_in: "th' \ readys s" + and tm_chain:"(Th tm, Th th') \ (RAG s)\<^sup>+" by auto + have "cp s th' = ?f tm" + proof(subst cp_eq_cpreced, subst cpreced_def, rule Max_eqI) + from dependants_threads finite_threads + show "finite ((\th. preced th s) ` ({th'} \ dependants (wq s) th'))" + by (auto intro:finite_subset) + next + fix p assume p_in: "p \ (\th. preced th s) ` ({th'} \ dependants (wq s) th')" + from tm_max have " preced tm s = Max ((\th. preced th s) ` threads s)" . + moreover have "p \ \" + proof(rule Max_ge) + from finite_threads + show "finite ((\th. preced th s) ` threads s)" by simp + next + from p_in and th'_in and dependants_threads[of th'] + show "p \ (\th. preced th s) ` threads s" + by (auto simp:readys_def) + qed + ultimately show "p \ preced tm s" by auto + next + show "preced tm s \ (\th. preced th s) ` ({th'} \ dependants (wq s) th')" + proof - + from tm_chain + have "tm \ dependants (wq s) th'" + by (unfold cs_dependants_def s_RAG_def cs_RAG_def, auto) + thus ?thesis by auto + qed + qed + with tm_max + have h: "cp s th' = Max ((\th. preced th s) ` threads s)" by simp + show ?thesis + proof (fold h, rule Max_eqI) + fix q + assume "q \ cp s ` readys s" + then obtain th1 where th1_in: "th1 \ readys s" + and eq_q: "q = cp s th1" by auto + show "q \ cp s th'" + apply (unfold h eq_q) + apply (unfold cp_eq_cpreced cpreced_def) + apply (rule Max_mono) + proof - + from dependants_threads [of th1] th1_in + show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) \ + (\th. preced th s) ` threads s" + by (auto simp:readys_def) + next + show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) \ {}" by simp + next + from finite_threads + show " finite ((\th. preced th s) ` threads s)" by simp + qed + next + from finite_threads + show "finite (cp s ` readys s)" by (auto simp:readys_def) + next + from th'_in + show "cp s th' \ cp s ` readys s" by simp + qed + next + assume tm_ready: "tm \ readys s" + show ?thesis + proof(fold tm_max) + have cp_eq_p: "cp s tm = preced tm s" + proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI) + fix y + assume hy: "y \ (\th. preced th s) ` ({tm} \ dependants (wq s) tm)" + show "y \ preced tm s" + proof - + { fix y' + assume hy' : "y' \ ((\th. preced th s) ` dependants (wq s) tm)" + have "y' \ preced tm s" + proof(unfold tm_max, rule Max_ge) + from hy' dependants_threads[of tm] + show "y' \ (\th. preced th s) ` threads s" by auto + next + from finite_threads + show "finite ((\th. preced th s) ` threads s)" by simp + qed + } with hy show ?thesis by auto + qed + next + from dependants_threads[of tm] finite_threads + show "finite ((\th. preced th s) ` ({tm} \ dependants (wq s) tm))" + by (auto intro:finite_subset) + next + show "preced tm s \ (\th. preced th s) ` ({tm} \ dependants (wq s) tm)" + by simp + qed + moreover have "Max (cp s ` readys s) = cp s tm" + proof(rule Max_eqI) + from tm_ready show "cp s tm \ cp s ` readys s" by simp + next + from finite_threads + show "finite (cp s ` readys s)" by (auto simp:readys_def) + next + fix y assume "y \ cp s ` readys s" + then obtain th1 where th1_readys: "th1 \ readys s" + and h: "y = cp s th1" by auto + show "y \ cp s tm" + apply(unfold cp_eq_p h) + apply(unfold cp_eq_cpreced cpreced_def tm_max, rule Max_mono) + proof - + from finite_threads + show "finite ((\th. preced th s) ` threads s)" by simp + next + show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) \ {}" + by simp + next + from dependants_threads[of th1] th1_readys + show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) + \ (\th. preced th s) ` threads s" + by (auto simp:readys_def) + qed + qed + ultimately show " Max (cp s ` readys s) = preced tm s" by simp + qed + qed + qed +qed + +text {* (* ccc *) \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. +*} +lemma max_cp_readys_threads: + shows "Max (cp s ` readys s) = Max (cp s ` threads s)" +proof(cases "threads s = {}") + case True + thus ?thesis + by (auto simp:readys_def) +next + case False + show ?thesis by (rule max_cp_readys_threads_pre[OF False]) +qed + +end + +end + diff -r 2056d9f481e2 -r ed938e2246b9 PIPBasics.thy --- a/PIPBasics.thy Thu Jan 28 16:36:46 2016 +0800 +++ b/PIPBasics.thy Thu Jan 28 21:14:17 2016 +0800 @@ -3784,5 +3784,4 @@ end - end diff -r 2056d9f481e2 -r ed938e2246b9 PIPBasics.thy~ --- a/PIPBasics.thy~ Thu Jan 28 16:36:46 2016 +0800 +++ b/PIPBasics.thy~ Thu Jan 28 21:14:17 2016 +0800 @@ -3784,4 +3784,5 @@ end + end diff -r 2056d9f481e2 -r ed938e2246b9 PrioG.thy --- a/PrioG.thy Thu Jan 28 16:36:46 2016 +0800 +++ b/PrioG.thy Thu Jan 28 21:14:17 2016 +0800 @@ -2,7 +2,6 @@ imports CpsG begin - text {* The following two auxiliary lemmas are used to reason about @{term Max}. *} @@ -512,7 +511,7 @@ thread. The proof is by contraction with the assumption @{text "th' \ th"}. - The key is the use of @{thm count_eq_dependants} to derive the + The key is the use of @{thm eq_pv_dependants} to derive the emptiness of @{text th'}s @{term dependants}-set from the balance of its @{term P} and @{term V} counts. From this, it can be shown @{text th'}s @{term cp}-value equals to its own precedence. @@ -551,7 +550,7 @@ of it contains only itself, so, its @{term cp}-value equals its @{term preced}-value: *} have "?L = cp (t@s) th'" - by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp) + by (unfold cp_eq_cpreced cpreced_def eq_dependants vat_t.eq_pv_dependants[OF eq_pv], simp) -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion}, its @{term cp}-value equals @{term "preced th s"}, which equals to @{term "?R"} by simplification: *} @@ -750,7 +749,7 @@ show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads) next show "subtree (tRAG (t @ s)) (Th th') \ Th ` threads (t @ s)" - by (metis Range.intros dp trancl_range vat_t.range_in vat_t.subtree_tRAG_thread) + by (metis Range.intros dp trancl_range vat_t.rg_RAG_threads vat_t.subtree_tRAG_thread) next show "Th th \ subtree (tRAG (t @ s)) (Th th')" using dp by (unfold tRAG_subtree_eq, auto simp:subtree_def) @@ -793,819 +792,5 @@ thus ?thesis using th_blockedE by auto qed - end end -======= -theory Correctness -imports PIPBasics -begin - - -text {* - The following two auxiliary lemmas are used to reason about @{term Max}. -*} -lemma image_Max_eqI: - assumes "finite B" - and "b \ B" - and "\ x \ B. f x \ f b" - shows "Max (f ` B) = f b" - using assms - using Max_eqI by blast - -lemma image_Max_subset: - assumes "finite A" - and "B \ A" - and "a \ B" - and "Max (f ` A) = f a" - shows "Max (f ` B) = f a" -proof(rule image_Max_eqI) - show "finite B" - using assms(1) assms(2) finite_subset by auto -next - show "a \ B" using assms by simp -next - show "\x\B. f x \ f a" - by (metis Max_ge assms(1) assms(2) assms(4) - finite_imageI image_eqI subsetCE) -qed - -text {* - The following locale @{text "highest_gen"} sets the basic context for our - investigation: supposing thread @{text th} holds the highest @{term cp}-value - in state @{text s}, which means the task for @{text th} is the - most urgent. We want to show that - @{text th} is treated correctly by PIP, which means - @{text th} will not be blocked unreasonably by other less urgent - threads. -*} -locale highest_gen = - fixes s th prio tm - assumes vt_s: "vt s" - and threads_s: "th \ threads s" - and highest: "preced th s = Max ((cp s)`threads s)" - -- {* The internal structure of @{term th}'s precedence is exposed:*} - and preced_th: "preced th s = Prc prio tm" - --- {* @{term s} is a valid trace, so it will inherit all results derived for - a valid trace: *} -sublocale highest_gen < vat_s: valid_trace "s" - by (unfold_locales, insert vt_s, simp) - -context highest_gen -begin - -text {* - @{term tm} is the time when the precedence of @{term th} is set, so - @{term tm} must be a valid moment index into @{term s}. -*} -lemma lt_tm: "tm < length s" - by (insert preced_tm_lt[OF threads_s preced_th], simp) - -text {* - Since @{term th} holds the highest precedence and @{text "cp"} - is the highest precedence of all threads in the sub-tree of - @{text "th"} and @{text th} is among these threads, - its @{term cp} must equal to its precedence: -*} -lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R") -proof - - have "?L \ ?R" - by (unfold highest, rule Max_ge, - auto simp:threads_s finite_threads) - moreover have "?R \ ?L" - by (unfold vat_s.cp_rec, rule Max_ge, - auto simp:the_preced_def vat_s.fsbttRAGs.finite_children) - ultimately show ?thesis by auto -qed - -lemma highest_cp_preced: "cp s th = Max (the_preced s ` threads s)" - using eq_cp_s_th highest max_cp_eq the_preced_def by presburger - - -lemma highest_preced_thread: "preced th s = Max (the_preced s ` threads s)" - by (fold eq_cp_s_th, unfold highest_cp_preced, simp) - -lemma highest': "cp s th = Max (cp s ` threads s)" - by (simp add: eq_cp_s_th highest) - -end - -locale extend_highest_gen = highest_gen + - fixes t - assumes vt_t: "vt (t@s)" - and create_low: "Create th' prio' \ set t \ prio' \ prio" - and set_diff_low: "Set th' prio' \ set t \ th' \ th \ prio' \ prio" - and exit_diff: "Exit th' \ set t \ th' \ th" - -sublocale extend_highest_gen < vat_t: valid_trace "t@s" - by (unfold_locales, insert vt_t, simp) - -lemma step_back_vt_app: - assumes vt_ts: "vt (t@s)" - shows "vt s" -proof - - from vt_ts show ?thesis - proof(induct t) - case Nil - from Nil show ?case by auto - next - case (Cons e t) - assume ih: " vt (t @ s) \ vt s" - and vt_et: "vt ((e # t) @ s)" - show ?case - proof(rule ih) - show "vt (t @ s)" - proof(rule step_back_vt) - from vt_et show "vt (e # t @ s)" by simp - qed - qed - qed -qed - -(* locale red_extend_highest_gen = extend_highest_gen + - fixes i::nat -*) - -(* -sublocale red_extend_highest_gen < red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)" - apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric]) - apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp) - by (unfold highest_gen_def, auto dest:step_back_vt_app) -*) - -context extend_highest_gen -begin - - lemma ind [consumes 0, case_names Nil Cons, induct type]: - assumes - h0: "R []" - and h2: "\ e t. \vt (t@s); step (t@s) e; - extend_highest_gen s th prio tm t; - extend_highest_gen s th prio tm (e#t); R t\ \ R (e#t)" - shows "R t" -proof - - from vt_t extend_highest_gen_axioms show ?thesis - proof(induct t) - from h0 show "R []" . - next - case (Cons e t') - assume ih: "\vt (t' @ s); extend_highest_gen s th prio tm t'\ \ R t'" - and vt_e: "vt ((e # t') @ s)" - and et: "extend_highest_gen s th prio tm (e # t')" - from vt_e and step_back_step have stp: "step (t'@s) e" by auto - from vt_e and step_back_vt have vt_ts: "vt (t'@s)" by auto - show ?case - proof(rule h2 [OF vt_ts stp _ _ _ ]) - show "R t'" - proof(rule ih) - from et show ext': "extend_highest_gen s th prio tm t'" - by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt) - next - from vt_ts show "vt (t' @ s)" . - qed - next - from et show "extend_highest_gen s th prio tm (e # t')" . - next - from et show ext': "extend_highest_gen s th prio tm t'" - by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt) - qed - qed -qed - - -lemma th_kept: "th \ threads (t @ s) \ - preced th (t@s) = preced th s" (is "?Q t") -proof - - show ?thesis - proof(induct rule:ind) - case Nil - from threads_s - show ?case - by auto - next - case (Cons e t) - interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto - interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto - show ?case - proof(cases e) - case (Create thread prio) - show ?thesis - proof - - from Cons and Create have "step (t@s) (Create thread prio)" by auto - hence "th \ thread" - proof(cases) - case thread_create - with Cons show ?thesis by auto - qed - hence "preced th ((e # t) @ s) = preced th (t @ s)" - by (unfold Create, auto simp:preced_def) - moreover note Cons - ultimately show ?thesis - by (auto simp:Create) - qed - next - case (Exit thread) - from h_e.exit_diff and Exit - have neq_th: "thread \ th" by auto - with Cons - show ?thesis - by (unfold Exit, auto simp:preced_def) - next - case (P thread cs) - with Cons - show ?thesis - by (auto simp:P preced_def) - next - case (V thread cs) - with Cons - show ?thesis - by (auto simp:V preced_def) - next - case (Set thread prio') - show ?thesis - proof - - from h_e.set_diff_low and Set - have "th \ thread" by auto - hence "preced th ((e # t) @ s) = preced th (t @ s)" - by (unfold Set, auto simp:preced_def) - moreover note Cons - ultimately show ?thesis - by (auto simp:Set) - qed - qed - qed -qed - -text {* - According to @{thm th_kept}, thread @{text "th"} has its living status - and precedence kept along the way of @{text "t"}. The following lemma - shows that this preserved precedence of @{text "th"} remains as the highest - along the way of @{text "t"}. - - The proof goes by induction over @{text "t"} using the specialized - induction rule @{thm ind}, followed by case analysis of each possible - operations of PIP. All cases follow the same pattern rendered by the - generalized introduction rule @{thm "image_Max_eqI"}. - - The very essence is to show that precedences, no matter whether they - are newly introduced or modified, are always lower than the one held - by @{term "th"}, which by @{thm th_kept} is preserved along the way. -*} -lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s" -proof(induct rule:ind) - case Nil - from highest_preced_thread - show ?case by simp -next - case (Cons e t) - interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto - interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto - show ?case - proof(cases e) - case (Create thread prio') - show ?thesis (is "Max (?f ` ?A) = ?t") - proof - - -- {* The following is the common pattern of each branch of the case analysis. *} - -- {* The major part is to show that @{text "th"} holds the highest precedence: *} - have "Max (?f ` ?A) = ?f th" - proof(rule image_Max_eqI) - show "finite ?A" using h_e.finite_threads by auto - next - show "th \ ?A" using h_e.th_kept by auto - next - show "\x\?A. ?f x \ ?f th" - proof - fix x - assume "x \ ?A" - hence "x = thread \ x \ threads (t@s)" by (auto simp:Create) - thus "?f x \ ?f th" - proof - assume "x = thread" - thus ?thesis - apply (simp add:Create the_preced_def preced_def, fold preced_def) - using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 - preced_th by force - next - assume h: "x \ threads (t @ s)" - from Cons(2)[unfolded Create] - have "x \ thread" using h by (cases, auto) - hence "?f x = the_preced (t@s) x" - by (simp add:Create the_preced_def preced_def) - hence "?f x \ Max (the_preced (t@s) ` threads (t@s))" - by (simp add: h_t.finite_threads h) - also have "... = ?f th" - by (metis Cons.hyps(5) h_e.th_kept the_preced_def) - finally show ?thesis . - qed - qed - qed - -- {* The minor part is to show that the precedence of @{text "th"} - equals to preserved one, given by the foregoing lemma @{thm th_kept} *} - also have "... = ?t" using h_e.th_kept the_preced_def by auto - -- {* Then it follows trivially that the precedence preserved - for @{term "th"} remains the maximum of all living threads along the way. *} - finally show ?thesis . - qed - next - case (Exit thread) - show ?thesis (is "Max (?f ` ?A) = ?t") - proof - - have "Max (?f ` ?A) = ?f th" - proof(rule image_Max_eqI) - show "finite ?A" using h_e.finite_threads by auto - next - show "th \ ?A" using h_e.th_kept by auto - next - show "\x\?A. ?f x \ ?f th" - proof - fix x - assume "x \ ?A" - hence "x \ threads (t@s)" by (simp add: Exit) - hence "?f x \ Max (?f ` threads (t@s))" - by (simp add: h_t.finite_threads) - also have "... \ ?f th" - apply (simp add:Exit the_preced_def preced_def, fold preced_def) - using Cons.hyps(5) h_t.th_kept the_preced_def by auto - finally show "?f x \ ?f th" . - qed - qed - also have "... = ?t" using h_e.th_kept the_preced_def by auto - finally show ?thesis . - qed - next - case (P thread cs) - with Cons - show ?thesis by (auto simp:preced_def the_preced_def) - next - case (V thread cs) - with Cons - show ?thesis by (auto simp:preced_def the_preced_def) - next - case (Set thread prio') - show ?thesis (is "Max (?f ` ?A) = ?t") - proof - - have "Max (?f ` ?A) = ?f th" - proof(rule image_Max_eqI) - show "finite ?A" using h_e.finite_threads by auto - next - show "th \ ?A" using h_e.th_kept by auto - next - show "\x\?A. ?f x \ ?f th" - proof - fix x - assume h: "x \ ?A" - show "?f x \ ?f th" - proof(cases "x = thread") - case True - moreover have "the_preced (Set thread prio' # t @ s) thread \ the_preced (t @ s) th" - proof - - have "the_preced (t @ s) th = Prc prio tm" - using h_t.th_kept preced_th by (simp add:the_preced_def) - moreover have "prio' \ prio" using Set h_e.set_diff_low by auto - ultimately show ?thesis by (insert lt_tm, auto simp:the_preced_def preced_def) - qed - ultimately show ?thesis - by (unfold Set, simp add:the_preced_def preced_def) - next - case False - then have "?f x = the_preced (t@s) x" - by (simp add:the_preced_def preced_def Set) - also have "... \ Max (the_preced (t@s) ` threads (t@s))" - using Set h h_t.finite_threads by auto - also have "... = ?f th" by (metis Cons.hyps(5) h_e.th_kept the_preced_def) - finally show ?thesis . - qed - qed - qed - also have "... = ?t" using h_e.th_kept the_preced_def by auto - finally show ?thesis . - qed - qed -qed - -lemma max_preced: "preced th (t@s) = Max (the_preced (t@s) ` (threads (t@s)))" - by (insert th_kept max_kept, auto) - -text {* - The reason behind the following lemma is that: - Since @{term "cp"} is defined as the maximum precedence - of those threads contained in the sub-tree of node @{term "Th th"} - in @{term "RAG (t@s)"}, and all these threads are living threads, and - @{term "th"} is also among them, the maximum precedence of - them all must be the one for @{text "th"}. -*} -lemma th_cp_max_preced: - "cp (t@s) th = Max (the_preced (t@s) ` (threads (t@s)))" (is "?L = ?R") -proof - - let ?f = "the_preced (t@s)" - have "?L = ?f th" - proof(unfold cp_alt_def, rule image_Max_eqI) - show "finite {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" - proof - - have "{th'. Th th' \ subtree (RAG (t @ s)) (Th th)} = - the_thread ` {n . n \ subtree (RAG (t @ s)) (Th th) \ - (\ th'. n = Th th')}" - by (smt Collect_cong Setcompr_eq_image mem_Collect_eq the_thread.simps) - moreover have "finite ..." by (simp add: vat_t.fsbtRAGs.finite_subtree) - ultimately show ?thesis by simp - qed - next - show "th \ {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" - by (auto simp:subtree_def) - next - show "\x\{th'. Th th' \ subtree (RAG (t @ s)) (Th th)}. - the_preced (t @ s) x \ the_preced (t @ s) th" - proof - fix th' - assume "th' \ {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" - hence "Th th' \ subtree (RAG (t @ s)) (Th th)" by auto - moreover have "... \ Field (RAG (t @ s)) \ {Th th}" - by (meson subtree_Field) - ultimately have "Th th' \ ..." by auto - hence "th' \ threads (t@s)" - proof - assume "Th th' \ {Th th}" - thus ?thesis using th_kept by auto - next - assume "Th th' \ Field (RAG (t @ s))" - thus ?thesis using vat_t.not_in_thread_isolated by blast - qed - thus "the_preced (t @ s) th' \ the_preced (t @ s) th" - by (metis Max_ge finite_imageI finite_threads image_eqI - max_kept th_kept the_preced_def) - qed - qed - also have "... = ?R" by (simp add: max_preced the_preced_def) - finally show ?thesis . -qed - -lemma th_cp_max[simp]: "Max (cp (t@s) ` threads (t@s)) = cp (t@s) th" - using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger - -lemma [simp]: "Max (cp (t@s) ` threads (t@s)) = Max (the_preced (t@s) ` threads (t@s))" - by (simp add: th_cp_max_preced) - -lemma [simp]: "Max (the_preced (t@s) ` threads (t@s)) = the_preced (t@s) th" - using max_kept th_kept the_preced_def by auto - -lemma [simp]: "the_preced (t@s) th = preced th (t@s)" - using the_preced_def by auto - -lemma [simp]: "preced th (t@s) = preced th s" - by (simp add: th_kept) - -lemma [simp]: "cp s th = preced th s" - by (simp add: eq_cp_s_th) - -lemma th_cp_preced [simp]: "cp (t@s) th = preced th s" - by (fold max_kept, unfold th_cp_max_preced, simp) - -lemma preced_less: - assumes th'_in: "th' \ threads s" - and neq_th': "th' \ th" - shows "preced th' s < preced th s" - using assms -by (metis Max.coboundedI finite_imageI highest not_le order.trans - preced_linorder rev_image_eqI threads_s vat_s.finite_threads - vat_s.le_cp) - -section {* The `blocking thread` *} - -text {* - - The purpose of PIP is to ensure that the most urgent thread @{term - th} is not blocked unreasonably. Therefore, below, we will derive - properties of the blocking thread. By blocking thread, we mean a - thread in running state t @ s, but is different from thread @{term - th}. - - The first lemmas shows that the @{term cp}-value of the blocking - thread @{text th'} equals to the highest precedence in the whole - system. - -*} - -lemma runing_preced_inversion: - assumes runing': "th' \ runing (t @ s)" - shows "cp (t @ s) th' = preced th s" -proof - - have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" - using assms by (unfold runing_def, auto) - also have "\ = preced th s" - by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) - finally show ?thesis . -qed - -text {* - - The next lemma shows how the counters for @{term "P"} and @{term - "V"} operations relate to the running threads in the states @{term - s} and @{term "t @ s"}: if a thread's @{term "P"}-count equals its - @{term "V"}-count (which means it no longer has any resource in its - possession), it cannot be a running thread. - - The proof is by contraction with the assumption @{text "th' \ th"}. - The key is the use of @{thm count_eq_dependants} to derive the - emptiness of @{text th'}s @{term dependants}-set from the balance of - its @{term P} and @{term V} counts. From this, it can be shown - @{text th'}s @{term cp}-value equals to its own precedence. - - On the other hand, since @{text th'} is running, by @{thm - runing_preced_inversion}, its @{term cp}-value equals to the - precedence of @{term th}. - - Combining the above two results we have that @{text th'} and @{term - th} have the same precedence. By uniqueness of precedences, we have - @{text "th' = th"}, which is in contradiction with the assumption - @{text "th' \ th"}. - -*} - -lemma eq_pv_blocked: (* ddd *) - assumes neq_th': "th' \ th" - and eq_pv: "cntP (t @ s) th' = cntV (t @ s) th'" - shows "th' \ runing (t @ s)" -proof - assume otherwise: "th' \ runing (t @ s)" - show False - proof - - have th'_in: "th' \ threads (t @ s)" - using otherwise readys_threads runing_def by auto - have "th' = th" - proof(rule preced_unique) - -- {* The proof goes like this: - it is first shown that the @{term preced}-value of @{term th'} - equals to that of @{term th}, then by uniqueness - of @{term preced}-values (given by lemma @{thm preced_unique}), - @{term th'} equals to @{term th}: *} - show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R") - proof - - -- {* Since the counts of @{term th'} are balanced, the subtree - of it contains only itself, so, its @{term cp}-value - equals its @{term preced}-value: *} - have "?L = cp (t @ s) th'" - by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp) - -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion}, - its @{term cp}-value equals @{term "preced th s"}, - which equals to @{term "?R"} by simplification: *} - also have "... = ?R" - using runing_preced_inversion[OF otherwise] by simp - finally show ?thesis . - qed - qed (auto simp: th'_in th_kept) - with `th' \ th` show ?thesis by simp - qed -qed - -text {* - The following lemma is the extrapolation of @{thm eq_pv_blocked}. - It says if a thread, different from @{term th}, - does not hold any resource at the very beginning, - it will keep hand-emptied in the future @{term "t@s"}. -*} -lemma eq_pv_persist: (* ddd *) - assumes neq_th': "th' \ th" - and eq_pv: "cntP s th' = cntV s th'" - shows "cntP (t @ s) th' = cntV (t @ s) th'" -proof(induction rule: ind) - -- {* The nontrivial case is for the @{term Cons}: *} - case (Cons e t) - -- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *} - interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp - interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp - show ?case - proof - - -- {* It can be proved that @{term cntP}-value of @{term th'} does not change - by the happening of event @{term e}: *} - have "cntP ((e#t)@s) th' = cntP (t@s) th'" - proof(rule ccontr) -- {* Proof by contradiction. *} - -- {* Suppose @{term cntP}-value of @{term th'} is changed by @{term e}: *} - assume otherwise: "cntP ((e # t) @ s) th' \ cntP (t @ s) th'" - -- {* Then the actor of @{term e} must be @{term th'} and @{term e} - must be a @{term P}-event: *} - hence "isP e" "actor e = th'" by (auto simp:cntP_diff_inv) - with vat_t.actor_inv[OF Cons(2)] - -- {* According to @{thm actor_inv}, @{term th'} must be running at - the moment @{term "t@s"}: *} - have "th' \ runing (t@s)" by (cases e, auto) - -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis - shows @{term th'} can not be running at moment @{term "t@s"}: *} - moreover have "th' \ runing (t@s)" - using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . - -- {* Contradiction is finally derived: *} - ultimately show False by simp - qed - -- {* It can also be proved that @{term cntV}-value of @{term th'} does not change - by the happening of event @{term e}: *} - -- {* The proof follows exactly the same pattern as the case for @{term cntP}-value: *} - moreover have "cntV ((e#t)@s) th' = cntV (t@s) th'" - proof(rule ccontr) -- {* Proof by contradiction. *} - assume otherwise: "cntV ((e # t) @ s) th' \ cntV (t @ s) th'" - hence "isV e" "actor e = th'" by (auto simp:cntV_diff_inv) - with vat_t.actor_inv[OF Cons(2)] - have "th' \ runing (t@s)" by (cases e, auto) - moreover have "th' \ runing (t@s)" - using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . - ultimately show False by simp - qed - -- {* Finally, it can be shown that the @{term cntP} and @{term cntV} - value for @{term th'} are still in balance, so @{term th'} - is still hand-emptied after the execution of event @{term e}: *} - ultimately show ?thesis using Cons(5) by metis - qed -qed (auto simp:eq_pv) - -text {* - - By combining @{thm eq_pv_blocked} and @{thm eq_pv_persist}, it can - be derived easily that @{term th'} can not be running in the future: - -*} - -lemma eq_pv_blocked_persist: - assumes neq_th': "th' \ th" - and eq_pv: "cntP s th' = cntV s th'" - shows "th' \ runing (t @ s)" - using assms - by (simp add: eq_pv_blocked eq_pv_persist) - -text {* - - The following lemma shows the blocking thread @{term th'} must hold - some resource in the very beginning. - -*} - -lemma runing_cntP_cntV_inv: (* ddd *) - assumes is_runing: "th' \ runing (t @ s)" - and neq_th': "th' \ th" - shows "cntP s th' > cntV s th'" - using assms -proof - - -- {* First, it can be shown that the number of @{term P} and - @{term V} operations can not be equal for thred @{term th'} *} - have "cntP s th' \ cntV s th'" - proof - -- {* The proof goes by contradiction, suppose otherwise: *} - assume otherwise: "cntP s th' = cntV s th'" - -- {* By applying @{thm eq_pv_blocked_persist} to this: *} - from eq_pv_blocked_persist[OF neq_th' otherwise] - -- {* we have that @{term th'} can not be running at moment @{term "t@s"}: *} - have "th' \ runing (t@s)" . - -- {* This is obvious in contradiction with assumption @{thm is_runing} *} - thus False using is_runing by simp - qed - -- {* However, the number of @{term V} is always less or equal to @{term P}: *} - moreover have "cntV s th' \ cntP s th'" using vat_s.cnp_cnv_cncs by auto - -- {* Thesis is finally derived by combining the these two results: *} - ultimately show ?thesis by auto -qed - - -text {* - - The following lemmas shows the blocking thread @{text th'} must be - live at the very beginning, i.e. the moment (or state) @{term s}. - The proof is a simple combination of the results above: - -*} - -lemma runing_threads_inv: - assumes runing': "th' \ runing (t@s)" - and neq_th': "th' \ th" - shows "th' \ threads s" -proof(rule ccontr) -- {* Proof by contradiction: *} - assume otherwise: "th' \ threads s" - have "th' \ runing (t @ s)" - proof - - from vat_s.cnp_cnv_eq[OF otherwise] - have "cntP s th' = cntV s th'" . - from eq_pv_blocked_persist[OF neq_th' this] - show ?thesis . - qed - with runing' show False by simp -qed - -text {* - - The following lemma summarises the above lemmas to give an overall - characterisationof the blocking thread @{text "th'"}: - -*} - -lemma runing_inversion: (* ddd, one of the main lemmas to present *) - assumes runing': "th' \ runing (t@s)" - and neq_th: "th' \ th" - shows "th' \ threads s" - and "\detached s th'" - and "cp (t@s) th' = preced th s" -proof - - from runing_threads_inv[OF assms] - show "th' \ threads s" . -next - from runing_cntP_cntV_inv[OF runing' neq_th] - show "\detached s th'" using vat_s.detached_eq by simp -next - from runing_preced_inversion[OF runing'] - show "cp (t@s) th' = preced th s" . -qed - - -section {* The existence of `blocking thread` *} - -text {* - - Suppose @{term th} is not running, it is first shown that there is a - path in RAG leading from node @{term th} to another thread @{text - "th'"} in the @{term readys}-set (So @{text "th'"} is an ancestor of - @{term th}}). - - Now, since @{term readys}-set is non-empty, there must be one in it - which holds the highest @{term cp}-value, which, by definition, is - the @{term runing}-thread. However, we are going to show more: this - running thread is exactly @{term "th'"}. - -*} - -lemma th_blockedE: (* ddd, the other main lemma to be presented: *) - assumes "th \ runing (t@s)" - obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" - "th' \ runing (t@s)" -proof - - -- {* According to @{thm vat_t.th_chain_to_ready}, either - @{term "th"} is in @{term "readys"} or there is path leading from it to - one thread in @{term "readys"}. *} - have "th \ readys (t @ s) \ (\th'. th' \ readys (t @ s) \ (Th th, Th th') \ (RAG (t @ s))\<^sup>+)" - using th_kept vat_t.th_chain_to_ready by auto - -- {* However, @{term th} can not be in @{term readys}, because otherwise, since - @{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *} - moreover have "th \ readys (t@s)" - using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto - -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in - term @{term readys}: *} - ultimately obtain th' where th'_in: "th' \ readys (t@s)" - and dp: "(Th th, Th th') \ (RAG (t @ s))\<^sup>+" by auto - -- {* We are going to show that this @{term th'} is running. *} - have "th' \ runing (t@s)" - proof - - -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *} - have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R") - proof - - have "?L = Max ((the_preced (t @ s) \ the_thread) ` subtree (tRAG (t @ s)) (Th th'))" - by (unfold cp_alt_def1, simp) - also have "... = (the_preced (t @ s) \ the_thread) (Th th)" - proof(rule image_Max_subset) - show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads) - next - show "subtree (tRAG (t @ s)) (Th th') \ Th ` threads (t @ s)" - by (metis Range.intros dp trancl_range vat_t.range_in vat_t.subtree_tRAG_thread) - next - show "Th th \ subtree (tRAG (t @ s)) (Th th')" using dp - by (unfold tRAG_subtree_eq, auto simp:subtree_def) - next - show "Max ((the_preced (t @ s) \ the_thread) ` Th ` threads (t @ s)) = - (the_preced (t @ s) \ the_thread) (Th th)" (is "Max ?L = _") - proof - - have "?L = the_preced (t @ s) ` threads (t @ s)" - by (unfold image_comp, rule image_cong, auto) - thus ?thesis using max_preced the_preced_def by auto - qed - qed - also have "... = ?R" - using th_cp_max th_cp_preced th_kept - the_preced_def vat_t.max_cp_readys_threads by auto - finally show ?thesis . - qed - -- {* Now, since @{term th'} holds the highest @{term cp} - and we have already show it is in @{term readys}, - it is @{term runing} by definition. *} - with `th' \ readys (t@s)` show ?thesis by (simp add: runing_def) - qed - -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *} - moreover have "Th th' \ ancestors (RAG (t @ s)) (Th th)" - using `(Th th, Th th') \ (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) - ultimately show ?thesis using that by metis -qed - -text {* - - Now it is easy to see there is always a thread to run by case - analysis on whether thread @{term th} is running: if the answer is - yes, the the running thread is obviously @{term th} itself; - otherwise, the running thread is the @{text th'} given by lemma - @{thm th_blockedE}. - -*} - -lemma live: "runing (t@s) \ {}" -proof(cases "th \ runing (t@s)") - case True thus ?thesis by auto -next - case False - thus ?thesis using th_blockedE by auto -qed - - -end -end diff -r 2056d9f481e2 -r ed938e2246b9 PrioG.thy~ --- a/PrioG.thy~ Thu Jan 28 16:36:46 2016 +0800 +++ b/PrioG.thy~ Thu Jan 28 21:14:17 2016 +0800 @@ -1,3628 +1,1611 @@ theory PrioG -imports PrioGDef RTree -begin - -locale valid_trace = - fixes s - assumes vt : "vt s" - -locale valid_trace_e = valid_trace + - fixes e - assumes vt_e: "vt (e#s)" -begin - -lemma pip_e: "PIP s e" - using vt_e by (cases, simp) - -end - -lemma runing_ready: - shows "runing s \ readys s" - unfolding runing_def readys_def - by auto - -lemma readys_threads: - shows "readys s \ threads s" - unfolding readys_def - by auto - -lemma wq_v_neq: - "cs \ cs' \ wq (V thread cs#s) cs' = wq s cs'" - by (auto simp:wq_def Let_def cp_def split:list.splits) - -context valid_trace +imports CpsG begin -lemma ind [consumes 0, case_names Nil Cons, induct type]: - assumes "PP []" - and "(\s e. valid_trace s \ valid_trace (e#s) \ - PP s \ PIP s e \ PP (e # s))" - shows "PP s" -proof(rule vt.induct[OF vt]) - from assms(1) show "PP []" . + +text {* + The following two auxiliary lemmas are used to reason about @{term Max}. +*} +lemma image_Max_eqI: + assumes "finite B" + and "b \ B" + and "\ x \ B. f x \ f b" + shows "Max (f ` B) = f b" + using assms + using Max_eqI by blast + +lemma image_Max_subset: + assumes "finite A" + and "B \ A" + and "a \ B" + and "Max (f ` A) = f a" + shows "Max (f ` B) = f a" +proof(rule image_Max_eqI) + show "finite B" + using assms(1) assms(2) finite_subset by auto next - fix s e - assume h: "vt s" "PP s" "PIP s e" - show "PP (e # s)" - proof(cases rule:assms(2)) - from h(1) show v1: "valid_trace s" by (unfold_locales, simp) - next - from h(1,3) have "vt (e#s)" by auto - thus "valid_trace (e # s)" by (unfold_locales, simp) - qed (insert h, auto) + show "a \ B" using assms by simp +next + show "\x\B. f x \ f a" + by (metis Max_ge assms(1) assms(2) assms(4) + finite_imageI image_eqI subsetCE) qed -lemma wq_distinct: "distinct (wq s cs)" -proof(rule ind, simp add:wq_def) - fix s e - assume h1: "step s e" - and h2: "distinct (wq s cs)" - thus "distinct (wq (e # s) cs)" - proof(induct rule:step.induct, auto simp: wq_def Let_def split:list.splits) - fix thread s - assume h1: "(Cs cs, Th thread) \ (RAG s)\<^sup>+" - and h2: "thread \ set (wq_fun (schs s) cs)" - and h3: "thread \ runing s" - show "False" - proof - - from h3 have "\ cs. thread \ set (wq_fun (schs s) cs) \ - thread = hd ((wq_fun (schs s) cs))" - by (simp add:runing_def readys_def s_waiting_def wq_def) - from this [OF h2] have "thread = hd (wq_fun (schs s) cs)" . - with h2 - have "(Cs cs, Th thread) \ (RAG s)" - by (simp add:s_RAG_def s_holding_def wq_def cs_holding_def) - with h1 show False by auto - qed - next - fix thread s a list - assume dst: "distinct list" - show "distinct (SOME q. distinct q \ set q = set list)" - proof(rule someI2) - from dst show "distinct list \ set list = set list" by auto - next - fix q assume "distinct q \ set q = set list" - thus "distinct q" by auto - qed - qed -qed +text {* + The following locale @{text "highest_gen"} sets the basic context for our + investigation: supposing thread @{text th} holds the highest @{term cp}-value + in state @{text s}, which means the task for @{text th} is the + most urgent. We want to show that + @{text th} is treated correctly by PIP, which means + @{text th} will not be blocked unreasonably by other less urgent + threads. +*} +locale highest_gen = + fixes s th prio tm + assumes vt_s: "vt s" + and threads_s: "th \ threads s" + and highest: "preced th s = Max ((cp s)`threads s)" + -- {* The internal structure of @{term th}'s precedence is exposed:*} + and preced_th: "preced th s = Prc prio tm" -end +-- {* @{term s} is a valid trace, so it will inherit all results derived for + a valid trace: *} +sublocale highest_gen < vat_s: valid_trace "s" + by (unfold_locales, insert vt_s, simp) - -context valid_trace_e +context highest_gen begin text {* - The following lemma shows that only the @{text "P"} - operation can add new thread into waiting queues. - Such kind of lemmas are very obvious, but need to be checked formally. - This is a kind of confirmation that our modelling is correct. + @{term tm} is the time when the precedence of @{term th} is set, so + @{term tm} must be a valid moment index into @{term s}. *} +lemma lt_tm: "tm < length s" + by (insert preced_tm_lt[OF threads_s preced_th], simp) -lemma block_pre: - assumes s_ni: "thread \ set (wq s cs)" - and s_i: "thread \ set (wq (e#s) cs)" - shows "e = P thread cs" +text {* + Since @{term th} holds the highest precedence and @{text "cp"} + is the highest precedence of all threads in the sub-tree of + @{text "th"} and @{text th} is among these threads, + its @{term cp} must equal to its precedence: +*} +lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R") proof - - show ?thesis - proof(cases e) - case (P th cs) - with assms - show ?thesis - by (auto simp:wq_def Let_def split:if_splits) - next - case (Create th prio) - with assms show ?thesis - by (auto simp:wq_def Let_def split:if_splits) - next - case (Exit th) - with assms show ?thesis - by (auto simp:wq_def Let_def split:if_splits) - next - case (Set th prio) - with assms show ?thesis - by (auto simp:wq_def Let_def split:if_splits) - next - case (V th cs) - with vt_e assms show ?thesis - apply (auto simp:wq_def Let_def split:if_splits) - proof - - fix q qs - assume h1: "thread \ set (wq_fun (schs s) cs)" - and h2: "q # qs = wq_fun (schs s) cs" - and h3: "thread \ set (SOME q. distinct q \ set q = set qs)" - and vt: "vt (V th cs # s)" - from h1 and h2[symmetric] have "thread \ set (q # qs)" by simp - moreover have "thread \ set qs" - proof - - have "set (SOME q. distinct q \ set q = set qs) = set qs" - proof(rule someI2) - from wq_distinct [of cs] - and h2[symmetric, folded wq_def] - show "distinct qs \ set qs = set qs" by auto - next - fix x assume "distinct x \ set x = set qs" - thus "set x = set qs" by auto - qed - with h3 show ?thesis by simp - qed - ultimately show "False" by auto - qed - qed + have "?L \ ?R" + by (unfold highest, rule Max_ge, + auto simp:threads_s finite_threads) + moreover have "?R \ ?L" + by (unfold vat_s.cp_rec, rule Max_ge, + auto simp:the_preced_def vat_s.fsbttRAGs.finite_children) + ultimately show ?thesis by auto qed +lemma highest_cp_preced: "cp s th = Max (the_preced s ` threads s)" + using eq_cp_s_th highest max_cp_eq the_preced_def by presburger + + +lemma highest_preced_thread: "preced th s = Max (the_preced s ` threads s)" + by (fold eq_cp_s_th, unfold highest_cp_preced, simp) + +lemma highest': "cp s th = Max (cp s ` threads s)" + by (simp add: eq_cp_s_th highest) + end -text {* - The following lemmas is also obvious and shallow. It says - that only running thread can request for a critical resource - and that the requested resource must be one which is - not current held by the thread. -*} - -lemma p_pre: "\vt ((P thread cs)#s)\ \ - thread \ runing s \ (Cs cs, Th thread) \ (RAG s)^+" -apply (ind_cases "vt ((P thread cs)#s)") -apply (ind_cases "step s (P thread cs)") -by auto +locale extend_highest_gen = highest_gen + + fixes t + assumes vt_t: "vt (t@s)" + and create_low: "Create th' prio' \ set t \ prio' \ prio" + and set_diff_low: "Set th' prio' \ set t \ th' \ th \ prio' \ prio" + and exit_diff: "Exit th' \ set t \ th' \ th" -lemma abs1: - assumes ein: "e \ set es" - and neq: "hd es \ hd (es @ [x])" - shows "False" -proof - - from ein have "es \ []" by auto - then obtain e ess where "es = e # ess" by (cases es, auto) - with neq show ?thesis by auto -qed - -lemma q_head: "Q (hd es) \ hd es = hd [th\es . Q th]" - by (cases es, auto) - -inductive_cases evt_cons: "vt (a#s)" - -context valid_trace_e -begin +sublocale extend_highest_gen < vat_t: valid_trace "t@s" + by (unfold_locales, insert vt_t, simp) -lemma abs2: - assumes inq: "thread \ set (wq s cs)" - and nh: "thread = hd (wq s cs)" - and qt: "thread \ hd (wq (e#s) cs)" - and inq': "thread \ set (wq (e#s) cs)" - shows "False" +lemma step_back_vt_app: + assumes vt_ts: "vt (t@s)" + shows "vt s" proof - - from vt_e assms show "False" - apply (cases e) - apply ((simp split:if_splits add:Let_def wq_def)[1])+ - apply (insert abs1, fast)[1] - apply (auto simp:wq_def simp:Let_def split:if_splits list.splits) - proof - - fix th qs - assume vt: "vt (V th cs # s)" - and th_in: "thread \ set (SOME q. distinct q \ set q = set qs)" - and eq_wq: "wq_fun (schs s) cs = thread # qs" - show "False" - proof - - from wq_distinct[of cs] - and eq_wq[folded wq_def] have "distinct (thread#qs)" by simp - moreover have "thread \ set qs" - proof - - have "set (SOME q. distinct q \ set q = set qs) = set qs" - proof(rule someI2) - from wq_distinct [of cs] - and eq_wq [folded wq_def] - show "distinct qs \ set qs = set qs" by auto - next - fix x assume "distinct x \ set x = set qs" - thus "set x = set qs" by auto - qed - with th_in show ?thesis by auto + from vt_ts show ?thesis + proof(induct t) + case Nil + from Nil show ?case by auto + next + case (Cons e t) + assume ih: " vt (t @ s) \ vt s" + and vt_et: "vt ((e # t) @ s)" + show ?case + proof(rule ih) + show "vt (t @ s)" + proof(rule step_back_vt) + from vt_et show "vt (e # t @ s)" by simp qed - ultimately show ?thesis by auto qed qed qed -end - -context valid_trace -begin +(* locale red_extend_highest_gen = extend_highest_gen + + fixes i::nat +*) -lemma vt_moment: "\ t. vt (moment t s)" -proof(induct rule:ind) - case Nil - thus ?case by (simp add:vt_nil) -next - case (Cons s e t) - show ?case - proof(cases "t \ length (e#s)") - case True - from True have "moment t (e#s) = e#s" by simp - thus ?thesis using Cons - by (simp add:valid_trace_def) - next - case False - from Cons have "vt (moment t s)" by simp - moreover have "moment t (e#s) = moment t s" - proof - - from False have "t \ length s" by simp - from moment_app [OF this, of "[e]"] - show ?thesis by simp - qed - ultimately show ?thesis by simp - qed -qed - -(* Wrong: - lemma \thread \ set (wq_fun cs1 s); thread \ set (wq_fun cs2 s)\ \ cs1 = cs2" +(* +sublocale red_extend_highest_gen < red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)" + apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric]) + apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp) + by (unfold highest_gen_def, auto dest:step_back_vt_app) *) -text {* (* ddd *) - The nature of the work is like this: since it starts from a very simple and basic - model, even intuitively very `basic` and `obvious` properties need to derived from scratch. - For instance, the fact - that one thread can not be blocked by two critical resources at the same time - is obvious, because only running threads can make new requests, if one is waiting for - a critical resource and get blocked, it can not make another resource request and get - blocked the second time (because it is not running). - - To derive this fact, one needs to prove by contraction and - reason about time (or @{text "moement"}). The reasoning is based on a generic theorem - named @{text "p_split"}, which is about status changing along the time axis. It says if - a condition @{text "Q"} is @{text "True"} at a state @{text "s"}, - but it was @{text "False"} at the very beginning, then there must exits a moment @{text "t"} - in the history of @{text "s"} (notice that @{text "s"} itself is essentially the history - of events leading to it), such that @{text "Q"} switched - from being @{text "False"} to @{text "True"} and kept being @{text "True"} - till the last moment of @{text "s"}. +context extend_highest_gen +begin - Suppose a thread @{text "th"} is blocked - on @{text "cs1"} and @{text "cs2"} in some state @{text "s"}, - since no thread is blocked at the very beginning, by applying - @{text "p_split"} to these two blocking facts, there exist - two moments @{text "t1"} and @{text "t2"} in @{text "s"}, such that - @{text "th"} got blocked on @{text "cs1"} and @{text "cs2"} - and kept on blocked on them respectively ever since. - - Without lose of generality, we assume @{text "t1"} is earlier than @{text "t2"}. - However, since @{text "th"} was blocked ever since memonent @{text "t1"}, so it was still - in blocked state at moment @{text "t2"} and could not - make any request and get blocked the second time: Contradiction. -*} - -lemma waiting_unique_pre: - assumes h11: "thread \ set (wq s cs1)" - and h12: "thread \ hd (wq s cs1)" - assumes h21: "thread \ set (wq s cs2)" - and h22: "thread \ hd (wq s cs2)" - and neq12: "cs1 \ cs2" - shows "False" + lemma ind [consumes 0, case_names Nil Cons, induct type]: + assumes + h0: "R []" + and h2: "\ e t. \vt (t@s); step (t@s) e; + extend_highest_gen s th prio tm t; + extend_highest_gen s th prio tm (e#t); R t\ \ R (e#t)" + shows "R t" proof - - let "?Q cs s" = "thread \ set (wq s cs) \ thread \ hd (wq s cs)" - from h11 and h12 have q1: "?Q cs1 s" by simp - from h21 and h22 have q2: "?Q cs2 s" by simp - have nq1: "\ ?Q cs1 []" by (simp add:wq_def) - have nq2: "\ ?Q cs2 []" by (simp add:wq_def) - from p_split [of "?Q cs1", OF q1 nq1] - obtain t1 where lt1: "t1 < length s" - and np1: "\(thread \ set (wq (moment t1 s) cs1) \ - thread \ hd (wq (moment t1 s) cs1))" - and nn1: "(\i'>t1. thread \ set (wq (moment i' s) cs1) \ - thread \ hd (wq (moment i' s) cs1))" by auto - from p_split [of "?Q cs2", OF q2 nq2] - obtain t2 where lt2: "t2 < length s" - and np2: "\(thread \ set (wq (moment t2 s) cs2) \ - thread \ hd (wq (moment t2 s) cs2))" - and nn2: "(\i'>t2. thread \ set (wq (moment i' s) cs2) \ - thread \ hd (wq (moment i' s) cs2))" by auto - show ?thesis - proof - - { - assume lt12: "t1 < t2" - let ?t3 = "Suc t2" - from lt2 have le_t3: "?t3 \ length s" by auto - from moment_plus [OF this] - obtain e where eq_m: "moment ?t3 s = e#moment t2 s" by auto - have "t2 < ?t3" by simp - from nn2 [rule_format, OF this] and eq_m - have h1: "thread \ set (wq (e#moment t2 s) cs2)" and - h2: "thread \ hd (wq (e#moment t2 s) cs2)" by auto - have "vt (e#moment t2 s)" - proof - - from vt_moment - have "vt (moment ?t3 s)" . - with eq_m show ?thesis by simp - qed - then interpret vt_e: valid_trace_e "moment t2 s" "e" - by (unfold_locales, auto, cases, simp) - have ?thesis - proof(cases "thread \ set (wq (moment t2 s) cs2)") - case True - from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)" - by auto - from vt_e.abs2 [OF True eq_th h2 h1] - show ?thesis by auto + from vt_t extend_highest_gen_axioms show ?thesis + proof(induct t) + from h0 show "R []" . + next + case (Cons e t') + assume ih: "\vt (t' @ s); extend_highest_gen s th prio tm t'\ \ R t'" + and vt_e: "vt ((e # t') @ s)" + and et: "extend_highest_gen s th prio tm (e # t')" + from vt_e and step_back_step have stp: "step (t'@s) e" by auto + from vt_e and step_back_vt have vt_ts: "vt (t'@s)" by auto + show ?case + proof(rule h2 [OF vt_ts stp _ _ _ ]) + show "R t'" + proof(rule ih) + from et show ext': "extend_highest_gen s th prio tm t'" + by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt) next - case False - from vt_e.block_pre[OF False h1] - have "e = P thread cs2" . - with vt_e.vt_e have "vt ((P thread cs2)# moment t2 s)" by simp - from p_pre [OF this] have "thread \ runing (moment t2 s)" by simp - with runing_ready have "thread \ readys (moment t2 s)" by auto - with nn1 [rule_format, OF lt12] - show ?thesis by (simp add:readys_def wq_def s_waiting_def, auto) - qed - } moreover { - assume lt12: "t2 < t1" - let ?t3 = "Suc t1" - from lt1 have le_t3: "?t3 \ length s" by auto - from moment_plus [OF this] - obtain e where eq_m: "moment ?t3 s = e#moment t1 s" by auto - have lt_t3: "t1 < ?t3" by simp - from nn1 [rule_format, OF this] and eq_m - have h1: "thread \ set (wq (e#moment t1 s) cs1)" and - h2: "thread \ hd (wq (e#moment t1 s) cs1)" by auto - have "vt (e#moment t1 s)" - proof - - from vt_moment - have "vt (moment ?t3 s)" . - with eq_m show ?thesis by simp - qed - then interpret vt_e: valid_trace_e "moment t1 s" e - by (unfold_locales, auto, cases, auto) - have ?thesis - proof(cases "thread \ set (wq (moment t1 s) cs1)") - case True - from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)" - by auto - from vt_e.abs2 True eq_th h2 h1 - show ?thesis by auto - next - case False - from vt_e.block_pre [OF False h1] - have "e = P thread cs1" . - with vt_e.vt_e have "vt ((P thread cs1)# moment t1 s)" by simp - from p_pre [OF this] have "thread \ runing (moment t1 s)" by simp - with runing_ready have "thread \ readys (moment t1 s)" by auto - with nn2 [rule_format, OF lt12] - show ?thesis by (simp add:readys_def wq_def s_waiting_def, auto) - qed - } moreover { - assume eqt12: "t1 = t2" - let ?t3 = "Suc t1" - from lt1 have le_t3: "?t3 \ length s" by auto - from moment_plus [OF this] - obtain e where eq_m: "moment ?t3 s = e#moment t1 s" by auto - have lt_t3: "t1 < ?t3" by simp - from nn1 [rule_format, OF this] and eq_m - have h1: "thread \ set (wq (e#moment t1 s) cs1)" and - h2: "thread \ hd (wq (e#moment t1 s) cs1)" by auto - have vt_e: "vt (e#moment t1 s)" - proof - - from vt_moment - have "vt (moment ?t3 s)" . - with eq_m show ?thesis by simp + from vt_ts show "vt (t' @ s)" . qed - then interpret vt_e: valid_trace_e "moment t1 s" e - by (unfold_locales, auto, cases, auto) - have ?thesis - proof(cases "thread \ set (wq (moment t1 s) cs1)") - case True - from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)" - by auto - from vt_e.abs2 [OF True eq_th h2 h1] - show ?thesis by auto - next - case False - from vt_e.block_pre [OF False h1] - have eq_e1: "e = P thread cs1" . - have lt_t3: "t1 < ?t3" by simp - with eqt12 have "t2 < ?t3" by simp - from nn2 [rule_format, OF this] and eq_m and eqt12 - have h1: "thread \ set (wq (e#moment t2 s) cs2)" and - h2: "thread \ hd (wq (e#moment t2 s) cs2)" by auto - show ?thesis - proof(cases "thread \ set (wq (moment t2 s) cs2)") - case True - from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)" - by auto - from vt_e and eqt12 have "vt (e#moment t2 s)" by simp - then interpret vt_e2: valid_trace_e "moment t2 s" e - by (unfold_locales, auto, cases, auto) - from vt_e2.abs2 [OF True eq_th h2 h1] - show ?thesis . - next - case False - have "vt (e#moment t2 s)" - proof - - from vt_moment eqt12 - have "vt (moment (Suc t2) s)" by auto - with eq_m eqt12 show ?thesis by simp - qed - then interpret vt_e2: valid_trace_e "moment t2 s" e - by (unfold_locales, auto, cases, auto) - from vt_e2.block_pre [OF False h1] - have "e = P thread cs2" . - with eq_e1 neq12 show ?thesis by auto - qed - qed - } ultimately show ?thesis by arith - qed -qed - -text {* - This lemma is a simple corrolary of @{text "waiting_unique_pre"}. -*} - -lemma waiting_unique: - assumes "waiting s th cs1" - and "waiting s th cs2" - shows "cs1 = cs2" -using waiting_unique_pre assms -unfolding wq_def s_waiting_def -by auto - -end - -(* not used *) -text {* - Every thread can only be blocked on one critical resource, - symmetrically, every critical resource can only be held by one thread. - This fact is much more easier according to our definition. -*} -lemma held_unique: - assumes "holding (s::event list) th1 cs" - and "holding s th2 cs" - shows "th1 = th2" - by (insert assms, unfold s_holding_def, auto) - - -lemma last_set_lt: "th \ threads s \ last_set th s < length s" - apply (induct s, auto) - by (case_tac a, auto split:if_splits) - -lemma last_set_unique: - "\last_set th1 s = last_set th2 s; th1 \ threads s; th2 \ threads s\ - \ th1 = th2" - apply (induct s, auto) - by (case_tac a, auto split:if_splits dest:last_set_lt) - -lemma preced_unique : - assumes pcd_eq: "preced th1 s = preced th2 s" - and th_in1: "th1 \ threads s" - and th_in2: " th2 \ threads s" - shows "th1 = th2" -proof - - from pcd_eq have "last_set th1 s = last_set th2 s" by (simp add:preced_def) - from last_set_unique [OF this th_in1 th_in2] - show ?thesis . -qed - -lemma preced_linorder: - assumes neq_12: "th1 \ th2" - and th_in1: "th1 \ threads s" - and th_in2: " th2 \ threads s" - shows "preced th1 s < preced th2 s \ preced th1 s > preced th2 s" -proof - - from preced_unique [OF _ th_in1 th_in2] and neq_12 - have "preced th1 s \ preced th2 s" by auto - thus ?thesis by auto -qed - -(* An aux lemma used later *) -lemma unique_minus: - fixes x y z r - assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" - and xy: "(x, y) \ r" - and xz: "(x, z) \ r^+" - and neq: "y \ z" - shows "(y, z) \ r^+" -proof - - from xz and neq show ?thesis - proof(induct) - case (base ya) - have "(x, ya) \ r" by fact - from unique [OF xy this] have "y = ya" . - with base show ?case by auto - next - case (step ya z) - show ?case - proof(cases "y = ya") - case True - from step True show ?thesis by simp - next - case False - from step False - show ?thesis by auto - qed - qed -qed - -lemma unique_base: - fixes r x y z - assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" - and xy: "(x, y) \ r" - and xz: "(x, z) \ r^+" - and neq_yz: "y \ z" - shows "(y, z) \ r^+" -proof - - from xz neq_yz show ?thesis - proof(induct) - case (base ya) - from xy unique base show ?case by auto - next - case (step ya z) - show ?case - proof(cases "y = ya") - case True - from True step show ?thesis by auto + next + from et show "extend_highest_gen s th prio tm (e # t')" . next - case False - from False step - have "(y, ya) \ r\<^sup>+" by auto - with step show ?thesis by auto + from et show ext': "extend_highest_gen s th prio tm t'" + by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt) qed qed qed -lemma unique_chain: - fixes r x y z - assumes unique: "\ a b c. \(a, b) \ r; (a, c) \ r\ \ b = c" - and xy: "(x, y) \ r^+" - and xz: "(x, z) \ r^+" - and neq_yz: "y \ z" - shows "(y, z) \ r^+ \ (z, y) \ r^+" + +lemma th_kept: "th \ threads (t @ s) \ + preced th (t@s) = preced th s" (is "?Q t") proof - - from xy xz neq_yz show ?thesis - proof(induct) - case (base y) - have h1: "(x, y) \ r" and h2: "(x, z) \ r\<^sup>+" and h3: "y \ z" using base by auto - from unique_base [OF _ h1 h2 h3] and unique show ?case by auto + show ?thesis + proof(induct rule:ind) + case Nil + from threads_s + show ?case + by auto next - case (step y za) + case (Cons e t) + interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto + interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto show ?case - proof(cases "y = z") - case True - from True step show ?thesis by auto + proof(cases e) + case (Create thread prio) + show ?thesis + proof - + from Cons and Create have "step (t@s) (Create thread prio)" by auto + hence "th \ thread" + proof(cases) + case thread_create + with Cons show ?thesis by auto + qed + hence "preced th ((e # t) @ s) = preced th (t @ s)" + by (unfold Create, auto simp:preced_def) + moreover note Cons + ultimately show ?thesis + by (auto simp:Create) + qed next - case False - from False step have "(y, z) \ r\<^sup>+ \ (z, y) \ r\<^sup>+" by auto - thus ?thesis - proof - assume "(z, y) \ r\<^sup>+" - with step have "(z, za) \ r\<^sup>+" by auto - thus ?thesis by auto - next - assume h: "(y, z) \ r\<^sup>+" - from step have yza: "(y, za) \ r" by simp - from step have "za \ z" by simp - from unique_minus [OF _ yza h this] and unique - have "(za, z) \ r\<^sup>+" by auto - thus ?thesis by auto + case (Exit thread) + from h_e.exit_diff and Exit + have neq_th: "thread \ th" by auto + with Cons + show ?thesis + by (unfold Exit, auto simp:preced_def) + next + case (P thread cs) + with Cons + show ?thesis + by (auto simp:P preced_def) + next + case (V thread cs) + with Cons + show ?thesis + by (auto simp:V preced_def) + next + case (Set thread prio') + show ?thesis + proof - + from h_e.set_diff_low and Set + have "th \ thread" by auto + hence "preced th ((e # t) @ s) = preced th (t @ s)" + by (unfold Set, auto simp:preced_def) + moreover note Cons + ultimately show ?thesis + by (auto simp:Set) qed qed qed qed text {* - The following three lemmas show that @{text "RAG"} does not change - by the happening of @{text "Set"}, @{text "Create"} and @{text "Exit"} - events, respectively. -*} - -lemma RAG_set_unchanged: "(RAG (Set th prio # s)) = RAG s" -apply (unfold s_RAG_def s_waiting_def wq_def) -by (simp add:Let_def) + According to @{thm th_kept}, thread @{text "th"} has its living status + and precedence kept along the way of @{text "t"}. The following lemma + shows that this preserved precedence of @{text "th"} remains as the highest + along the way of @{text "t"}. -lemma RAG_create_unchanged: "(RAG (Create th prio # s)) = RAG s" -apply (unfold s_RAG_def s_waiting_def wq_def) -by (simp add:Let_def) - -lemma RAG_exit_unchanged: "(RAG (Exit th # s)) = RAG s" -apply (unfold s_RAG_def s_waiting_def wq_def) -by (simp add:Let_def) + The proof goes by induction over @{text "t"} using the specialized + induction rule @{thm ind}, followed by case analysis of each possible + operations of PIP. All cases follow the same pattern rendered by the + generalized introduction rule @{thm "image_Max_eqI"}. - -text {* - The following lemmas are used in the proof of - lemma @{text "step_RAG_v"}, which characterizes how the @{text "RAG"} is changed - by @{text "V"}-events. - However, since our model is very concise, such seemingly obvious lemmas need to be derived from scratch, - starting from the model definitions. + The very essence is to show that precedences, no matter whether they + are newly introduced or modified, are always lower than the one held + by @{term "th"}, which by @{thm th_kept} is preserved along the way. *} -lemma step_v_hold_inv[elim_format]: - "\c t. \vt (V th cs # s); - \ holding (wq s) t c; holding (wq (V th cs # s)) t c\ \ - next_th s th cs t \ c = cs" -proof - - fix c t - assume vt: "vt (V th cs # s)" - and nhd: "\ holding (wq s) t c" - and hd: "holding (wq (V th cs # s)) t c" - show "next_th s th cs t \ c = cs" - proof(cases "c = cs") - case False - with nhd hd show ?thesis - by (unfold cs_holding_def wq_def, auto simp:Let_def) - next - case True - with step_back_step [OF vt] - have "step s (V th c)" by simp - hence "next_th s th cs t" - proof(cases) - assume "holding s th c" - with nhd hd show ?thesis - apply (unfold s_holding_def cs_holding_def wq_def next_th_def, - auto simp:Let_def split:list.splits if_splits) - proof - - assume " hd (SOME q. distinct q \ q = []) \ set (SOME q. distinct q \ q = [])" - moreover have "\ = set []" - proof(rule someI2) - show "distinct [] \ [] = []" by auto +lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s" +proof(induct rule:ind) + case Nil + from highest_preced_thread + show ?case by simp +next + case (Cons e t) + interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto + interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto + show ?case + proof(cases e) + case (Create thread prio') + show ?thesis (is "Max (?f ` ?A) = ?t") + proof - + -- {* The following is the common pattern of each branch of the case analysis. *} + -- {* The major part is to show that @{text "th"} holds the highest precedence: *} + have "Max (?f ` ?A) = ?f th" + proof(rule image_Max_eqI) + show "finite ?A" using h_e.finite_threads by auto + next + show "th \ ?A" using h_e.th_kept by auto + next + show "\x\?A. ?f x \ ?f th" + proof + fix x + assume "x \ ?A" + hence "x = thread \ x \ threads (t@s)" by (auto simp:Create) + thus "?f x \ ?f th" + proof + assume "x = thread" + thus ?thesis + apply (simp add:Create the_preced_def preced_def, fold preced_def) + using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 + preced_th by force next - fix x assume "distinct x \ x = []" - thus "set x = set []" by auto + assume h: "x \ threads (t @ s)" + from Cons(2)[unfolded Create] + have "x \ thread" using h by (cases, auto) + hence "?f x = the_preced (t@s) x" + by (simp add:Create the_preced_def preced_def) + hence "?f x \ Max (the_preced (t@s) ` threads (t@s))" + by (simp add: h_t.finite_threads h) + also have "... = ?f th" + by (metis Cons.hyps(5) h_e.th_kept the_preced_def) + finally show ?thesis . qed - ultimately show False by auto - next - assume " hd (SOME q. distinct q \ q = []) \ set (SOME q. distinct q \ q = [])" - moreover have "\ = set []" - proof(rule someI2) - show "distinct [] \ [] = []" by auto - next - fix x assume "distinct x \ x = []" - thus "set x = set []" by auto - qed - ultimately show False by auto qed - qed - with True show ?thesis by auto - qed -qed - -text {* - The following @{text "step_v_wait_inv"} is also an obvious lemma, which, however, needs to be - derived from scratch, which confirms the correctness of the definition of @{text "next_th"}. -*} -lemma step_v_wait_inv[elim_format]: - "\t c. \vt (V th cs # s); \ waiting (wq (V th cs # s)) t c; waiting (wq s) t c - \ - \ (next_th s th cs t \ cs = c)" -proof - - fix t c - assume vt: "vt (V th cs # s)" - and nw: "\ waiting (wq (V th cs # s)) t c" - and wt: "waiting (wq s) t c" - from vt interpret vt_v: valid_trace_e s "V th cs" - by (cases, unfold_locales, simp) - show "next_th s th cs t \ cs = c" - proof(cases "cs = c") - case False - with nw wt show ?thesis - by (auto simp:cs_waiting_def wq_def Let_def) - next - case True - from nw[folded True] wt[folded True] - have "next_th s th cs t" - apply (unfold next_th_def, auto simp:cs_waiting_def wq_def Let_def split:list.splits) + qed + -- {* The minor part is to show that the precedence of @{text "th"} + equals to preserved one, given by the foregoing lemma @{thm th_kept} *} + also have "... = ?t" using h_e.th_kept the_preced_def by auto + -- {* Then it follows trivially that the precedence preserved + for @{term "th"} remains the maximum of all living threads along the way. *} + finally show ?thesis . + qed + next + case (Exit thread) + show ?thesis (is "Max (?f ` ?A) = ?t") proof - - fix a list - assume t_in: "t \ set list" - and t_ni: "t \ set (SOME q. distinct q \ set q = set list)" - and eq_wq: "wq_fun (schs s) cs = a # list" - have " set (SOME q. distinct q \ set q = set list) = set list" - proof(rule someI2) - from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def] - show "distinct list \ set list = set list" by auto + have "Max (?f ` ?A) = ?f th" + proof(rule image_Max_eqI) + show "finite ?A" using h_e.finite_threads by auto + next + show "th \ ?A" using h_e.th_kept by auto next - show "\x. distinct x \ set x = set list \ set x = set list" - by auto + show "\x\?A. ?f x \ ?f th" + proof + fix x + assume "x \ ?A" + hence "x \ threads (t@s)" by (simp add: Exit) + hence "?f x \ Max (?f ` threads (t@s))" + by (simp add: h_t.finite_threads) + also have "... \ ?f th" + apply (simp add:Exit the_preced_def preced_def, fold preced_def) + using Cons.hyps(5) h_t.th_kept the_preced_def by auto + finally show "?f x \ ?f th" . + qed qed - with t_ni and t_in show "a = th" by auto - next - fix a list - assume t_in: "t \ set list" - and t_ni: "t \ set (SOME q. distinct q \ set q = set list)" - and eq_wq: "wq_fun (schs s) cs = a # list" - have " set (SOME q. distinct q \ set q = set list) = set list" - proof(rule someI2) - from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def] - show "distinct list \ set list = set list" by auto + also have "... = ?t" using h_e.th_kept the_preced_def by auto + finally show ?thesis . + qed + next + case (P thread cs) + with Cons + show ?thesis by (auto simp:preced_def the_preced_def) + next + case (V thread cs) + with Cons + show ?thesis by (auto simp:preced_def the_preced_def) + next + case (Set thread prio') + show ?thesis (is "Max (?f ` ?A) = ?t") + proof - + have "Max (?f ` ?A) = ?f th" + proof(rule image_Max_eqI) + show "finite ?A" using h_e.finite_threads by auto + next + show "th \ ?A" using h_e.th_kept by auto next - show "\x. distinct x \ set x = set list \ set x = set list" - by auto + show "\x\?A. ?f x \ ?f th" + proof + fix x + assume h: "x \ ?A" + show "?f x \ ?f th" + proof(cases "x = thread") + case True + moreover have "the_preced (Set thread prio' # t @ s) thread \ the_preced (t @ s) th" + proof - + have "the_preced (t @ s) th = Prc prio tm" + using h_t.th_kept preced_th by (simp add:the_preced_def) + moreover have "prio' \ prio" using Set h_e.set_diff_low by auto + ultimately show ?thesis by (insert lt_tm, auto simp:the_preced_def preced_def) + qed + ultimately show ?thesis + by (unfold Set, simp add:the_preced_def preced_def) + next + case False + then have "?f x = the_preced (t@s) x" + by (simp add:the_preced_def preced_def Set) + also have "... \ Max (the_preced (t@s) ` threads (t@s))" + using Set h h_t.finite_threads by auto + also have "... = ?f th" by (metis Cons.hyps(5) h_e.th_kept the_preced_def) + finally show ?thesis . + qed + qed qed - with t_ni and t_in show "t = hd (SOME q. distinct q \ set q = set list)" by auto - next - fix a list - assume eq_wq: "wq_fun (schs s) cs = a # list" - from step_back_step[OF vt] - show "a = th" - proof(cases) - assume "holding s th cs" - with eq_wq show ?thesis - by (unfold s_holding_def wq_def, auto) - qed - qed - with True show ?thesis by simp + also have "... = ?t" using h_e.th_kept the_preced_def by auto + finally show ?thesis . + qed qed qed -lemma step_v_not_wait[consumes 3]: - "\vt (V th cs # s); next_th s th cs t; waiting (wq (V th cs # s)) t cs\ \ False" - by (unfold next_th_def cs_waiting_def wq_def, auto simp:Let_def) +lemma max_preced: "preced th (t@s) = Max (the_preced (t@s) ` (threads (t@s)))" + by (insert th_kept max_kept, auto) -lemma step_v_release: - "\vt (V th cs # s); holding (wq (V th cs # s)) th cs\ \ False" +text {* + The reason behind the following lemma is that: + Since @{term "cp"} is defined as the maximum precedence + of those threads contained in the sub-tree of node @{term "Th th"} + in @{term "RAG (t@s)"}, and all these threads are living threads, and + @{term "th"} is also among them, the maximum precedence of + them all must be the one for @{text "th"}. +*} +lemma th_cp_max_preced: + "cp (t@s) th = Max (the_preced (t@s) ` (threads (t@s)))" (is "?L = ?R") proof - - assume vt: "vt (V th cs # s)" - and hd: "holding (wq (V th cs # s)) th cs" - from vt interpret vt_v: valid_trace_e s "V th cs" - by (cases, unfold_locales, simp+) - from step_back_step [OF vt] and hd - show "False" - proof(cases) - assume "holding (wq (V th cs # s)) th cs" and "holding s th cs" - thus ?thesis - apply (unfold s_holding_def wq_def cs_holding_def) - apply (auto simp:Let_def split:list.splits) + let ?f = "the_preced (t@s)" + have "?L = ?f th" + proof(unfold cp_alt_def, rule image_Max_eqI) + show "finite {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" proof - - fix list - assume eq_wq[folded wq_def]: - "wq_fun (schs s) cs = hd (SOME q. distinct q \ set q = set list) # list" - and hd_in: "hd (SOME q. distinct q \ set q = set list) - \ set (SOME q. distinct q \ set q = set list)" - have "set (SOME q. distinct q \ set q = set list) = set list" - proof(rule someI2) - from vt_v.wq_distinct[of cs] and eq_wq - show "distinct list \ set list = set list" by auto - next - show "\x. distinct x \ set x = set list \ set x = set list" - by auto - qed - moreover have "distinct (hd (SOME q. distinct q \ set q = set list) # list)" - proof - - from vt_v.wq_distinct[of cs] and eq_wq - show ?thesis by auto - qed - moreover note eq_wq and hd_in - ultimately show "False" by auto - qed - qed -qed - -lemma step_v_get_hold: - "\th'. \vt (V th cs # s); \ holding (wq (V th cs # s)) th' cs; next_th s th cs th'\ \ False" - apply (unfold cs_holding_def next_th_def wq_def, - auto simp:Let_def) -proof - - fix rest - assume vt: "vt (V th cs # s)" - and eq_wq[folded wq_def]: " wq_fun (schs s) cs = th # rest" - and nrest: "rest \ []" - and ni: "hd (SOME q. distinct q \ set q = set rest) - \ set (SOME q. distinct q \ set q = set rest)" - from vt interpret vt_v: valid_trace_e s "V th cs" - by (cases, unfold_locales, simp+) - have "(SOME q. distinct q \ set q = set rest) \ []" - proof(rule someI2) - from vt_v.wq_distinct[of cs] and eq_wq - show "distinct rest \ set rest = set rest" by auto - next - fix x assume "distinct x \ set x = set rest" - hence "set x = set rest" by auto - with nrest - show "x \ []" by (case_tac x, auto) - qed - with ni show "False" by auto -qed - -lemma step_v_release_inv[elim_format]: -"\c t. \vt (V th cs # s); \ holding (wq (V th cs # s)) t c; holding (wq s) t c\ \ - c = cs \ t = th" - apply (unfold cs_holding_def wq_def, auto simp:Let_def split:if_splits list.splits) - proof - - fix a list - assume vt: "vt (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list" - from step_back_step [OF vt] show "a = th" - proof(cases) - assume "holding s th cs" with eq_wq - show ?thesis - by (unfold s_holding_def wq_def, auto) + have "{th'. Th th' \ subtree (RAG (t @ s)) (Th th)} = + the_thread ` {n . n \ subtree (RAG (t @ s)) (Th th) \ + (\ th'. n = Th th')}" + by (smt Collect_cong Setcompr_eq_image mem_Collect_eq the_thread.simps) + moreover have "finite ..." by (simp add: vat_t.fsbtRAGs.finite_subtree) + ultimately show ?thesis by simp qed next - fix a list - assume vt: "vt (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list" - from step_back_step [OF vt] show "a = th" - proof(cases) - assume "holding s th cs" with eq_wq - show ?thesis - by (unfold s_holding_def wq_def, auto) + show "th \ {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" + by (auto simp:subtree_def) + next + show "\x\{th'. Th th' \ subtree (RAG (t @ s)) (Th th)}. + the_preced (t @ s) x \ the_preced (t @ s) th" + proof + fix th' + assume "th' \ {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" + hence "Th th' \ subtree (RAG (t @ s)) (Th th)" by auto + moreover have "... \ Field (RAG (t @ s)) \ {Th th}" + by (meson subtree_Field) + ultimately have "Th th' \ ..." by auto + hence "th' \ threads (t@s)" + proof + assume "Th th' \ {Th th}" + thus ?thesis using th_kept by auto + next + assume "Th th' \ Field (RAG (t @ s))" + thus ?thesis using vat_t.not_in_thread_isolated by blast + qed + thus "the_preced (t @ s) th' \ the_preced (t @ s) th" + by (metis Max_ge finite_imageI finite_threads image_eqI + max_kept th_kept the_preced_def) qed qed + also have "... = ?R" by (simp add: max_preced the_preced_def) + finally show ?thesis . +qed -lemma step_v_waiting_mono: - "\t c. \vt (V th cs # s); waiting (wq (V th cs # s)) t c\ \ waiting (wq s) t c" +lemma th_cp_max[simp]: "Max (cp (t@s) ` threads (t@s)) = cp (t@s) th" + using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger + +lemma [simp]: "Max (cp (t@s) ` threads (t@s)) = Max (the_preced (t@s) ` threads (t@s))" + by (simp add: th_cp_max_preced) + +lemma [simp]: "Max (the_preced (t@s) ` threads (t@s)) = the_preced (t@s) th" + using max_kept th_kept the_preced_def by auto + +lemma [simp]: "the_preced (t@s) th = preced th (t@s)" + using the_preced_def by auto + +lemma [simp]: "preced th (t@s) = preced th s" + by (simp add: th_kept) + +lemma [simp]: "cp s th = preced th s" + by (simp add: eq_cp_s_th) + +lemma th_cp_preced [simp]: "cp (t@s) th = preced th s" + by (fold max_kept, unfold th_cp_max_preced, simp) + +lemma preced_less: + assumes th'_in: "th' \ threads s" + and neq_th': "th' \ th" + shows "preced th' s < preced th s" + using assms +by (metis Max.coboundedI finite_imageI highest not_le order.trans + preced_linorder rev_image_eqI threads_s vat_s.finite_threads + vat_s.le_cp) + +section {* The `blocking thread` *} + +text {* + The purpose of PIP is to ensure that the most + urgent thread @{term th} is not blocked unreasonably. + Therefore, a clear picture of the blocking thread is essential + to assure people that the purpose is fulfilled. + + In this section, we are going to derive a series of lemmas + with finally give rise to a picture of the blocking thread. + + By `blocking thread`, we mean a thread in running state but + different from thread @{term th}. +*} + +text {* + The following lemmas shows that the @{term cp}-value + of the blocking thread @{text th'} equals to the highest + precedence in the whole system. +*} +lemma runing_preced_inversion: + assumes runing': "th' \ runing (t@s)" + shows "cp (t@s) th' = preced th s" (is "?L = ?R") proof - - fix t c - let ?s' = "(V th cs # s)" - assume vt: "vt ?s'" - and wt: "waiting (wq ?s') t c" - from vt interpret vt_v: valid_trace_e s "V th cs" - by (cases, unfold_locales, simp+) - show "waiting (wq s) t c" - proof(cases "c = cs") - case False - assume neq_cs: "c \ cs" - hence "waiting (wq ?s') t c = waiting (wq s) t c" - by (unfold cs_waiting_def wq_def, auto simp:Let_def) - with wt show ?thesis by simp - next - case True - with wt show ?thesis - apply (unfold cs_waiting_def wq_def, auto simp:Let_def split:list.splits) - proof - - fix a list - assume not_in: "t \ set list" - and is_in: "t \ set (SOME q. distinct q \ set q = set list)" - and eq_wq: "wq_fun (schs s) cs = a # list" - have "set (SOME q. distinct q \ set q = set list) = set list" - proof(rule someI2) - from vt_v.wq_distinct [of cs] - and eq_wq[folded wq_def] - show "distinct list \ set list = set list" by auto - next - fix x assume "distinct x \ set x = set list" - thus "set x = set list" by auto + have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms + by (unfold runing_def, auto) + also have "\ = ?R" + by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) + finally show ?thesis . +qed + +text {* + + The following lemma shows how the counters for @{term "P"} and + @{term "V"} operations relate to the running threads in the states + @{term s} and @{term "t @ s"}. The lemma shows that if a thread's + @{term "P"}-count equals its @{term "V"}-count (which means it no + longer has any resource in its possession), it cannot be a running + thread. + + The proof is by contraction with the assumption @{text "th' \ th"}. + The key is the use of @{thm count_eq_dependants} to derive the + emptiness of @{text th'}s @{term dependants}-set from the balance of + its @{term P} and @{term V} counts. From this, it can be shown + @{text th'}s @{term cp}-value equals to its own precedence. + + On the other hand, since @{text th'} is running, by @{thm + runing_preced_inversion}, its @{term cp}-value equals to the + precedence of @{term th}. + + Combining the above two resukts we have that @{text th'} and @{term + th} have the same precedence. By uniqueness of precedences, we have + @{text "th' = th"}, which is in contradiction with the assumption + @{text "th' \ th"}. + +*} + +lemma eq_pv_blocked: (* ddd *) + assumes neq_th': "th' \ th" + and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" + shows "th' \ runing (t@s)" +proof + assume otherwise: "th' \ runing (t@s)" + show False + proof - + have th'_in: "th' \ threads (t@s)" + using otherwise readys_threads runing_def by auto + have "th' = th" + proof(rule preced_unique) + -- {* The proof goes like this: + it is first shown that the @{term preced}-value of @{term th'} + equals to that of @{term th}, then by uniqueness + of @{term preced}-values (given by lemma @{thm preced_unique}), + @{term th'} equals to @{term th}: *} + show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R") + proof - + -- {* Since the counts of @{term th'} are balanced, the subtree + of it contains only itself, so, its @{term cp}-value + equals its @{term preced}-value: *} + have "?L = cp (t@s) th'" + by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp) + -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion}, + its @{term cp}-value equals @{term "preced th s"}, + which equals to @{term "?R"} by simplification: *} + also have "... = ?R" + thm runing_preced_inversion + using runing_preced_inversion[OF otherwise] by simp + finally show ?thesis . qed - with not_in is_in show "t = a" by auto - next - fix list - assume is_waiting: "waiting (wq (V th cs # s)) t cs" - and eq_wq: "wq_fun (schs s) cs = t # list" - hence "t \ set list" - apply (unfold wq_def, auto simp:Let_def cs_waiting_def) - proof - - assume " t \ set (SOME q. distinct q \ set q = set list)" - moreover have "\ = set list" - proof(rule someI2) - from vt_v.wq_distinct [of cs] - and eq_wq[folded wq_def] - show "distinct list \ set list = set list" by auto - next - fix x assume "distinct x \ set x = set list" - thus "set x = set list" by auto - qed - ultimately show "t \ set list" by simp - qed - with eq_wq and vt_v.wq_distinct [of cs, unfolded wq_def] - show False by auto - qed - qed + qed (auto simp: th'_in th_kept) + with `th' \ th` show ?thesis by simp + qed qed -text {* (* ddd *) - The following @{text "step_RAG_v"} lemma charaterizes how @{text "RAG"} is changed - with the happening of @{text "V"}-events: +text {* + The following lemma is the extrapolation of @{thm eq_pv_blocked}. + It says if a thread, different from @{term th}, + does not hold any resource at the very beginning, + it will keep hand-emptied in the future @{term "t@s"}. +*} +lemma eq_pv_persist: (* ddd *) + assumes neq_th': "th' \ th" + and eq_pv: "cntP s th' = cntV s th'" + shows "cntP (t@s) th' = cntV (t@s) th'" +proof(induction rule:ind) -- {* The proof goes by induction. *} + -- {* The nontrivial case is for the @{term Cons}: *} + case (Cons e t) + -- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *} + interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp + interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp + show ?case + proof - + -- {* It can be proved that @{term cntP}-value of @{term th'} does not change + by the happening of event @{term e}: *} + have "cntP ((e#t)@s) th' = cntP (t@s) th'" + proof(rule ccontr) -- {* Proof by contradiction. *} + -- {* Suppose @{term cntP}-value of @{term th'} is changed by @{term e}: *} + assume otherwise: "cntP ((e # t) @ s) th' \ cntP (t @ s) th'" + -- {* Then the actor of @{term e} must be @{term th'} and @{term e} + must be a @{term P}-event: *} + hence "isP e" "actor e = th'" by (auto simp:cntP_diff_inv) + with vat_t.actor_inv[OF Cons(2)] + -- {* According to @{thm actor_inv}, @{term th'} must be running at + the moment @{term "t@s"}: *} + have "th' \ runing (t@s)" by (cases e, auto) + -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis + shows @{term th'} can not be running at moment @{term "t@s"}: *} + moreover have "th' \ runing (t@s)" + using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . + -- {* Contradiction is finally derived: *} + ultimately show False by simp + qed + -- {* It can also be proved that @{term cntV}-value of @{term th'} does not change + by the happening of event @{term e}: *} + -- {* The proof follows exactly the same pattern as the case for @{term cntP}-value: *} + moreover have "cntV ((e#t)@s) th' = cntV (t@s) th'" + proof(rule ccontr) -- {* Proof by contradiction. *} + assume otherwise: "cntV ((e # t) @ s) th' \ cntV (t @ s) th'" + hence "isV e" "actor e = th'" by (auto simp:cntV_diff_inv) + with vat_t.actor_inv[OF Cons(2)] + have "th' \ runing (t@s)" by (cases e, auto) + moreover have "th' \ runing (t@s)" + using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . + ultimately show False by simp + qed + -- {* Finally, it can be shown that the @{term cntP} and @{term cntV} + value for @{term th'} are still in balance, so @{term th'} + is still hand-emptied after the execution of event @{term e}: *} + ultimately show ?thesis using Cons(5) by metis + qed +qed (auto simp:eq_pv) + +text {* + By combining @{thm eq_pv_blocked} and @{thm eq_pv_persist}, + it can be derived easily that @{term th'} can not be running in the future: *} -lemma step_RAG_v: -fixes th::thread -assumes vt: - "vt (V th cs#s)" -shows " - RAG (V th cs # s) = - RAG s - {(Cs cs, Th th)} - - {(Th th', Cs cs) |th'. next_th s th cs th'} \ - {(Cs cs, Th th') |th'. next_th s th cs th'}" - apply (insert vt, unfold s_RAG_def) - apply (auto split:if_splits list.splits simp:Let_def) - apply (auto elim: step_v_waiting_mono step_v_hold_inv - step_v_release step_v_wait_inv - step_v_get_hold step_v_release_inv) - apply (erule_tac step_v_not_wait, auto) - done +lemma eq_pv_blocked_persist: + assumes neq_th': "th' \ th" + and eq_pv: "cntP s th' = cntV s th'" + shows "th' \ runing (t@s)" + using assms + by (simp add: eq_pv_blocked eq_pv_persist) + +text {* + The following lemma shows the blocking thread @{term th'} + must hold some resource in the very beginning. +*} +lemma runing_cntP_cntV_inv: (* ddd *) + assumes is_runing: "th' \ runing (t@s)" + and neq_th': "th' \ th" + shows "cntP s th' > cntV s th'" + using assms +proof - + -- {* First, it can be shown that the number of @{term P} and + @{term V} operations can not be equal for thred @{term th'} *} + have "cntP s th' \ cntV s th'" + proof + -- {* The proof goes by contradiction, suppose otherwise: *} + assume otherwise: "cntP s th' = cntV s th'" + -- {* By applying @{thm eq_pv_blocked_persist} to this: *} + from eq_pv_blocked_persist[OF neq_th' otherwise] + -- {* we have that @{term th'} can not be running at moment @{term "t@s"}: *} + have "th' \ runing (t@s)" . + -- {* This is obvious in contradiction with assumption @{thm is_runing} *} + thus False using is_runing by simp + qed + -- {* However, the number of @{term V} is always less or equal to @{term P}: *} + moreover have "cntV s th' \ cntP s th'" using vat_s.cnp_cnv_cncs by auto + -- {* Thesis is finally derived by combining the these two results: *} + ultimately show ?thesis by auto +qed + + +text {* + The following lemmas shows the blocking thread @{text th'} must be live + at the very beginning, i.e. the moment (or state) @{term s}. + + The proof is a simple combination of the results above: +*} +lemma runing_threads_inv: + assumes runing': "th' \ runing (t@s)" + and neq_th': "th' \ th" + shows "th' \ threads s" +proof(rule ccontr) -- {* Proof by contradiction: *} + assume otherwise: "th' \ threads s" + have "th' \ runing (t @ s)" + proof - + from vat_s.cnp_cnv_eq[OF otherwise] + have "cntP s th' = cntV s th'" . + from eq_pv_blocked_persist[OF neq_th' this] + show ?thesis . + qed + with runing' show False by simp +qed + +text {* + The following lemma summarizes several foregoing + lemmas to give an overall picture of the blocking thread @{text "th'"}: +*} +lemma runing_inversion: (* ddd, one of the main lemmas to present *) + assumes runing': "th' \ runing (t@s)" + and neq_th: "th' \ th" + shows "th' \ threads s" + and "\detached s th'" + and "cp (t@s) th' = preced th s" +proof - + from runing_threads_inv[OF assms] + show "th' \ threads s" . +next + from runing_cntP_cntV_inv[OF runing' neq_th] + show "\detached s th'" using vat_s.detached_eq by simp +next + from runing_preced_inversion[OF runing'] + show "cp (t@s) th' = preced th s" . +qed + +section {* The existence of `blocking thread` *} text {* - The following @{text "step_RAG_p"} lemma charaterizes how @{text "RAG"} is changed - with the happening of @{text "P"}-events: + Suppose @{term th} is not running, it is first shown that + there is a path in RAG leading from node @{term th} to another thread @{text "th'"} + in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}). + + Now, since @{term readys}-set is non-empty, there must be + one in it which holds the highest @{term cp}-value, which, by definition, + is the @{term runing}-thread. However, we are going to show more: this running thread + is exactly @{term "th'"}. + *} +lemma th_blockedE: (* ddd, the other main lemma to be presented: *) + assumes "th \ runing (t@s)" + obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" + "th' \ runing (t@s)" +proof - + -- {* According to @{thm vat_t.th_chain_to_ready}, either + @{term "th"} is in @{term "readys"} or there is path leading from it to + one thread in @{term "readys"}. *} + have "th \ readys (t @ s) \ (\th'. th' \ readys (t @ s) \ (Th th, Th th') \ (RAG (t @ s))\<^sup>+)" + using th_kept vat_t.th_chain_to_ready by auto + -- {* However, @{term th} can not be in @{term readys}, because otherwise, since + @{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *} + moreover have "th \ readys (t@s)" + using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto + -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in + term @{term readys}: *} + ultimately obtain th' where th'_in: "th' \ readys (t@s)" + and dp: "(Th th, Th th') \ (RAG (t @ s))\<^sup>+" by auto + -- {* We are going to show that this @{term th'} is running. *} + have "th' \ runing (t@s)" + proof - + -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *} + have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R") + proof - + have "?L = Max ((the_preced (t @ s) \ the_thread) ` subtree (tRAG (t @ s)) (Th th'))" + by (unfold cp_alt_def1, simp) + also have "... = (the_preced (t @ s) \ the_thread) (Th th)" + proof(rule image_Max_subset) + show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads) + next + show "subtree (tRAG (t @ s)) (Th th') \ Th ` threads (t @ s)" + by (metis Range.intros dp trancl_range vat_t.range_in vat_t.subtree_tRAG_thread) + next + show "Th th \ subtree (tRAG (t @ s)) (Th th')" using dp + by (unfold tRAG_subtree_eq, auto simp:subtree_def) + next + show "Max ((the_preced (t @ s) \ the_thread) ` Th ` threads (t @ s)) = + (the_preced (t @ s) \ the_thread) (Th th)" (is "Max ?L = _") + proof - + have "?L = the_preced (t @ s) ` threads (t @ s)" + by (unfold image_comp, rule image_cong, auto) + thus ?thesis using max_preced the_preced_def by auto + qed + qed + also have "... = ?R" + using th_cp_max th_cp_preced th_kept + the_preced_def vat_t.max_cp_readys_threads by auto + finally show ?thesis . + qed + -- {* Now, since @{term th'} holds the highest @{term cp} + and we have already show it is in @{term readys}, + it is @{term runing} by definition. *} + with `th' \ readys (t@s)` show ?thesis by (simp add: runing_def) + qed + -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *} + moreover have "Th th' \ ancestors (RAG (t @ s)) (Th th)" + using `(Th th, Th th') \ (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) + ultimately show ?thesis using that by metis +qed + +text {* + Now it is easy to see there is always a thread to run by case analysis + on whether thread @{term th} is running: if the answer is Yes, the + the running thread is obviously @{term th} itself; otherwise, the running + thread is the @{text th'} given by lemma @{thm th_blockedE}. *} -lemma step_RAG_p: - "vt (P th cs#s) \ - RAG (P th cs # s) = (if (wq s cs = []) then RAG s \ {(Cs cs, Th th)} - else RAG s \ {(Th th, Cs cs)})" - apply(simp only: s_RAG_def wq_def) - apply (auto split:list.splits prod.splits simp:Let_def wq_def cs_waiting_def cs_holding_def) - apply(case_tac "csa = cs", auto) - apply(fold wq_def) - apply(drule_tac step_back_step) - apply(ind_cases " step s (P (hd (wq s cs)) cs)") - apply(simp add:s_RAG_def wq_def cs_holding_def) - apply(auto) - done +lemma live: "runing (t@s) \ {}" +proof(cases "th \ runing (t@s)") + case True thus ?thesis by auto +next + case False + thus ?thesis using th_blockedE by auto +qed -lemma RAG_target_th: "(Th th, x) \ RAG (s::state) \ \ cs. x = Cs cs" - by (unfold s_RAG_def, auto) +end +end +======= +theory Correctness +imports PIPBasics +begin + + +text {* + The following two auxiliary lemmas are used to reason about @{term Max}. +*} +lemma image_Max_eqI: + assumes "finite B" + and "b \ B" + and "\ x \ B. f x \ f b" + shows "Max (f ` B) = f b" + using assms + using Max_eqI by blast -context valid_trace +lemma image_Max_subset: + assumes "finite A" + and "B \ A" + and "a \ B" + and "Max (f ` A) = f a" + shows "Max (f ` B) = f a" +proof(rule image_Max_eqI) + show "finite B" + using assms(1) assms(2) finite_subset by auto +next + show "a \ B" using assms by simp +next + show "\x\B. f x \ f a" + by (metis Max_ge assms(1) assms(2) assms(4) + finite_imageI image_eqI subsetCE) +qed + +text {* + The following locale @{text "highest_gen"} sets the basic context for our + investigation: supposing thread @{text th} holds the highest @{term cp}-value + in state @{text s}, which means the task for @{text th} is the + most urgent. We want to show that + @{text th} is treated correctly by PIP, which means + @{text th} will not be blocked unreasonably by other less urgent + threads. +*} +locale highest_gen = + fixes s th prio tm + assumes vt_s: "vt s" + and threads_s: "th \ threads s" + and highest: "preced th s = Max ((cp s)`threads s)" + -- {* The internal structure of @{term th}'s precedence is exposed:*} + and preced_th: "preced th s = Prc prio tm" + +-- {* @{term s} is a valid trace, so it will inherit all results derived for + a valid trace: *} +sublocale highest_gen < vat_s: valid_trace "s" + by (unfold_locales, insert vt_s, simp) + +context highest_gen begin text {* - The following lemma shows that @{text "RAG"} is acyclic. - The overall structure is by induction on the formation of @{text "vt s"} - and then case analysis on event @{text "e"}, where the non-trivial cases - for those for @{text "V"} and @{text "P"} events. + @{term tm} is the time when the precedence of @{term th} is set, so + @{term tm} must be a valid moment index into @{term s}. *} -lemma acyclic_RAG: - shows "acyclic (RAG s)" -using vt -proof(induct) - case (vt_cons s e) - interpret vt_s: valid_trace s using vt_cons(1) - by (unfold_locales, simp) - assume ih: "acyclic (RAG s)" - and stp: "step s e" - and vt: "vt s" - show ?case - proof(cases e) - case (Create th prio) - with ih - show ?thesis by (simp add:RAG_create_unchanged) - next - case (Exit th) - with ih show ?thesis by (simp add:RAG_exit_unchanged) - next - case (V th cs) - from V vt stp have vtt: "vt (V th cs#s)" by auto - from step_RAG_v [OF this] - have eq_de: - "RAG (e # s) = - RAG s - {(Cs cs, Th th)} - {(Th th', Cs cs) |th'. next_th s th cs th'} \ - {(Cs cs, Th th') |th'. next_th s th cs th'}" - (is "?L = (?A - ?B - ?C) \ ?D") by (simp add:V) - from ih have ac: "acyclic (?A - ?B - ?C)" by (auto elim:acyclic_subset) - from step_back_step [OF vtt] - have "step s (V th cs)" . - thus ?thesis - proof(cases) - assume "holding s th cs" - hence th_in: "th \ set (wq s cs)" and - eq_hd: "th = hd (wq s cs)" unfolding s_holding_def wq_def by auto - then obtain rest where - eq_wq: "wq s cs = th#rest" - by (cases "wq s cs", auto) - show ?thesis - proof(cases "rest = []") - case False - let ?th' = "hd (SOME q. distinct q \ set q = set rest)" - from eq_wq False have eq_D: "?D = {(Cs cs, Th ?th')}" - by (unfold next_th_def, auto) - let ?E = "(?A - ?B - ?C)" - have "(Th ?th', Cs cs) \ ?E\<^sup>*" - proof - assume "(Th ?th', Cs cs) \ ?E\<^sup>*" - hence " (Th ?th', Cs cs) \ ?E\<^sup>+" by (simp add: rtrancl_eq_or_trancl) - from tranclD [OF this] - obtain x where th'_e: "(Th ?th', x) \ ?E" by blast - hence th_d: "(Th ?th', x) \ ?A" by simp - from RAG_target_th [OF this] - obtain cs' where eq_x: "x = Cs cs'" by auto - with th_d have "(Th ?th', Cs cs') \ ?A" by simp - hence wt_th': "waiting s ?th' cs'" - unfolding s_RAG_def s_waiting_def cs_waiting_def wq_def by simp - hence "cs' = cs" - proof(rule vt_s.waiting_unique) - from eq_wq vt_s.wq_distinct[of cs] - show "waiting s ?th' cs" - apply (unfold s_waiting_def wq_def, auto) - proof - - assume hd_in: "hd (SOME q. distinct q \ set q = set rest) \ set rest" - and eq_wq: "wq_fun (schs s) cs = th # rest" - have "(SOME q. distinct q \ set q = set rest) \ []" - proof(rule someI2) - from vt_s.wq_distinct[of cs] and eq_wq - show "distinct rest \ set rest = set rest" unfolding wq_def by auto - next - fix x assume "distinct x \ set x = set rest" - with False show "x \ []" by auto - qed - hence "hd (SOME q. distinct q \ set q = set rest) \ - set (SOME q. distinct q \ set q = set rest)" by auto - moreover have "\ = set rest" - proof(rule someI2) - from vt_s.wq_distinct[of cs] and eq_wq - show "distinct rest \ set rest = set rest" unfolding wq_def by auto - next - show "\x. distinct x \ set x = set rest \ set x = set rest" by auto - qed - moreover note hd_in - ultimately show "hd (SOME q. distinct q \ set q = set rest) = th" by auto - next - assume hd_in: "hd (SOME q. distinct q \ set q = set rest) \ set rest" - and eq_wq: "wq s cs = hd (SOME q. distinct q \ set q = set rest) # rest" - have "(SOME q. distinct q \ set q = set rest) \ []" - proof(rule someI2) - from vt_s.wq_distinct[of cs] and eq_wq - show "distinct rest \ set rest = set rest" by auto - next - fix x assume "distinct x \ set x = set rest" - with False show "x \ []" by auto - qed - hence "hd (SOME q. distinct q \ set q = set rest) \ - set (SOME q. distinct q \ set q = set rest)" by auto - moreover have "\ = set rest" - proof(rule someI2) - from vt_s.wq_distinct[of cs] and eq_wq - show "distinct rest \ set rest = set rest" by auto - next - show "\x. distinct x \ set x = set rest \ set x = set rest" by auto - qed - moreover note hd_in - ultimately show False by auto - qed - qed - with th'_e eq_x have "(Th ?th', Cs cs) \ ?E" by simp - with False - show "False" by (auto simp: next_th_def eq_wq) - qed - with acyclic_insert[symmetric] and ac - and eq_de eq_D show ?thesis by auto - next - case True - with eq_wq - have eq_D: "?D = {}" - by (unfold next_th_def, auto) - with eq_de ac - show ?thesis by auto - qed - qed - next - case (P th cs) - from P vt stp have vtt: "vt (P th cs#s)" by auto - from step_RAG_p [OF this] P - have "RAG (e # s) = - (if wq s cs = [] then RAG s \ {(Cs cs, Th th)} else - RAG s \ {(Th th, Cs cs)})" (is "?L = ?R") - by simp - moreover have "acyclic ?R" - proof(cases "wq s cs = []") - case True - hence eq_r: "?R = RAG s \ {(Cs cs, Th th)}" by simp - have "(Th th, Cs cs) \ (RAG s)\<^sup>*" - proof - assume "(Th th, Cs cs) \ (RAG s)\<^sup>*" - hence "(Th th, Cs cs) \ (RAG s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl) - from tranclD2 [OF this] - obtain x where "(x, Cs cs) \ RAG s" by auto - with True show False by (auto simp:s_RAG_def cs_waiting_def) - qed - with acyclic_insert ih eq_r show ?thesis by auto - next - case False - hence eq_r: "?R = RAG s \ {(Th th, Cs cs)}" by simp - have "(Cs cs, Th th) \ (RAG s)\<^sup>*" - proof - assume "(Cs cs, Th th) \ (RAG s)\<^sup>*" - hence "(Cs cs, Th th) \ (RAG s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl) - moreover from step_back_step [OF vtt] have "step s (P th cs)" . - ultimately show False - proof - - show " \(Cs cs, Th th) \ (RAG s)\<^sup>+; step s (P th cs)\ \ False" - by (ind_cases "step s (P th cs)", simp) - qed - qed - with acyclic_insert ih eq_r show ?thesis by auto - qed - ultimately show ?thesis by simp - next - case (Set thread prio) - with ih - thm RAG_set_unchanged - show ?thesis by (simp add:RAG_set_unchanged) - qed - next - case vt_nil - show "acyclic (RAG ([]::state))" - by (auto simp: s_RAG_def cs_waiting_def - cs_holding_def wq_def acyclic_def) +lemma lt_tm: "tm < length s" + by (insert preced_tm_lt[OF threads_s preced_th], simp) + +text {* + Since @{term th} holds the highest precedence and @{text "cp"} + is the highest precedence of all threads in the sub-tree of + @{text "th"} and @{text th} is among these threads, + its @{term cp} must equal to its precedence: +*} +lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R") +proof - + have "?L \ ?R" + by (unfold highest, rule Max_ge, + auto simp:threads_s finite_threads) + moreover have "?R \ ?L" + by (unfold vat_s.cp_rec, rule Max_ge, + auto simp:the_preced_def vat_s.fsbttRAGs.finite_children) + ultimately show ?thesis by auto qed +lemma highest_cp_preced: "cp s th = Max (the_preced s ` threads s)" + using eq_cp_s_th highest max_cp_eq the_preced_def by presburger + -lemma finite_RAG: - shows "finite (RAG s)" -proof - - from vt show ?thesis - proof(induct) - case (vt_cons s e) - interpret vt_s: valid_trace s using vt_cons(1) - by (unfold_locales, simp) - assume ih: "finite (RAG s)" - and stp: "step s e" - and vt: "vt s" - show ?case - proof(cases e) - case (Create th prio) - with ih - show ?thesis by (simp add:RAG_create_unchanged) - next - case (Exit th) - with ih show ?thesis by (simp add:RAG_exit_unchanged) - next - case (V th cs) - from V vt stp have vtt: "vt (V th cs#s)" by auto - from step_RAG_v [OF this] - have eq_de: "RAG (e # s) = - RAG s - {(Cs cs, Th th)} - {(Th th', Cs cs) |th'. next_th s th cs th'} \ - {(Cs cs, Th th') |th'. next_th s th cs th'} -" - (is "?L = (?A - ?B - ?C) \ ?D") by (simp add:V) - moreover from ih have ac: "finite (?A - ?B - ?C)" by simp - moreover have "finite ?D" - proof - - have "?D = {} \ (\ a. ?D = {a})" - by (unfold next_th_def, auto) - thus ?thesis - proof - assume h: "?D = {}" - show ?thesis by (unfold h, simp) - next - assume "\ a. ?D = {a}" - thus ?thesis - by (metis finite.simps) - qed - qed - ultimately show ?thesis by simp - next - case (P th cs) - from P vt stp have vtt: "vt (P th cs#s)" by auto - from step_RAG_p [OF this] P - have "RAG (e # s) = - (if wq s cs = [] then RAG s \ {(Cs cs, Th th)} else - RAG s \ {(Th th, Cs cs)})" (is "?L = ?R") - by simp - moreover have "finite ?R" - proof(cases "wq s cs = []") - case True - hence eq_r: "?R = RAG s \ {(Cs cs, Th th)}" by simp - with True and ih show ?thesis by auto - next - case False - hence "?R = RAG s \ {(Th th, Cs cs)}" by simp - with False and ih show ?thesis by auto - qed - ultimately show ?thesis by auto - next - case (Set thread prio) - with ih - show ?thesis by (simp add:RAG_set_unchanged) - qed - next - case vt_nil - show "finite (RAG ([]::state))" - by (auto simp: s_RAG_def cs_waiting_def - cs_holding_def wq_def acyclic_def) - qed -qed +lemma highest_preced_thread: "preced th s = Max (the_preced s ` threads s)" + by (fold eq_cp_s_th, unfold highest_cp_preced, simp) -text {* Several useful lemmas *} - -lemma wf_dep_converse: - shows "wf ((RAG s)^-1)" -proof(rule finite_acyclic_wf_converse) - from finite_RAG - show "finite (RAG s)" . -next - from acyclic_RAG - show "acyclic (RAG s)" . -qed +lemma highest': "cp s th = Max (cp s ` threads s)" + by (simp add: eq_cp_s_th highest) end -lemma hd_np_in: "x \ set l \ hd l \ set l" - by (induct l, auto) +locale extend_highest_gen = highest_gen + + fixes t + assumes vt_t: "vt (t@s)" + and create_low: "Create th' prio' \ set t \ prio' \ prio" + and set_diff_low: "Set th' prio' \ set t \ th' \ th \ prio' \ prio" + and exit_diff: "Exit th' \ set t \ th' \ th" -lemma th_chasing: "(Th th, Cs cs) \ RAG (s::state) \ \ th'. (Cs cs, Th th') \ RAG s" - by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in) - -context valid_trace -begin +sublocale extend_highest_gen < vat_t: valid_trace "t@s" + by (unfold_locales, insert vt_t, simp) -lemma wq_threads: - assumes h: "th \ set (wq s cs)" - shows "th \ threads s" +lemma step_back_vt_app: + assumes vt_ts: "vt (t@s)" + shows "vt s" proof - - from vt and h show ?thesis - proof(induct arbitrary: th cs) - case (vt_cons s e) - interpret vt_s: valid_trace s - using vt_cons(1) by (unfold_locales, auto) - assume ih: "\th cs. th \ set (wq s cs) \ th \ threads s" - and stp: "step s e" - and vt: "vt s" - and h: "th \ set (wq (e # s) cs)" + from vt_ts show ?thesis + proof(induct t) + case Nil + from Nil show ?case by auto + next + case (Cons e t) + assume ih: " vt (t @ s) \ vt s" + and vt_et: "vt ((e # t) @ s)" show ?case - proof(cases e) - case (Create th' prio) - with ih h show ?thesis - by (auto simp:wq_def Let_def) - next - case (Exit th') - with stp ih h show ?thesis - apply (auto simp:wq_def Let_def) - apply (ind_cases "step s (Exit th')") - apply (auto simp:runing_def readys_def s_holding_def s_waiting_def holdents_def - s_RAG_def s_holding_def cs_holding_def) - done - next - case (V th' cs') - show ?thesis - proof(cases "cs' = cs") - case False - with h - show ?thesis - apply(unfold wq_def V, auto simp:Let_def V split:prod.splits, fold wq_def) - by (drule_tac ih, simp) - next - case True - from h - show ?thesis - proof(unfold V wq_def) - assume th_in: "th \ set (wq_fun (schs (V th' cs' # s)) cs)" (is "th \ set ?l") - show "th \ threads (V th' cs' # s)" - proof(cases "cs = cs'") - case False - hence "?l = wq_fun (schs s) cs" by (simp add:Let_def) - with th_in have " th \ set (wq s cs)" - by (fold wq_def, simp) - from ih [OF this] show ?thesis by simp - next - case True - show ?thesis - proof(cases "wq_fun (schs s) cs'") - case Nil - with h V show ?thesis - apply (auto simp:wq_def Let_def split:if_splits) - by (fold wq_def, drule_tac ih, simp) - next - case (Cons a rest) - assume eq_wq: "wq_fun (schs s) cs' = a # rest" - with h V show ?thesis - apply (auto simp:Let_def wq_def split:if_splits) - proof - - assume th_in: "th \ set (SOME q. distinct q \ set q = set rest)" - have "set (SOME q. distinct q \ set q = set rest) = set rest" - proof(rule someI2) - from vt_s.wq_distinct[of cs'] and eq_wq[folded wq_def] - show "distinct rest \ set rest = set rest" by auto - next - show "\x. distinct x \ set x = set rest \ set x = set rest" - by auto - qed - with eq_wq th_in have "th \ set (wq_fun (schs s) cs')" by auto - from ih[OF this[folded wq_def]] show "th \ threads s" . - next - assume th_in: "th \ set (wq_fun (schs s) cs)" - from ih[OF this[folded wq_def]] - show "th \ threads s" . - qed - qed - qed - qed - qed - next - case (P th' cs') - from h stp - show ?thesis - apply (unfold P wq_def) - apply (auto simp:Let_def split:if_splits, fold wq_def) - apply (auto intro:ih) - apply(ind_cases "step s (P th' cs')") - by (unfold runing_def readys_def, auto) - next - case (Set thread prio) - with ih h show ?thesis - by (auto simp:wq_def Let_def) - qed - next - case vt_nil - thus ?case by (auto simp:wq_def) - qed -qed - -lemma range_in: "\(Th th) \ Range (RAG (s::state))\ \ th \ threads s" - apply(unfold s_RAG_def cs_waiting_def cs_holding_def) - by (auto intro:wq_threads) - -lemma readys_v_eq: - fixes th thread cs rest - assumes neq_th: "th \ thread" - and eq_wq: "wq s cs = thread#rest" - and not_in: "th \ set rest" - shows "(th \ readys (V thread cs#s)) = (th \ readys s)" -proof - - from assms show ?thesis - apply (auto simp:readys_def) - apply(simp add:s_waiting_def[folded wq_def]) - apply (erule_tac x = csa in allE) - apply (simp add:s_waiting_def wq_def Let_def split:if_splits) - apply (case_tac "csa = cs", simp) - apply (erule_tac x = cs in allE) - apply(auto simp add: s_waiting_def[folded wq_def] Let_def split: list.splits) - apply(auto simp add: wq_def) - apply (auto simp:s_waiting_def wq_def Let_def split:list.splits) - proof - - assume th_nin: "th \ set rest" - and th_in: "th \ set (SOME q. distinct q \ set q = set rest)" - and eq_wq: "wq_fun (schs s) cs = thread # rest" - have "set (SOME q. distinct q \ set q = set rest) = set rest" - proof(rule someI2) - from wq_distinct[of cs, unfolded wq_def] and eq_wq[unfolded wq_def] - show "distinct rest \ set rest = set rest" by auto - next - show "\x. distinct x \ set x = set rest \ set x = set rest" by auto - qed - with th_nin th_in show False by auto - qed -qed - -text {* \noindent - The following lemmas shows that: starting from any node in @{text "RAG"}, - by chasing out-going edges, it is always possible to reach a node representing a ready - thread. In this lemma, it is the @{text "th'"}. -*} - -lemma chain_building: - shows "node \ Domain (RAG s) \ (\ th'. th' \ readys s \ (node, Th th') \ (RAG s)^+)" -proof - - from wf_dep_converse - have h: "wf ((RAG s)\)" . - show ?thesis - proof(induct rule:wf_induct [OF h]) - fix x - assume ih [rule_format]: - "\y. (y, x) \ (RAG s)\ \ - y \ Domain (RAG s) \ (\th'. th' \ readys s \ (y, Th th') \ (RAG s)\<^sup>+)" - show "x \ Domain (RAG s) \ (\th'. th' \ readys s \ (x, Th th') \ (RAG s)\<^sup>+)" - proof - assume x_d: "x \ Domain (RAG s)" - show "\th'. th' \ readys s \ (x, Th th') \ (RAG s)\<^sup>+" - proof(cases x) - case (Th th) - from x_d Th obtain cs where x_in: "(Th th, Cs cs) \ RAG s" by (auto simp:s_RAG_def) - with Th have x_in_r: "(Cs cs, x) \ (RAG s)^-1" by simp - from th_chasing [OF x_in] obtain th' where "(Cs cs, Th th') \ RAG s" by blast - hence "Cs cs \ Domain (RAG s)" by auto - from ih [OF x_in_r this] obtain th' - where th'_ready: " th' \ readys s" and cs_in: "(Cs cs, Th th') \ (RAG s)\<^sup>+" by auto - have "(x, Th th') \ (RAG s)\<^sup>+" using Th x_in cs_in by auto - with th'_ready show ?thesis by auto - next - case (Cs cs) - from x_d Cs obtain th' where th'_d: "(Th th', x) \ (RAG s)^-1" by (auto simp:s_RAG_def) - show ?thesis - proof(cases "th' \ readys s") - case True - from True and th'_d show ?thesis by auto - next - case False - from th'_d and range_in have "th' \ threads s" by auto - with False have "Th th' \ Domain (RAG s)" - by (auto simp:readys_def wq_def s_waiting_def s_RAG_def cs_waiting_def Domain_def) - from ih [OF th'_d this] - obtain th'' where - th''_r: "th'' \ readys s" and - th''_in: "(Th th', Th th'') \ (RAG s)\<^sup>+" by auto - from th'_d and th''_in - have "(x, Th th'') \ (RAG s)\<^sup>+" by auto - with th''_r show ?thesis by auto - qed + proof(rule ih) + show "vt (t @ s)" + proof(rule step_back_vt) + from vt_et show "vt (e # t @ s)" by simp qed qed qed qed -text {* \noindent - The following is just an instance of @{text "chain_building"}. -*} -lemma th_chain_to_ready: - assumes th_in: "th \ threads s" - shows "th \ readys s \ (\ th'. th' \ readys s \ (Th th, Th th') \ (RAG s)^+)" -proof(cases "th \ readys s") - case True - thus ?thesis by auto -next - case False - from False and th_in have "Th th \ Domain (RAG s)" - by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_def Domain_def) - from chain_building [rule_format, OF this] - show ?thesis by auto -qed - -end +(* locale red_extend_highest_gen = extend_highest_gen + + fixes i::nat +*) -lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs" - by (unfold s_waiting_def cs_waiting_def wq_def, auto) - -lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs" - by (unfold s_holding_def wq_def cs_holding_def, simp) - -lemma holding_unique: "\holding (s::state) th1 cs; holding s th2 cs\ \ th1 = th2" - by (unfold s_holding_def cs_holding_def, auto) - -context valid_trace -begin +(* +sublocale red_extend_highest_gen < red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)" + apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric]) + apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp) + by (unfold highest_gen_def, auto dest:step_back_vt_app) +*) -lemma unique_RAG: "\(n, n1) \ RAG s; (n, n2) \ RAG s\ \ n1 = n2" - apply(unfold s_RAG_def, auto, fold waiting_eq holding_eq) - by(auto elim:waiting_unique holding_unique) - -end - - -lemma trancl_split: "(a, b) \ r^+ \ \ c. (a, c) \ r" -by (induct rule:trancl_induct, auto) - -context valid_trace +context extend_highest_gen begin -lemma dchain_unique: - assumes th1_d: "(n, Th th1) \ (RAG s)^+" - and th1_r: "th1 \ readys s" - and th2_d: "(n, Th th2) \ (RAG s)^+" - and th2_r: "th2 \ readys s" - shows "th1 = th2" -proof - - { assume neq: "th1 \ th2" - hence "Th th1 \ Th th2" by simp - from unique_chain [OF _ th1_d th2_d this] and unique_RAG - have "(Th th1, Th th2) \ (RAG s)\<^sup>+ \ (Th th2, Th th1) \ (RAG s)\<^sup>+" by auto - hence "False" - proof - assume "(Th th1, Th th2) \ (RAG s)\<^sup>+" - from trancl_split [OF this] - obtain n where dd: "(Th th1, n) \ RAG s" by auto - then obtain cs where eq_n: "n = Cs cs" - by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in) - from dd eq_n have "th1 \ readys s" - by (auto simp:readys_def s_RAG_def wq_def s_waiting_def cs_waiting_def) - with th1_r show ?thesis by auto - next - assume "(Th th2, Th th1) \ (RAG s)\<^sup>+" - from trancl_split [OF this] - obtain n where dd: "(Th th2, n) \ RAG s" by auto - then obtain cs where eq_n: "n = Cs cs" - by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in) - from dd eq_n have "th2 \ readys s" - by (auto simp:readys_def wq_def s_RAG_def s_waiting_def cs_waiting_def) - with th2_r show ?thesis by auto - qed - } thus ?thesis by auto -qed - -end - - -lemma step_holdents_p_add: - fixes th cs s - assumes vt: "vt (P th cs#s)" - and "wq s cs = []" - shows "holdents (P th cs#s) th = holdents s th \ {cs}" -proof - - from assms show ?thesis - unfolding holdents_test step_RAG_p[OF vt] by (auto) -qed - -lemma step_holdents_p_eq: - fixes th cs s - assumes vt: "vt (P th cs#s)" - and "wq s cs \ []" - shows "holdents (P th cs#s) th = holdents s th" -proof - - from assms show ?thesis - unfolding holdents_test step_RAG_p[OF vt] by auto -qed - - -lemma (in valid_trace) finite_holding : - shows "finite (holdents s th)" -proof - - let ?F = "\ (x, y). the_cs x" - from finite_RAG - have "finite (RAG s)" . - hence "finite (?F `(RAG s))" by simp - moreover have "{cs . (Cs cs, Th th) \ RAG s} \ \" - proof - - { have h: "\ a A f. a \ A \ f a \ f ` A" by auto - fix x assume "(Cs x, Th th) \ RAG s" - hence "?F (Cs x, Th th) \ ?F `(RAG s)" by (rule h) - moreover have "?F (Cs x, Th th) = x" by simp - ultimately have "x \ (\(x, y). the_cs x) ` RAG s" by simp - } thus ?thesis by auto - qed - ultimately show ?thesis by (unfold holdents_test, auto intro:finite_subset) -qed - -lemma cntCS_v_dec: - fixes s thread cs - assumes vtv: "vt (V thread cs#s)" - shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread" -proof - - from vtv interpret vt_s: valid_trace s - by (cases, unfold_locales, simp) - from vtv interpret vt_v: valid_trace "V thread cs#s" - by (unfold_locales, simp) - from step_back_step[OF vtv] - have cs_in: "cs \ holdents s thread" - apply (cases, unfold holdents_test s_RAG_def, simp) - by (unfold cs_holding_def s_holding_def wq_def, auto) - moreover have cs_not_in: - "(holdents (V thread cs#s) thread) = holdents s thread - {cs}" - apply (insert vt_s.wq_distinct[of cs]) - apply (unfold holdents_test, unfold step_RAG_v[OF vtv], - auto simp:next_th_def) - proof - - fix rest - assume dst: "distinct (rest::thread list)" - and ne: "rest \ []" - and hd_ni: "hd (SOME q. distinct q \ set q = set rest) \ set rest" - moreover have "set (SOME q. distinct q \ set q = set rest) = set rest" - proof(rule someI2) - from dst show "distinct rest \ set rest = set rest" by auto - next - show "\x. distinct x \ set x = set rest \ set x = set rest" by auto - qed - ultimately have "hd (SOME q. distinct q \ set q = set rest) \ - set (SOME q. distinct q \ set q = set rest)" by simp - moreover have "(SOME q. distinct q \ set q = set rest) \ []" - proof(rule someI2) - from dst show "distinct rest \ set rest = set rest" by auto - next - fix x assume " distinct x \ set x = set rest" with ne - show "x \ []" by auto - qed - ultimately - show "(Cs cs, Th (hd (SOME q. distinct q \ set q = set rest))) \ RAG s" - by auto - next - fix rest - assume dst: "distinct (rest::thread list)" - and ne: "rest \ []" - and hd_ni: "hd (SOME q. distinct q \ set q = set rest) \ set rest" - moreover have "set (SOME q. distinct q \ set q = set rest) = set rest" - proof(rule someI2) - from dst show "distinct rest \ set rest = set rest" by auto - next - show "\x. distinct x \ set x = set rest \ set x = set rest" by auto - qed - ultimately have "hd (SOME q. distinct q \ set q = set rest) \ - set (SOME q. distinct q \ set q = set rest)" by simp - moreover have "(SOME q. distinct q \ set q = set rest) \ []" - proof(rule someI2) - from dst show "distinct rest \ set rest = set rest" by auto - next - fix x assume " distinct x \ set x = set rest" with ne - show "x \ []" by auto - qed - ultimately show "False" by auto - qed - ultimately - have "holdents s thread = insert cs (holdents (V thread cs#s) thread)" - by auto - moreover have "card \ = - Suc (card ((holdents (V thread cs#s) thread) - {cs}))" - proof(rule card_insert) - from vt_v.finite_holding - show " finite (holdents (V thread cs # s) thread)" . - qed - moreover from cs_not_in - have "cs \ (holdents (V thread cs#s) thread)" by auto - ultimately show ?thesis by (simp add:cntCS_def) -qed - -context valid_trace -begin - -text {* (* ddd *) \noindent - The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"} - of one particular thread. -*} - -lemma cnp_cnv_cncs: - shows "cntP s th = cntV s th + (if (th \ readys s \ th \ threads s) - then cntCS s th else cntCS s th + 1)" + lemma ind [consumes 0, case_names Nil Cons, induct type]: + assumes + h0: "R []" + and h2: "\ e t. \vt (t@s); step (t@s) e; + extend_highest_gen s th prio tm t; + extend_highest_gen s th prio tm (e#t); R t\ \ R (e#t)" + shows "R t" proof - - from vt show ?thesis - proof(induct arbitrary:th) - case (vt_cons s e) - interpret vt_s: valid_trace s using vt_cons(1) by (unfold_locales, simp) - assume vt: "vt s" - and ih: "\th. cntP s th = cntV s th + - (if (th \ readys s \ th \ threads s) then cntCS s th else cntCS s th + 1)" - and stp: "step s e" - from stp show ?case - proof(cases) - case (thread_create thread prio) - assume eq_e: "e = Create thread prio" - and not_in: "thread \ threads s" - show ?thesis - proof - - { fix cs - assume "thread \ set (wq s cs)" - from vt_s.wq_threads [OF this] have "thread \ threads s" . - with not_in have "False" by simp - } with eq_e have eq_readys: "readys (e#s) = readys s \ {thread}" - by (auto simp:readys_def threads.simps s_waiting_def - wq_def cs_waiting_def Let_def) - from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) - from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) - have eq_cncs: "cntCS (e#s) th = cntCS s th" - unfolding cntCS_def holdents_test - by (simp add:RAG_create_unchanged eq_e) - { assume "th \ thread" - with eq_readys eq_e - have "(th \ readys (e # s) \ th \ threads (e # s)) = - (th \ readys (s) \ th \ threads (s))" - by (simp add:threads.simps) - with eq_cnp eq_cnv eq_cncs ih not_in - have ?thesis by simp - } moreover { - assume eq_th: "th = thread" - with not_in ih have " cntP s th = cntV s th + cntCS s th" by simp - moreover from eq_th and eq_readys have "th \ readys (e#s)" by simp - moreover note eq_cnp eq_cnv eq_cncs - ultimately have ?thesis by auto - } ultimately show ?thesis by blast - qed - next - case (thread_exit thread) - assume eq_e: "e = Exit thread" - and is_runing: "thread \ runing s" - and no_hold: "holdents s thread = {}" - from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) - from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) - have eq_cncs: "cntCS (e#s) th = cntCS s th" - unfolding cntCS_def holdents_test - by (simp add:RAG_exit_unchanged eq_e) - { assume "th \ thread" - with eq_e - have "(th \ readys (e # s) \ th \ threads (e # s)) = - (th \ readys (s) \ th \ threads (s))" - apply (simp add:threads.simps readys_def) - apply (subst s_waiting_def) - apply (simp add:Let_def) - apply (subst s_waiting_def, simp) - done - with eq_cnp eq_cnv eq_cncs ih - have ?thesis by simp - } moreover { - assume eq_th: "th = thread" - with ih is_runing have " cntP s th = cntV s th + cntCS s th" - by (simp add:runing_def) - moreover from eq_th eq_e have "th \ threads (e#s)" - by simp - moreover note eq_cnp eq_cnv eq_cncs - ultimately have ?thesis by auto - } ultimately show ?thesis by blast - next - case (thread_P thread cs) - assume eq_e: "e = P thread cs" - and is_runing: "thread \ runing s" - and no_dep: "(Cs cs, Th thread) \ (RAG s)\<^sup>+" - from thread_P vt stp ih have vtp: "vt (P thread cs#s)" by auto - then interpret vt_p: valid_trace "(P thread cs#s)" - by (unfold_locales, simp) - show ?thesis - proof - - { have hh: "\ A B C. (B = C) \ (A \ B) = (A \ C)" by blast - assume neq_th: "th \ thread" - with eq_e - have eq_readys: "(th \ readys (e#s)) = (th \ readys (s))" - apply (simp add:readys_def s_waiting_def wq_def Let_def) - apply (rule_tac hh) - apply (intro iffI allI, clarify) - apply (erule_tac x = csa in allE, auto) - apply (subgoal_tac "wq_fun (schs s) cs \ []", auto) - apply (erule_tac x = cs in allE, auto) - by (case_tac "(wq_fun (schs s) cs)", auto) - moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th" - apply (simp add:cntCS_def holdents_test) - by (unfold step_RAG_p [OF vtp], auto) - moreover from eq_e neq_th have "cntP (e # s) th = cntP s th" - by (simp add:cntP_def count_def) - moreover from eq_e neq_th have "cntV (e#s) th = cntV s th" - by (simp add:cntV_def count_def) - moreover from eq_e neq_th have "threads (e#s) = threads s" by simp - moreover note ih [of th] - ultimately have ?thesis by simp - } moreover { - assume eq_th: "th = thread" - have ?thesis - proof - - from eq_e eq_th have eq_cnp: "cntP (e # s) th = 1 + (cntP s th)" - by (simp add:cntP_def count_def) - from eq_e eq_th have eq_cnv: "cntV (e#s) th = cntV s th" - by (simp add:cntV_def count_def) - show ?thesis - proof (cases "wq s cs = []") - case True - with is_runing - have "th \ readys (e#s)" - apply (unfold eq_e wq_def, unfold readys_def s_RAG_def) - apply (simp add: wq_def[symmetric] runing_def eq_th s_waiting_def) - by (auto simp:readys_def wq_def Let_def s_waiting_def wq_def) - moreover have "cntCS (e # s) th = 1 + cntCS s th" - proof - - have "card {csa. csa = cs \ (Cs csa, Th thread) \ RAG s} = - Suc (card {cs. (Cs cs, Th thread) \ RAG s})" (is "card ?L = Suc (card ?R)") - proof - - have "?L = insert cs ?R" by auto - moreover have "card \ = Suc (card (?R - {cs}))" - proof(rule card_insert) - from vt_s.finite_holding [of thread] - show " finite {cs. (Cs cs, Th thread) \ RAG s}" - by (unfold holdents_test, simp) - qed - moreover have "?R - {cs} = ?R" - proof - - have "cs \ ?R" - proof - assume "cs \ {cs. (Cs cs, Th thread) \ RAG s}" - with no_dep show False by auto - qed - thus ?thesis by auto - qed - ultimately show ?thesis by auto - qed - thus ?thesis - apply (unfold eq_e eq_th cntCS_def) - apply (simp add: holdents_test) - by (unfold step_RAG_p [OF vtp], auto simp:True) - qed - moreover from is_runing have "th \ readys s" - by (simp add:runing_def eq_th) - moreover note eq_cnp eq_cnv ih [of th] - ultimately show ?thesis by auto - next - case False - have eq_wq: "wq (e#s) cs = wq s cs @ [th]" - by (unfold eq_th eq_e wq_def, auto simp:Let_def) - have "th \ readys (e#s)" - proof - assume "th \ readys (e#s)" - hence "\cs. \ waiting (e # s) th cs" by (simp add:readys_def) - from this[rule_format, of cs] have " \ waiting (e # s) th cs" . - hence "th \ set (wq (e#s) cs) \ th = hd (wq (e#s) cs)" - by (simp add:s_waiting_def wq_def) - moreover from eq_wq have "th \ set (wq (e#s) cs)" by auto - ultimately have "th = hd (wq (e#s) cs)" by blast - with eq_wq have "th = hd (wq s cs @ [th])" by simp - hence "th = hd (wq s cs)" using False by auto - with False eq_wq vt_p.wq_distinct [of cs] - show False by (fold eq_e, auto) - qed - moreover from is_runing have "th \ threads (e#s)" - by (unfold eq_e, auto simp:runing_def readys_def eq_th) - moreover have "cntCS (e # s) th = cntCS s th" - apply (unfold cntCS_def holdents_test eq_e step_RAG_p[OF vtp]) - by (auto simp:False) - moreover note eq_cnp eq_cnv ih[of th] - moreover from is_runing have "th \ readys s" - by (simp add:runing_def eq_th) - ultimately show ?thesis by auto - qed - qed - } ultimately show ?thesis by blast + from vt_t extend_highest_gen_axioms show ?thesis + proof(induct t) + from h0 show "R []" . + next + case (Cons e t') + assume ih: "\vt (t' @ s); extend_highest_gen s th prio tm t'\ \ R t'" + and vt_e: "vt ((e # t') @ s)" + and et: "extend_highest_gen s th prio tm (e # t')" + from vt_e and step_back_step have stp: "step (t'@s) e" by auto + from vt_e and step_back_vt have vt_ts: "vt (t'@s)" by auto + show ?case + proof(rule h2 [OF vt_ts stp _ _ _ ]) + show "R t'" + proof(rule ih) + from et show ext': "extend_highest_gen s th prio tm t'" + by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt) + next + from vt_ts show "vt (t' @ s)" . qed next - case (thread_V thread cs) - from assms vt stp ih thread_V have vtv: "vt (V thread cs # s)" by auto - then interpret vt_v: valid_trace "(V thread cs # s)" by (unfold_locales, simp) - assume eq_e: "e = V thread cs" - and is_runing: "thread \ runing s" - and hold: "holding s thread cs" - from hold obtain rest - where eq_wq: "wq s cs = thread # rest" - by (case_tac "wq s cs", auto simp: wq_def s_holding_def) - have eq_threads: "threads (e#s) = threads s" by (simp add: eq_e) - have eq_set: "set (SOME q. distinct q \ set q = set rest) = set rest" - proof(rule someI2) - from vt_v.wq_distinct[of cs] and eq_wq - show "distinct rest \ set rest = set rest" - by (metis distinct.simps(2) vt_s.wq_distinct) - next - show "\x. distinct x \ set x = set rest \ set x = set rest" - by auto - qed - show ?thesis - proof - - { assume eq_th: "th = thread" - from eq_th have eq_cnp: "cntP (e # s) th = cntP s th" - by (unfold eq_e, simp add:cntP_def count_def) - moreover from eq_th have eq_cnv: "cntV (e#s) th = 1 + cntV s th" - by (unfold eq_e, simp add:cntV_def count_def) - moreover from cntCS_v_dec [OF vtv] - have "cntCS (e # s) thread + 1 = cntCS s thread" - by (simp add:eq_e) - moreover from is_runing have rd_before: "thread \ readys s" - by (unfold runing_def, simp) - moreover have "thread \ readys (e # s)" - proof - - from is_runing - have "thread \ threads (e#s)" - by (unfold eq_e, auto simp:runing_def readys_def) - moreover have "\ cs1. \ waiting (e#s) thread cs1" - proof - fix cs1 - { assume eq_cs: "cs1 = cs" - have "\ waiting (e # s) thread cs1" - proof - - from eq_wq - have "thread \ set (wq (e#s) cs1)" - apply(unfold eq_e wq_def eq_cs s_holding_def) - apply (auto simp:Let_def) - proof - - assume "thread \ set (SOME q. distinct q \ set q = set rest)" - with eq_set have "thread \ set rest" by simp - with vt_v.wq_distinct[of cs] - and eq_wq show False - by (metis distinct.simps(2) vt_s.wq_distinct) - qed - thus ?thesis by (simp add:wq_def s_waiting_def) - qed - } moreover { - assume neq_cs: "cs1 \ cs" - have "\ waiting (e # s) thread cs1" - proof - - from wq_v_neq [OF neq_cs[symmetric]] - have "wq (V thread cs # s) cs1 = wq s cs1" . - moreover have "\ waiting s thread cs1" - proof - - from runing_ready and is_runing - have "thread \ readys s" by auto - thus ?thesis by (simp add:readys_def) - qed - ultimately show ?thesis - by (auto simp:wq_def s_waiting_def eq_e) - qed - } ultimately show "\ waiting (e # s) thread cs1" by blast - qed - ultimately show ?thesis by (simp add:readys_def) - qed - moreover note eq_th ih - ultimately have ?thesis by auto - } moreover { - assume neq_th: "th \ thread" - from neq_th eq_e have eq_cnp: "cntP (e # s) th = cntP s th" - by (simp add:cntP_def count_def) - from neq_th eq_e have eq_cnv: "cntV (e # s) th = cntV s th" - by (simp add:cntV_def count_def) - have ?thesis - proof(cases "th \ set rest") - case False - have "(th \ readys (e # s)) = (th \ readys s)" - apply (insert step_back_vt[OF vtv]) - by (simp add: False eq_e eq_wq neq_th vt_s.readys_v_eq) - moreover have "cntCS (e#s) th = cntCS s th" - apply (insert neq_th, unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto) - proof - - have "{csa. (Cs csa, Th th) \ RAG s \ csa = cs \ next_th s thread cs th} = - {cs. (Cs cs, Th th) \ RAG s}" - proof - - from False eq_wq - have " next_th s thread cs th \ (Cs cs, Th th) \ RAG s" - apply (unfold next_th_def, auto) - proof - - assume ne: "rest \ []" - and ni: "hd (SOME q. distinct q \ set q = set rest) \ set rest" - and eq_wq: "wq s cs = thread # rest" - from eq_set ni have "hd (SOME q. distinct q \ set q = set rest) \ - set (SOME q. distinct q \ set q = set rest) - " by simp - moreover have "(SOME q. distinct q \ set q = set rest) \ []" - proof(rule someI2) - from vt_s.wq_distinct[ of cs] and eq_wq - show "distinct rest \ set rest = set rest" by auto - next - fix x assume "distinct x \ set x = set rest" - with ne show "x \ []" by auto - qed - ultimately show - "(Cs cs, Th (hd (SOME q. distinct q \ set q = set rest))) \ RAG s" - by auto - qed - thus ?thesis by auto - qed - thus "card {csa. (Cs csa, Th th) \ RAG s \ csa = cs \ next_th s thread cs th} = - card {cs. (Cs cs, Th th) \ RAG s}" by simp - qed - moreover note ih eq_cnp eq_cnv eq_threads - ultimately show ?thesis by auto - next - case True - assume th_in: "th \ set rest" - show ?thesis - proof(cases "next_th s thread cs th") - case False - with eq_wq and th_in have - neq_hd: "th \ hd (SOME q. distinct q \ set q = set rest)" (is "th \ hd ?rest") - by (auto simp:next_th_def) - have "(th \ readys (e # s)) = (th \ readys s)" - proof - - from eq_wq and th_in - have "\ th \ readys s" - apply (auto simp:readys_def s_waiting_def) - apply (rule_tac x = cs in exI, auto) - by (insert vt_s.wq_distinct[of cs], auto simp add: wq_def) - moreover - from eq_wq and th_in and neq_hd - have "\ (th \ readys (e # s))" - apply (auto simp:readys_def s_waiting_def eq_e wq_def Let_def split:list.splits) - by (rule_tac x = cs in exI, auto simp:eq_set) - ultimately show ?thesis by auto - qed - moreover have "cntCS (e#s) th = cntCS s th" - proof - - from eq_wq and th_in and neq_hd - have "(holdents (e # s) th) = (holdents s th)" - apply (unfold eq_e step_RAG_v[OF vtv], - auto simp:next_th_def eq_set s_RAG_def holdents_test wq_def - Let_def cs_holding_def) - by (insert vt_s.wq_distinct[of cs], auto simp:wq_def) - thus ?thesis by (simp add:cntCS_def) - qed - moreover note ih eq_cnp eq_cnv eq_threads - ultimately show ?thesis by auto - next - case True - let ?rest = " (SOME q. distinct q \ set q = set rest)" - let ?t = "hd ?rest" - from True eq_wq th_in neq_th - have "th \ readys (e # s)" - apply (auto simp:eq_e readys_def s_waiting_def wq_def - Let_def next_th_def) - proof - - assume eq_wq: "wq_fun (schs s) cs = thread # rest" - and t_in: "?t \ set rest" - show "?t \ threads s" - proof(rule vt_s.wq_threads) - from eq_wq and t_in - show "?t \ set (wq s cs)" by (auto simp:wq_def) - qed - next - fix csa - assume eq_wq: "wq_fun (schs s) cs = thread # rest" - and t_in: "?t \ set rest" - and neq_cs: "csa \ cs" - and t_in': "?t \ set (wq_fun (schs s) csa)" - show "?t = hd (wq_fun (schs s) csa)" - proof - - { assume neq_hd': "?t \ hd (wq_fun (schs s) csa)" - from vt_s.wq_distinct[of cs] and - eq_wq[folded wq_def] and t_in eq_wq - have "?t \ thread" by auto - with eq_wq and t_in - have w1: "waiting s ?t cs" - by (auto simp:s_waiting_def wq_def) - from t_in' neq_hd' - have w2: "waiting s ?t csa" - by (auto simp:s_waiting_def wq_def) - from vt_s.waiting_unique[OF w1 w2] - and neq_cs have "False" by auto - } thus ?thesis by auto - qed - qed - moreover have "cntP s th = cntV s th + cntCS s th + 1" - proof - - have "th \ readys s" - proof - - from True eq_wq neq_th th_in - show ?thesis - apply (unfold readys_def s_waiting_def, auto) - by (rule_tac x = cs in exI, auto simp add: wq_def) - qed - moreover have "th \ threads s" - proof - - from th_in eq_wq - have "th \ set (wq s cs)" by simp - from vt_s.wq_threads [OF this] - show ?thesis . - qed - ultimately show ?thesis using ih by auto - qed - moreover from True neq_th have "cntCS (e # s) th = 1 + cntCS s th" - apply (unfold cntCS_def holdents_test eq_e step_RAG_v[OF vtv], auto) - proof - - show "card {csa. (Cs csa, Th th) \ RAG s \ csa = cs} = - Suc (card {cs. (Cs cs, Th th) \ RAG s})" - (is "card ?A = Suc (card ?B)") - proof - - have "?A = insert cs ?B" by auto - hence "card ?A = card (insert cs ?B)" by simp - also have "\ = Suc (card ?B)" - proof(rule card_insert_disjoint) - have "?B \ ((\ (x, y). the_cs x) ` RAG s)" - apply (auto simp:image_def) - by (rule_tac x = "(Cs x, Th th)" in bexI, auto) - with vt_s.finite_RAG - show "finite {cs. (Cs cs, Th th) \ RAG s}" by (auto intro:finite_subset) - next - show "cs \ {cs. (Cs cs, Th th) \ RAG s}" - proof - assume "cs \ {cs. (Cs cs, Th th) \ RAG s}" - hence "(Cs cs, Th th) \ RAG s" by simp - with True neq_th eq_wq show False - by (auto simp:next_th_def s_RAG_def cs_holding_def) - qed - qed - finally show ?thesis . - qed - qed - moreover note eq_cnp eq_cnv - ultimately show ?thesis by simp - qed - qed - } ultimately show ?thesis by blast - qed - next - case (thread_set thread prio) - assume eq_e: "e = Set thread prio" - and is_runing: "thread \ runing s" - show ?thesis - proof - - from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) - from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) - have eq_cncs: "cntCS (e#s) th = cntCS s th" - unfolding cntCS_def holdents_test - by (simp add:RAG_set_unchanged eq_e) - from eq_e have eq_readys: "readys (e#s) = readys s" - by (simp add:readys_def cs_waiting_def s_waiting_def wq_def, - auto simp:Let_def) - { assume "th \ thread" - with eq_readys eq_e - have "(th \ readys (e # s) \ th \ threads (e # s)) = - (th \ readys (s) \ th \ threads (s))" - by (simp add:threads.simps) - with eq_cnp eq_cnv eq_cncs ih is_runing - have ?thesis by simp - } moreover { - assume eq_th: "th = thread" - with is_runing ih have " cntP s th = cntV s th + cntCS s th" - by (unfold runing_def, auto) - moreover from eq_th and eq_readys is_runing have "th \ readys (e#s)" - by (simp add:runing_def) - moreover note eq_cnp eq_cnv eq_cncs - ultimately have ?thesis by auto - } ultimately show ?thesis by blast - qed - qed - next - case vt_nil - show ?case - by (unfold cntP_def cntV_def cntCS_def, - auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def) - qed -qed - -lemma not_thread_cncs: - assumes not_in: "th \ threads s" - shows "cntCS s th = 0" -proof - - from vt not_in show ?thesis - proof(induct arbitrary:th) - case (vt_cons s e th) - interpret vt_s: valid_trace s using vt_cons(1) - by (unfold_locales, simp) - assume vt: "vt s" - and ih: "\th. th \ threads s \ cntCS s th = 0" - and stp: "step s e" - and not_in: "th \ threads (e # s)" - from stp show ?case - proof(cases) - case (thread_create thread prio) - assume eq_e: "e = Create thread prio" - and not_in': "thread \ threads s" - have "cntCS (e # s) th = cntCS s th" - apply (unfold eq_e cntCS_def holdents_test) - by (simp add:RAG_create_unchanged) - moreover have "th \ threads s" - proof - - from not_in eq_e show ?thesis by simp - qed - moreover note ih ultimately show ?thesis by auto + from et show "extend_highest_gen s th prio tm (e # t')" . next - case (thread_exit thread) - assume eq_e: "e = Exit thread" - and nh: "holdents s thread = {}" - have eq_cns: "cntCS (e # s) th = cntCS s th" - apply (unfold eq_e cntCS_def holdents_test) - by (simp add:RAG_exit_unchanged) - show ?thesis - proof(cases "th = thread") - case True - have "cntCS s th = 0" by (unfold cntCS_def, auto simp:nh True) - with eq_cns show ?thesis by simp - next - case False - with not_in and eq_e - have "th \ threads s" by simp - from ih[OF this] and eq_cns show ?thesis by simp - qed - next - case (thread_P thread cs) - assume eq_e: "e = P thread cs" - and is_runing: "thread \ runing s" - from assms thread_P ih vt stp thread_P have vtp: "vt (P thread cs#s)" by auto - have neq_th: "th \ thread" - proof - - from not_in eq_e have "th \ threads s" by simp - moreover from is_runing have "thread \ threads s" - by (simp add:runing_def readys_def) - ultimately show ?thesis by auto - qed - hence "cntCS (e # s) th = cntCS s th " - apply (unfold cntCS_def holdents_test eq_e) - by (unfold step_RAG_p[OF vtp], auto) - moreover have "cntCS s th = 0" - proof(rule ih) - from not_in eq_e show "th \ threads s" by simp - qed - ultimately show ?thesis by simp - next - case (thread_V thread cs) - assume eq_e: "e = V thread cs" - and is_runing: "thread \ runing s" - and hold: "holding s thread cs" - have neq_th: "th \ thread" - proof - - from not_in eq_e have "th \ threads s" by simp - moreover from is_runing have "thread \ threads s" - by (simp add:runing_def readys_def) - ultimately show ?thesis by auto - qed - from assms thread_V vt stp ih - have vtv: "vt (V thread cs#s)" by auto - then interpret vt_v: valid_trace "(V thread cs#s)" - by (unfold_locales, simp) - from hold obtain rest - where eq_wq: "wq s cs = thread # rest" - by (case_tac "wq s cs", auto simp: wq_def s_holding_def) - from not_in eq_e eq_wq - have "\ next_th s thread cs th" - apply (auto simp:next_th_def) - proof - - assume ne: "rest \ []" - and ni: "hd (SOME q. distinct q \ set q = set rest) \ threads s" (is "?t \ threads s") - have "?t \ set rest" - proof(rule someI2) - from vt_v.wq_distinct[of cs] and eq_wq - show "distinct rest \ set rest = set rest" - by (metis distinct.simps(2) vt_s.wq_distinct) - next - fix x assume "distinct x \ set x = set rest" with ne - show "hd x \ set rest" by (cases x, auto) - qed - with eq_wq have "?t \ set (wq s cs)" by simp - from vt_s.wq_threads[OF this] and ni - show False - using `hd (SOME q. distinct q \ set q = set rest) \ set (wq s cs)` - ni vt_s.wq_threads by blast - qed - moreover note neq_th eq_wq - ultimately have "cntCS (e # s) th = cntCS s th" - by (unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto) - moreover have "cntCS s th = 0" - proof(rule ih) - from not_in eq_e show "th \ threads s" by simp - qed - ultimately show ?thesis by simp - next - case (thread_set thread prio) - print_facts - assume eq_e: "e = Set thread prio" - and is_runing: "thread \ runing s" - from not_in and eq_e have "th \ threads s" by auto - from ih [OF this] and eq_e - show ?thesis - apply (unfold eq_e cntCS_def holdents_test) - by (simp add:RAG_set_unchanged) - qed - next - case vt_nil - show ?case - by (unfold cntCS_def, - auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def) - qed -qed - -end - -lemma eq_waiting: "waiting (wq (s::state)) th cs = waiting s th cs" - by (auto simp:s_waiting_def cs_waiting_def wq_def) - -context valid_trace -begin - -lemma dm_RAG_threads: - assumes in_dom: "(Th th) \ Domain (RAG s)" - shows "th \ threads s" -proof - - from in_dom obtain n where "(Th th, n) \ RAG s" by auto - moreover from RAG_target_th[OF this] obtain cs where "n = Cs cs" by auto - ultimately have "(Th th, Cs cs) \ RAG s" by simp - hence "th \ set (wq s cs)" - by (unfold s_RAG_def, auto simp:cs_waiting_def) - from wq_threads [OF this] show ?thesis . -qed - -end - -lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th" -unfolding cp_def wq_def -apply(induct s rule: schs.induct) -thm cpreced_initial -apply(simp add: Let_def cpreced_initial) -apply(simp add: Let_def) -apply(simp add: Let_def) -apply(simp add: Let_def) -apply(subst (2) schs.simps) -apply(simp add: Let_def) -apply(subst (2) schs.simps) -apply(simp add: Let_def) -done - -context valid_trace -begin - -lemma runing_unique: - assumes runing_1: "th1 \ runing s" - and runing_2: "th2 \ runing s" - shows "th1 = th2" -proof - - from runing_1 and runing_2 have "cp s th1 = cp s th2" - unfolding runing_def - apply(simp) - done - hence eq_max: "Max ((\th. preced th s) ` ({th1} \ dependants (wq s) th1)) = - Max ((\th. preced th s) ` ({th2} \ dependants (wq s) th2))" - (is "Max (?f ` ?A) = Max (?f ` ?B)") - unfolding cp_eq_cpreced - unfolding cpreced_def . - obtain th1' where th1_in: "th1' \ ?A" and eq_f_th1: "?f th1' = Max (?f ` ?A)" - proof - - have h1: "finite (?f ` ?A)" - proof - - have "finite ?A" - proof - - have "finite (dependants (wq s) th1)" - proof- - have "finite {th'. (Th th', Th th1) \ (RAG (wq s))\<^sup>+}" - proof - - let ?F = "\ (x, y). the_th x" - have "{th'. (Th th', Th th1) \ (RAG (wq s))\<^sup>+} \ ?F ` ((RAG (wq s))\<^sup>+)" - apply (auto simp:image_def) - by (rule_tac x = "(Th x, Th th1)" in bexI, auto) - moreover have "finite \" - proof - - from finite_RAG have "finite (RAG s)" . - hence "finite ((RAG (wq s))\<^sup>+)" - apply (unfold finite_trancl) - by (auto simp: s_RAG_def cs_RAG_def wq_def) - thus ?thesis by auto - qed - ultimately show ?thesis by (auto intro:finite_subset) - qed - thus ?thesis by (simp add:cs_dependants_def) - qed - thus ?thesis by simp - qed - thus ?thesis by auto - qed - moreover have h2: "(?f ` ?A) \ {}" - proof - - have "?A \ {}" by simp - thus ?thesis by simp - qed - from Max_in [OF h1 h2] - have "Max (?f ` ?A) \ (?f ` ?A)" . - thus ?thesis - thm cpreced_def - unfolding cpreced_def[symmetric] - unfolding cp_eq_cpreced[symmetric] - unfolding cpreced_def - using that[intro] by (auto) - qed - obtain th2' where th2_in: "th2' \ ?B" and eq_f_th2: "?f th2' = Max (?f ` ?B)" - proof - - have h1: "finite (?f ` ?B)" - proof - - have "finite ?B" - proof - - have "finite (dependants (wq s) th2)" - proof- - have "finite {th'. (Th th', Th th2) \ (RAG (wq s))\<^sup>+}" - proof - - let ?F = "\ (x, y). the_th x" - have "{th'. (Th th', Th th2) \ (RAG (wq s))\<^sup>+} \ ?F ` ((RAG (wq s))\<^sup>+)" - apply (auto simp:image_def) - by (rule_tac x = "(Th x, Th th2)" in bexI, auto) - moreover have "finite \" - proof - - from finite_RAG have "finite (RAG s)" . - hence "finite ((RAG (wq s))\<^sup>+)" - apply (unfold finite_trancl) - by (auto simp: s_RAG_def cs_RAG_def wq_def) - thus ?thesis by auto - qed - ultimately show ?thesis by (auto intro:finite_subset) - qed - thus ?thesis by (simp add:cs_dependants_def) - qed - thus ?thesis by simp - qed - thus ?thesis by auto - qed - moreover have h2: "(?f ` ?B) \ {}" - proof - - have "?B \ {}" by simp - thus ?thesis by simp - qed - from Max_in [OF h1 h2] - have "Max (?f ` ?B) \ (?f ` ?B)" . - thus ?thesis by (auto intro:that) - qed - from eq_f_th1 eq_f_th2 eq_max - have eq_preced: "preced th1' s = preced th2' s" by auto - hence eq_th12: "th1' = th2'" - proof (rule preced_unique) - from th1_in have "th1' = th1 \ (th1' \ dependants (wq s) th1)" by simp - thus "th1' \ threads s" - proof - assume "th1' \ dependants (wq s) th1" - hence "(Th th1') \ Domain ((RAG s)^+)" - apply (unfold cs_dependants_def cs_RAG_def s_RAG_def) - by (auto simp:Domain_def) - hence "(Th th1') \ Domain (RAG s)" by (simp add:trancl_domain) - from dm_RAG_threads[OF this] show ?thesis . - next - assume "th1' = th1" - with runing_1 show ?thesis - by (unfold runing_def readys_def, auto) - qed - next - from th2_in have "th2' = th2 \ (th2' \ dependants (wq s) th2)" by simp - thus "th2' \ threads s" - proof - assume "th2' \ dependants (wq s) th2" - hence "(Th th2') \ Domain ((RAG s)^+)" - apply (unfold cs_dependants_def cs_RAG_def s_RAG_def) - by (auto simp:Domain_def) - hence "(Th th2') \ Domain (RAG s)" by (simp add:trancl_domain) - from dm_RAG_threads[OF this] show ?thesis . - next - assume "th2' = th2" - with runing_2 show ?thesis - by (unfold runing_def readys_def, auto) - qed - qed - from th1_in have "th1' = th1 \ th1' \ dependants (wq s) th1" by simp - thus ?thesis - proof - assume eq_th': "th1' = th1" - from th2_in have "th2' = th2 \ th2' \ dependants (wq s) th2" by simp - thus ?thesis - proof - assume "th2' = th2" thus ?thesis using eq_th' eq_th12 by simp - next - assume "th2' \ dependants (wq s) th2" - with eq_th12 eq_th' have "th1 \ dependants (wq s) th2" by simp - hence "(Th th1, Th th2) \ (RAG s)^+" - by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp) - hence "Th th1 \ Domain ((RAG s)^+)" - apply (unfold cs_dependants_def cs_RAG_def s_RAG_def) - by (auto simp:Domain_def) - hence "Th th1 \ Domain (RAG s)" by (simp add:trancl_domain) - then obtain n where d: "(Th th1, n) \ RAG s" by (auto simp:Domain_def) - from RAG_target_th [OF this] - obtain cs' where "n = Cs cs'" by auto - with d have "(Th th1, Cs cs') \ RAG s" by simp - with runing_1 have "False" - apply (unfold runing_def readys_def s_RAG_def) - by (auto simp:eq_waiting) - thus ?thesis by simp - qed - next - assume th1'_in: "th1' \ dependants (wq s) th1" - from th2_in have "th2' = th2 \ th2' \ dependants (wq s) th2" by simp - thus ?thesis - proof - assume "th2' = th2" - with th1'_in eq_th12 have "th2 \ dependants (wq s) th1" by simp - hence "(Th th2, Th th1) \ (RAG s)^+" - by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp) - hence "Th th2 \ Domain ((RAG s)^+)" - apply (unfold cs_dependants_def cs_RAG_def s_RAG_def) - by (auto simp:Domain_def) - hence "Th th2 \ Domain (RAG s)" by (simp add:trancl_domain) - then obtain n where d: "(Th th2, n) \ RAG s" by (auto simp:Domain_def) - from RAG_target_th [OF this] - obtain cs' where "n = Cs cs'" by auto - with d have "(Th th2, Cs cs') \ RAG s" by simp - with runing_2 have "False" - apply (unfold runing_def readys_def s_RAG_def) - by (auto simp:eq_waiting) - thus ?thesis by simp - next - assume "th2' \ dependants (wq s) th2" - with eq_th12 have "th1' \ dependants (wq s) th2" by simp - hence h1: "(Th th1', Th th2) \ (RAG s)^+" - by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp) - from th1'_in have h2: "(Th th1', Th th1) \ (RAG s)^+" - by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp) - show ?thesis - proof(rule dchain_unique[OF h1 _ h2, symmetric]) - from runing_1 show "th1 \ readys s" by (simp add:runing_def) - from runing_2 show "th2 \ readys s" by (simp add:runing_def) - qed + from et show ext': "extend_highest_gen s th prio tm t'" + by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt) qed qed qed -lemma "card (runing s) \ 1" -apply(subgoal_tac "finite (runing s)") -prefer 2 -apply (metis finite_nat_set_iff_bounded lessI runing_unique) -apply(rule ccontr) -apply(simp) -apply(case_tac "Suc (Suc 0) \ card (runing s)") -apply(subst (asm) card_le_Suc_iff) -apply(simp) -apply(auto)[1] -apply (metis insertCI runing_unique) -apply(auto) -done - -end - - -lemma create_pre: - assumes stp: "step s e" - and not_in: "th \ threads s" - and is_in: "th \ threads (e#s)" - obtains prio where "e = Create th prio" -proof - - from assms - show ?thesis - proof(cases) - case (thread_create thread prio) - with is_in not_in have "e = Create th prio" by simp - from that[OF this] show ?thesis . - next - case (thread_exit thread) - with assms show ?thesis by (auto intro!:that) - next - case (thread_P thread) - with assms show ?thesis by (auto intro!:that) - next - case (thread_V thread) - with assms show ?thesis by (auto intro!:that) - next - case (thread_set thread) - with assms show ?thesis by (auto intro!:that) - qed -qed - -lemma length_down_to_in: - assumes le_ij: "i \ j" - and le_js: "j \ length s" - shows "length (down_to j i s) = j - i" +lemma th_kept: "th \ threads (t @ s) \ + preced th (t@s) = preced th s" (is "?Q t") proof - - have "length (down_to j i s) = length (from_to i j (rev s))" - by (unfold down_to_def, auto) - also have "\ = j - i" - proof(rule length_from_to_in[OF le_ij]) - from le_js show "j \ length (rev s)" by simp - qed - finally show ?thesis . -qed - - -lemma moment_head: - assumes le_it: "Suc i \ length t" - obtains e where "moment (Suc i) t = e#moment i t" -proof - - have "i \ Suc i" by simp - from length_down_to_in [OF this le_it] - have "length (down_to (Suc i) i t) = 1" by auto - then obtain e where "down_to (Suc i) i t = [e]" - apply (cases "(down_to (Suc i) i t)") by auto - moreover have "down_to (Suc i) 0 t = down_to (Suc i) i t @ down_to i 0 t" - by (rule down_to_conc[symmetric], auto) - ultimately have eq_me: "moment (Suc i) t = e#(moment i t)" - by (auto simp:down_to_moment) - from that [OF this] show ?thesis . -qed - -context valid_trace -begin - -lemma cnp_cnv_eq: - assumes "th \ threads s" - shows "cntP s th = cntV s th" - using assms - using cnp_cnv_cncs not_thread_cncs by auto - -end - - -lemma eq_RAG: - "RAG (wq s) = RAG s" -by (unfold cs_RAG_def s_RAG_def, auto) - -context valid_trace -begin - -lemma count_eq_dependants: - assumes eq_pv: "cntP s th = cntV s th" - shows "dependants (wq s) th = {}" -proof - - from cnp_cnv_cncs and eq_pv - have "cntCS s th = 0" - by (auto split:if_splits) - moreover have "finite {cs. (Cs cs, Th th) \ RAG s}" - proof - - from finite_holding[of th] show ?thesis - by (simp add:holdents_test) - qed - ultimately have h: "{cs. (Cs cs, Th th) \ RAG s} = {}" - by (unfold cntCS_def holdents_test cs_dependants_def, auto) show ?thesis - proof(unfold cs_dependants_def) - { assume "{th'. (Th th', Th th) \ (RAG (wq s))\<^sup>+} \ {}" - then obtain th' where "(Th th', Th th) \ (RAG (wq s))\<^sup>+" by auto - hence "False" - proof(cases) - assume "(Th th', Th th) \ RAG (wq s)" - thus "False" by (auto simp:cs_RAG_def) - next - fix c - assume "(c, Th th) \ RAG (wq s)" - with h and eq_RAG show "False" - by (cases c, auto simp:cs_RAG_def) - qed - } thus "{th'. (Th th', Th th) \ (RAG (wq s))\<^sup>+} = {}" by auto - qed -qed - -lemma dependants_threads: - shows "dependants (wq s) th \ threads s" -proof - { fix th th' - assume h: "th \ {th'a. (Th th'a, Th th') \ (RAG (wq s))\<^sup>+}" - have "Th th \ Domain (RAG s)" - proof - - from h obtain th' where "(Th th, Th th') \ (RAG (wq s))\<^sup>+" by auto - hence "(Th th) \ Domain ( (RAG (wq s))\<^sup>+)" by (auto simp:Domain_def) - with trancl_domain have "(Th th) \ Domain (RAG (wq s))" by simp - thus ?thesis using eq_RAG by simp - qed - from dm_RAG_threads[OF this] - have "th \ threads s" . - } note hh = this - fix th1 - assume "th1 \ dependants (wq s) th" - hence "th1 \ {th'a. (Th th'a, Th th) \ (RAG (wq s))\<^sup>+}" - by (unfold cs_dependants_def, simp) - from hh [OF this] show "th1 \ threads s" . -qed - -lemma finite_threads: - shows "finite (threads s)" -using vt by (induct) (auto elim: step.cases) - -end - -lemma Max_f_mono: - assumes seq: "A \ B" - and np: "A \ {}" - and fnt: "finite B" - shows "Max (f ` A) \ Max (f ` B)" -proof(rule Max_mono) - from seq show "f ` A \ f ` B" by auto -next - from np show "f ` A \ {}" by auto -next - from fnt and seq show "finite (f ` B)" by auto -qed - -context valid_trace -begin - -lemma cp_le: - assumes th_in: "th \ threads s" - shows "cp s th \ Max ((\ th. (preced th s)) ` threads s)" -proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def) - show "Max ((\th. preced th s) ` ({th} \ {th'. (Th th', Th th) \ (RAG (wq s))\<^sup>+})) - \ Max ((\th. preced th s) ` threads s)" - (is "Max (?f ` ?A) \ Max (?f ` ?B)") - proof(rule Max_f_mono) - show "{th} \ {th'. (Th th', Th th) \ (RAG (wq s))\<^sup>+} \ {}" by simp - next - from finite_threads - show "finite (threads s)" . - next - from th_in - show "{th} \ {th'. (Th th', Th th) \ (RAG (wq s))\<^sup>+} \ threads s" - apply (auto simp:Domain_def) - apply (rule_tac dm_RAG_threads) - apply (unfold trancl_domain [of "RAG s", symmetric]) - by (unfold cs_RAG_def s_RAG_def, auto simp:Domain_def) - qed -qed - -lemma le_cp: - shows "preced th s \ cp s th" -proof(unfold cp_eq_cpreced preced_def cpreced_def, simp) - show "Prc (priority th s) (last_set th s) - \ Max (insert (Prc (priority th s) (last_set th s)) - ((\th. Prc (priority th s) (last_set th s)) ` dependants (wq s) th))" - (is "?l \ Max (insert ?l ?A)") - proof(cases "?A = {}") - case False - have "finite ?A" (is "finite (?f ` ?B)") - proof - - have "finite ?B" - proof- - have "finite {th'. (Th th', Th th) \ (RAG (wq s))\<^sup>+}" - proof - - let ?F = "\ (x, y). the_th x" - have "{th'. (Th th', Th th) \ (RAG (wq s))\<^sup>+} \ ?F ` ((RAG (wq s))\<^sup>+)" - apply (auto simp:image_def) - by (rule_tac x = "(Th x, Th th)" in bexI, auto) - moreover have "finite \" - proof - - from finite_RAG have "finite (RAG s)" . - hence "finite ((RAG (wq s))\<^sup>+)" - apply (unfold finite_trancl) - by (auto simp: s_RAG_def cs_RAG_def wq_def) - thus ?thesis by auto - qed - ultimately show ?thesis by (auto intro:finite_subset) - qed - thus ?thesis by (simp add:cs_dependants_def) - qed - thus ?thesis by simp - qed - from Max_insert [OF this False, of ?l] show ?thesis by auto + proof(induct rule:ind) + case Nil + from threads_s + show ?case + by auto next - case True - thus ?thesis by auto - qed -qed - -lemma max_cp_eq: - shows "Max ((cp s) ` threads s) = Max ((\ th. (preced th s)) ` threads s)" - (is "?l = ?r") -proof(cases "threads s = {}") - case True - thus ?thesis by auto -next - case False - have "?l \ ((cp s) ` threads s)" - proof(rule Max_in) - from finite_threads - show "finite (cp s ` threads s)" by auto - next - from False show "cp s ` threads s \ {}" by auto - qed - then obtain th - where th_in: "th \ threads s" and eq_l: "?l = cp s th" by auto - have "\ \ ?r" by (rule cp_le[OF th_in]) - moreover have "?r \ cp s th" (is "Max (?f ` ?A) \ cp s th") - proof - - have "?r \ (?f ` ?A)" - proof(rule Max_in) - from finite_threads - show " finite ((\th. preced th s) ` threads s)" by auto - next - from False show " (\th. preced th s) ` threads s \ {}" by auto - qed - then obtain th' where - th_in': "th' \ ?A " and eq_r: "?r = ?f th'" by auto - from le_cp [of th'] eq_r - have "?r \ cp s th'" by auto - moreover have "\ \ cp s th" - proof(fold eq_l) - show " cp s th' \ Max (cp s ` threads s)" - proof(rule Max_ge) - from th_in' show "cp s th' \ cp s ` threads s" - by auto - next - from finite_threads - show "finite (cp s ` threads s)" by auto - qed - qed - ultimately show ?thesis by auto - qed - ultimately show ?thesis using eq_l by auto -qed - -lemma max_cp_readys_threads_pre: - assumes np: "threads s \ {}" - shows "Max (cp s ` readys s) = Max (cp s ` threads s)" -proof(unfold max_cp_eq) - show "Max (cp s ` readys s) = Max ((\th. preced th s) ` threads s)" - proof - - let ?p = "Max ((\th. preced th s) ` threads s)" - let ?f = "(\th. preced th s)" - have "?p \ ((\th. preced th s) ` threads s)" - proof(rule Max_in) - from finite_threads show "finite (?f ` threads s)" by simp - next - from np show "?f ` threads s \ {}" by simp - qed - then obtain tm where tm_max: "?f tm = ?p" and tm_in: "tm \ threads s" - by (auto simp:Image_def) - from th_chain_to_ready [OF tm_in] - have "tm \ readys s \ (\th'. th' \ readys s \ (Th tm, Th th') \ (RAG s)\<^sup>+)" . - thus ?thesis - proof - assume "\th'. th' \ readys s \ (Th tm, Th th') \ (RAG s)\<^sup>+ " - then obtain th' where th'_in: "th' \ readys s" - and tm_chain:"(Th tm, Th th') \ (RAG s)\<^sup>+" by auto - have "cp s th' = ?f tm" - proof(subst cp_eq_cpreced, subst cpreced_def, rule Max_eqI) - from dependants_threads finite_threads - show "finite ((\th. preced th s) ` ({th'} \ dependants (wq s) th'))" - by (auto intro:finite_subset) - next - fix p assume p_in: "p \ (\th. preced th s) ` ({th'} \ dependants (wq s) th')" - from tm_max have " preced tm s = Max ((\th. preced th s) ` threads s)" . - moreover have "p \ \" - proof(rule Max_ge) - from finite_threads - show "finite ((\th. preced th s) ` threads s)" by simp - next - from p_in and th'_in and dependants_threads[of th'] - show "p \ (\th. preced th s) ` threads s" - by (auto simp:readys_def) + case (Cons e t) + interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto + interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto + show ?case + proof(cases e) + case (Create thread prio) + show ?thesis + proof - + from Cons and Create have "step (t@s) (Create thread prio)" by auto + hence "th \ thread" + proof(cases) + case thread_create + with Cons show ?thesis by auto qed - ultimately show "p \ preced tm s" by auto - next - show "preced tm s \ (\th. preced th s) ` ({th'} \ dependants (wq s) th')" - proof - - from tm_chain - have "tm \ dependants (wq s) th'" - by (unfold cs_dependants_def s_RAG_def cs_RAG_def, auto) - thus ?thesis by auto - qed - qed - with tm_max - have h: "cp s th' = Max ((\th. preced th s) ` threads s)" by simp - show ?thesis - proof (fold h, rule Max_eqI) - fix q - assume "q \ cp s ` readys s" - then obtain th1 where th1_in: "th1 \ readys s" - and eq_q: "q = cp s th1" by auto - show "q \ cp s th'" - apply (unfold h eq_q) - apply (unfold cp_eq_cpreced cpreced_def) - apply (rule Max_mono) - proof - - from dependants_threads [of th1] th1_in - show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) \ - (\th. preced th s) ` threads s" - by (auto simp:readys_def) - next - show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) \ {}" by simp - next - from finite_threads - show " finite ((\th. preced th s) ` threads s)" by simp - qed - next - from finite_threads - show "finite (cp s ` readys s)" by (auto simp:readys_def) - next - from th'_in - show "cp s th' \ cp s ` readys s" by simp + hence "preced th ((e # t) @ s) = preced th (t @ s)" + by (unfold Create, auto simp:preced_def) + moreover note Cons + ultimately show ?thesis + by (auto simp:Create) qed next - assume tm_ready: "tm \ readys s" + case (Exit thread) + from h_e.exit_diff and Exit + have neq_th: "thread \ th" by auto + with Cons show ?thesis - proof(fold tm_max) - have cp_eq_p: "cp s tm = preced tm s" - proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI) - fix y - assume hy: "y \ (\th. preced th s) ` ({tm} \ dependants (wq s) tm)" - show "y \ preced tm s" - proof - - { fix y' - assume hy' : "y' \ ((\th. preced th s) ` dependants (wq s) tm)" - have "y' \ preced tm s" - proof(unfold tm_max, rule Max_ge) - from hy' dependants_threads[of tm] - show "y' \ (\th. preced th s) ` threads s" by auto - next - from finite_threads - show "finite ((\th. preced th s) ` threads s)" by simp - qed - } with hy show ?thesis by auto - qed - next - from dependants_threads[of tm] finite_threads - show "finite ((\th. preced th s) ` ({tm} \ dependants (wq s) tm))" - by (auto intro:finite_subset) - next - show "preced tm s \ (\th. preced th s) ` ({tm} \ dependants (wq s) tm)" - by simp - qed - moreover have "Max (cp s ` readys s) = cp s tm" - proof(rule Max_eqI) - from tm_ready show "cp s tm \ cp s ` readys s" by simp - next - from finite_threads - show "finite (cp s ` readys s)" by (auto simp:readys_def) - next - fix y assume "y \ cp s ` readys s" - then obtain th1 where th1_readys: "th1 \ readys s" - and h: "y = cp s th1" by auto - show "y \ cp s tm" - apply(unfold cp_eq_p h) - apply(unfold cp_eq_cpreced cpreced_def tm_max, rule Max_mono) - proof - - from finite_threads - show "finite ((\th. preced th s) ` threads s)" by simp - next - show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) \ {}" - by simp - next - from dependants_threads[of th1] th1_readys - show "(\th. preced th s) ` ({th1} \ dependants (wq s) th1) - \ (\th. preced th s) ` threads s" - by (auto simp:readys_def) - qed - qed - ultimately show " Max (cp s ` readys s) = preced tm s" by simp - qed + by (unfold Exit, auto simp:preced_def) + next + case (P thread cs) + with Cons + show ?thesis + by (auto simp:P preced_def) + next + case (V thread cs) + with Cons + show ?thesis + by (auto simp:V preced_def) + next + case (Set thread prio') + show ?thesis + proof - + from h_e.set_diff_low and Set + have "th \ thread" by auto + hence "preced th ((e # t) @ s) = preced th (t @ s)" + by (unfold Set, auto simp:preced_def) + moreover note Cons + ultimately show ?thesis + by (auto simp:Set) + qed qed qed qed -text {* (* ccc *) \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. -*} -lemma max_cp_readys_threads: - shows "Max (cp s ` readys s) = Max (cp s ` threads s)" -proof(cases "threads s = {}") - case True - thus ?thesis - by (auto simp:readys_def) -next - case False - show ?thesis by (rule max_cp_readys_threads_pre[OF False]) -qed - -end - -lemma eq_holding: "holding (wq s) th cs = holding s th cs" - apply (unfold s_holding_def cs_holding_def wq_def, simp) - done - -lemma f_image_eq: - assumes h: "\ a. a \ A \ f a = g a" - shows "f ` A = g ` A" -proof - show "f ` A \ g ` A" - by(rule image_subsetI, auto intro:h) -next - show "g ` A \ f ` A" - by (rule image_subsetI, auto intro:h[symmetric]) -qed - - -definition detached :: "state \ thread \ bool" - where "detached s th \ (\(\ cs. holding s th cs)) \ (\(\cs. waiting s th cs))" - - -lemma detached_test: - shows "detached s th = (Th th \ Field (RAG s))" -apply(simp add: detached_def Field_def) -apply(simp add: s_RAG_def) -apply(simp add: s_holding_abv s_waiting_abv) -apply(simp add: Domain_iff Range_iff) -apply(simp add: wq_def) -apply(auto) -done - -context valid_trace -begin - -lemma detached_intro: - assumes eq_pv: "cntP s th = cntV s th" - shows "detached s th" -proof - - from cnp_cnv_cncs - have eq_cnt: "cntP s th = - cntV s th + (if th \ readys s \ th \ threads s then cntCS s th else cntCS s th + 1)" . - hence cncs_zero: "cntCS s th = 0" - by (auto simp:eq_pv split:if_splits) - with eq_cnt - have "th \ readys s \ th \ threads s" by (auto simp:eq_pv) - thus ?thesis - proof - assume "th \ threads s" - with range_in dm_RAG_threads - show ?thesis - by (auto simp add: detached_def s_RAG_def s_waiting_abv s_holding_abv wq_def Domain_iff Range_iff) - next - assume "th \ readys s" - moreover have "Th th \ Range (RAG s)" - proof - - from card_0_eq [OF finite_holding] and cncs_zero - have "holdents s th = {}" - by (simp add:cntCS_def) - thus ?thesis - apply(auto simp:holdents_test) - apply(case_tac a) - apply(auto simp:holdents_test s_RAG_def) - done - qed - ultimately show ?thesis - by (auto simp add: detached_def s_RAG_def s_waiting_abv s_holding_abv wq_def readys_def) - qed -qed +text {* + According to @{thm th_kept}, thread @{text "th"} has its living status + and precedence kept along the way of @{text "t"}. The following lemma + shows that this preserved precedence of @{text "th"} remains as the highest + along the way of @{text "t"}. -lemma detached_elim: - assumes dtc: "detached s th" - shows "cntP s th = cntV s th" -proof - - from cnp_cnv_cncs - have eq_pv: " cntP s th = - cntV s th + (if th \ readys s \ th \ threads s then cntCS s th else cntCS s th + 1)" . - have cncs_z: "cntCS s th = 0" - proof - - from dtc have "holdents s th = {}" - unfolding detached_def holdents_test s_RAG_def - by (simp add: s_waiting_abv wq_def s_holding_abv Domain_iff Range_iff) - thus ?thesis by (auto simp:cntCS_def) - qed - show ?thesis - proof(cases "th \ threads s") - case True - with dtc - have "th \ readys s" - by (unfold readys_def detached_def Field_def Domain_def Range_def, - auto simp:eq_waiting s_RAG_def) - with cncs_z and eq_pv show ?thesis by simp - next - case False - with cncs_z and eq_pv show ?thesis by simp - qed -qed - -lemma detached_eq: - shows "(detached s th) = (cntP s th = cntV s th)" - by (insert vt, auto intro:detached_intro detached_elim) - -end - -text {* - The lemmas in this .thy file are all obvious lemmas, however, they still needs to be derived - from the concise and miniature model of PIP given in PrioGDef.thy. -*} - -lemma eq_dependants: "dependants (wq s) = dependants s" - by (simp add: s_dependants_abv wq_def) - -lemma next_th_unique: - assumes nt1: "next_th s th cs th1" - and nt2: "next_th s th cs th2" - shows "th1 = th2" -using assms by (unfold next_th_def, auto) - -lemma birth_time_lt: "s \ [] \ last_set th s < length s" - apply (induct s, simp) -proof - - fix a s - assume ih: "s \ [] \ last_set th s < length s" - and eq_as: "a # s \ []" - show "last_set th (a # s) < length (a # s)" - proof(cases "s \ []") - case False - from False show ?thesis - by (cases a, auto simp:last_set.simps) - next - case True - from ih [OF True] show ?thesis - by (cases a, auto simp:last_set.simps) - qed -qed - -lemma th_in_ne: "th \ threads s \ s \ []" - by (induct s, auto simp:threads.simps) - -lemma preced_tm_lt: "th \ threads s \ preced th s = Prc x y \ y < length s" - apply (drule_tac th_in_ne) - by (unfold preced_def, auto intro: birth_time_lt) - -text {* @{text "the_preced"} is also the same as @{text "preced"}, the only - difference is the order of arguemts. *} -definition "the_preced s th = preced th s" - -lemma inj_the_preced: - "inj_on (the_preced s) (threads s)" - by (metis inj_onI preced_unique the_preced_def) - -text {* @{term "the_thread"} extracts thread out of RAG node. *} -fun the_thread :: "node \ thread" where - "the_thread (Th th) = th" - -text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *} -definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}" - -text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *} -definition "hRAG (s::state) = {(Cs cs, Th th) | th cs. holding s th cs}" + The proof goes by induction over @{text "t"} using the specialized + induction rule @{thm ind}, followed by case analysis of each possible + operations of PIP. All cases follow the same pattern rendered by the + generalized introduction rule @{thm "image_Max_eqI"}. -text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *} -lemma RAG_split: "RAG s = (wRAG s \ hRAG s)" - by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv - s_holding_abv cs_RAG_def, auto) - -text {* - The following @{text "tRAG"} is the thread-graph derived from @{term "RAG"}. - It characterizes the dependency between threads when calculating current - precedences. It is defined as the composition of the above two sub-graphs, - names @{term "wRAG"} and @{term "hRAG"}. - *} -definition "tRAG s = wRAG s O hRAG s" - -(* ccc *) - -definition "cp_gen s x = - Max ((the_preced s \ the_thread) ` subtree (tRAG s) x)" - -lemma tRAG_alt_def: - "tRAG s = {(Th th1, Th th2) | th1 th2. - \ cs. (Th th1, Cs cs) \ RAG s \ (Cs cs, Th th2) \ RAG s}" - by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def) - -lemma tRAG_Field: - "Field (tRAG s) \ Field (RAG s)" - by (unfold tRAG_alt_def Field_def, auto) - -lemma tRAG_ancestorsE: - assumes "x \ ancestors (tRAG s) u" - obtains th where "x = Th th" -proof - - from assms have "(u, x) \ (tRAG s)^+" - by (unfold ancestors_def, auto) - from tranclE[OF this] obtain c where "(c, x) \ tRAG s" by auto - then obtain th where "x = Th th" - by (unfold tRAG_alt_def, auto) - from that[OF this] show ?thesis . -qed - -lemma tRAG_mono: - assumes "RAG s' \ RAG s" - shows "tRAG s' \ tRAG s" - using assms - by (unfold tRAG_alt_def, auto) - -lemma holding_next_thI: - assumes "holding s th cs" - and "length (wq s cs) > 1" - obtains th' where "next_th s th cs th'" -proof - - from assms(1)[folded eq_holding, unfolded cs_holding_def] - have " th \ set (wq s cs) \ th = hd (wq s cs)" . - then obtain rest where h1: "wq s cs = th#rest" - by (cases "wq s cs", auto) - with assms(2) have h2: "rest \ []" by auto - let ?th' = "hd (SOME q. distinct q \ set q = set rest)" - have "next_th s th cs ?th'" using h1(1) h2 - by (unfold next_th_def, auto) - from that[OF this] show ?thesis . -qed - -lemma RAG_tRAG_transfer: - assumes "vt s'" - assumes "RAG s = RAG s' \ {(Th th, Cs cs)}" - and "(Cs cs, Th th'') \ RAG s'" - shows "tRAG s = tRAG s' \ {(Th th, Th th'')}" (is "?L = ?R") -proof - - interpret vt_s': valid_trace "s'" using assms(1) - by (unfold_locales, simp) - interpret rtree: rtree "RAG s'" - proof - show "single_valued (RAG s')" - apply (intro_locales) - by (unfold single_valued_def, - auto intro:vt_s'.unique_RAG) - - show "acyclic (RAG s')" - by (rule vt_s'.acyclic_RAG) - qed - { fix n1 n2 - assume "(n1, n2) \ ?L" - from this[unfolded tRAG_alt_def] - obtain th1 th2 cs' where - h: "n1 = Th th1" "n2 = Th th2" - "(Th th1, Cs cs') \ RAG s" - "(Cs cs', Th th2) \ RAG s" by auto - from h(4) and assms(2) have cs_in: "(Cs cs', Th th2) \ RAG s'" by auto - from h(3) and assms(2) - have "(Th th1, Cs cs') = (Th th, Cs cs) \ - (Th th1, Cs cs') \ RAG s'" by auto - hence "(n1, n2) \ ?R" - proof - assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)" - hence eq_th1: "th1 = th" by simp - moreover have "th2 = th''" - proof - - from h1 have "cs' = cs" by simp - from assms(3) cs_in[unfolded this] rtree.sgv - show ?thesis - by (unfold single_valued_def, auto) + The very essence is to show that precedences, no matter whether they + are newly introduced or modified, are always lower than the one held + by @{term "th"}, which by @{thm th_kept} is preserved along the way. +*} +lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s" +proof(induct rule:ind) + case Nil + from highest_preced_thread + show ?case by simp +next + case (Cons e t) + interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto + interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto + show ?case + proof(cases e) + case (Create thread prio') + show ?thesis (is "Max (?f ` ?A) = ?t") + proof - + -- {* The following is the common pattern of each branch of the case analysis. *} + -- {* The major part is to show that @{text "th"} holds the highest precedence: *} + have "Max (?f ` ?A) = ?f th" + proof(rule image_Max_eqI) + show "finite ?A" using h_e.finite_threads by auto + next + show "th \ ?A" using h_e.th_kept by auto + next + show "\x\?A. ?f x \ ?f th" + proof + fix x + assume "x \ ?A" + hence "x = thread \ x \ threads (t@s)" by (auto simp:Create) + thus "?f x \ ?f th" + proof + assume "x = thread" + thus ?thesis + apply (simp add:Create the_preced_def preced_def, fold preced_def) + using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 + preced_th by force + next + assume h: "x \ threads (t @ s)" + from Cons(2)[unfolded Create] + have "x \ thread" using h by (cases, auto) + hence "?f x = the_preced (t@s) x" + by (simp add:Create the_preced_def preced_def) + hence "?f x \ Max (the_preced (t@s) ` threads (t@s))" + by (simp add: h_t.finite_threads h) + also have "... = ?f th" + by (metis Cons.hyps(5) h_e.th_kept the_preced_def) + finally show ?thesis . + qed + qed qed - ultimately show ?thesis using h(1,2) by auto - next - assume "(Th th1, Cs cs') \ RAG s'" - with cs_in have "(Th th1, Th th2) \ tRAG s'" - by (unfold tRAG_alt_def, auto) - from this[folded h(1, 2)] show ?thesis by auto - qed - } moreover { - fix n1 n2 - assume "(n1, n2) \ ?R" - hence "(n1, n2) \tRAG s' \ (n1, n2) = (Th th, Th th'')" by auto - hence "(n1, n2) \ ?L" - proof - assume "(n1, n2) \ tRAG s'" - moreover have "... \ ?L" - proof(rule tRAG_mono) - show "RAG s' \ RAG s" by (unfold assms(2), auto) + -- {* The minor part is to show that the precedence of @{text "th"} + equals to preserved one, given by the foregoing lemma @{thm th_kept} *} + also have "... = ?t" using h_e.th_kept the_preced_def by auto + -- {* Then it follows trivially that the precedence preserved + for @{term "th"} remains the maximum of all living threads along the way. *} + finally show ?thesis . + qed + next + case (Exit thread) + show ?thesis (is "Max (?f ` ?A) = ?t") + proof - + have "Max (?f ` ?A) = ?f th" + proof(rule image_Max_eqI) + show "finite ?A" using h_e.finite_threads by auto + next + show "th \ ?A" using h_e.th_kept by auto + next + show "\x\?A. ?f x \ ?f th" + proof + fix x + assume "x \ ?A" + hence "x \ threads (t@s)" by (simp add: Exit) + hence "?f x \ Max (?f ` threads (t@s))" + by (simp add: h_t.finite_threads) + also have "... \ ?f th" + apply (simp add:Exit the_preced_def preced_def, fold preced_def) + using Cons.hyps(5) h_t.th_kept the_preced_def by auto + finally show "?f x \ ?f th" . + qed qed - ultimately show ?thesis by auto - next - assume eq_n: "(n1, n2) = (Th th, Th th'')" - from assms(2, 3) have "(Cs cs, Th th'') \ RAG s" by auto - moreover have "(Th th, Cs cs) \ RAG s" using assms(2) by auto - ultimately show ?thesis - by (unfold eq_n tRAG_alt_def, auto) - qed - } ultimately show ?thesis by auto -qed - -context valid_trace -begin - -lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt] - -end - -lemma cp_alt_def: - "cp s th = - Max ((the_preced s) ` {th'. Th th' \ (subtree (RAG s) (Th th))})" -proof - - have "Max (the_preced s ` ({th} \ dependants (wq s) th)) = - Max (the_preced s ` {th'. Th th' \ 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 cp_gen_alt_def: - "cp_gen s = (Max \ (\x. (the_preced s \ the_thread) ` subtree (tRAG s) x))" - by (auto simp:cp_gen_def) - -lemma tRAG_nodeE: - assumes "(n1, n2) \ tRAG s" - obtains th1 th2 where "n1 = Th th1" "n2 = Th th2" - using assms - by (auto simp: tRAG_def wRAG_def hRAG_def tRAG_def) - -lemma subtree_nodeE: - assumes "n \ subtree (tRAG s) (Th th)" - obtains th1 where "n = Th th1" -proof - - show ?thesis - proof(rule subtreeE[OF assms]) - assume "n = Th th" - from that[OF this] show ?thesis . + also have "... = ?t" using h_e.th_kept the_preced_def by auto + finally show ?thesis . + qed + next + case (P thread cs) + with Cons + show ?thesis by (auto simp:preced_def the_preced_def) next - assume "Th th \ ancestors (tRAG s) n" - hence "(n, Th th) \ (tRAG s)^+" by (auto simp:ancestors_def) - hence "\ th1. n = Th th1" - proof(induct) - case (base y) - from tRAG_nodeE[OF this] show ?case by metis - next - case (step y z) - thus ?case by auto - qed - with that show ?thesis by auto + case (V thread cs) + with Cons + show ?thesis by (auto simp:preced_def the_preced_def) + next + case (Set thread prio') + show ?thesis (is "Max (?f ` ?A) = ?t") + proof - + have "Max (?f ` ?A) = ?f th" + proof(rule image_Max_eqI) + show "finite ?A" using h_e.finite_threads by auto + next + show "th \ ?A" using h_e.th_kept by auto + next + show "\x\?A. ?f x \ ?f th" + proof + fix x + assume h: "x \ ?A" + show "?f x \ ?f th" + proof(cases "x = thread") + case True + moreover have "the_preced (Set thread prio' # t @ s) thread \ the_preced (t @ s) th" + proof - + have "the_preced (t @ s) th = Prc prio tm" + using h_t.th_kept preced_th by (simp add:the_preced_def) + moreover have "prio' \ prio" using Set h_e.set_diff_low by auto + ultimately show ?thesis by (insert lt_tm, auto simp:the_preced_def preced_def) + qed + ultimately show ?thesis + by (unfold Set, simp add:the_preced_def preced_def) + next + case False + then have "?f x = the_preced (t@s) x" + by (simp add:the_preced_def preced_def Set) + also have "... \ Max (the_preced (t@s) ` threads (t@s))" + using Set h h_t.finite_threads by auto + also have "... = ?f th" by (metis Cons.hyps(5) h_e.th_kept the_preced_def) + finally show ?thesis . + qed + qed + qed + also have "... = ?t" using h_e.th_kept the_preced_def by auto + finally show ?thesis . + qed qed qed -lemma tRAG_star_RAG: "(tRAG s)^* \ (RAG s)^*" +lemma max_preced: "preced th (t@s) = Max (the_preced (t@s) ` (threads (t@s)))" + by (insert th_kept max_kept, auto) + +text {* + The reason behind the following lemma is that: + Since @{term "cp"} is defined as the maximum precedence + of those threads contained in the sub-tree of node @{term "Th th"} + in @{term "RAG (t@s)"}, and all these threads are living threads, and + @{term "th"} is also among them, the maximum precedence of + them all must be the one for @{text "th"}. +*} +lemma th_cp_max_preced: + "cp (t@s) th = Max (the_preced (t@s) ` (threads (t@s)))" (is "?L = ?R") proof - - have "(wRAG s O hRAG s)^* \ (RAG s O RAG s)^*" - by (rule rtrancl_mono, auto simp:RAG_split) - also have "... \ ((RAG s)^*)^*" - by (rule rtrancl_mono, auto) - also have "... = (RAG s)^*" by simp - finally show ?thesis by (unfold tRAG_def, simp) + let ?f = "the_preced (t@s)" + have "?L = ?f th" + proof(unfold cp_alt_def, rule image_Max_eqI) + show "finite {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" + proof - + have "{th'. Th th' \ subtree (RAG (t @ s)) (Th th)} = + the_thread ` {n . n \ subtree (RAG (t @ s)) (Th th) \ + (\ th'. n = Th th')}" + by (smt Collect_cong Setcompr_eq_image mem_Collect_eq the_thread.simps) + moreover have "finite ..." by (simp add: vat_t.fsbtRAGs.finite_subtree) + ultimately show ?thesis by simp + qed + next + show "th \ {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" + by (auto simp:subtree_def) + next + show "\x\{th'. Th th' \ subtree (RAG (t @ s)) (Th th)}. + the_preced (t @ s) x \ the_preced (t @ s) th" + proof + fix th' + assume "th' \ {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" + hence "Th th' \ subtree (RAG (t @ s)) (Th th)" by auto + moreover have "... \ Field (RAG (t @ s)) \ {Th th}" + by (meson subtree_Field) + ultimately have "Th th' \ ..." by auto + hence "th' \ threads (t@s)" + proof + assume "Th th' \ {Th th}" + thus ?thesis using th_kept by auto + next + assume "Th th' \ Field (RAG (t @ s))" + thus ?thesis using vat_t.not_in_thread_isolated by blast + qed + thus "the_preced (t @ s) th' \ the_preced (t @ s) th" + by (metis Max_ge finite_imageI finite_threads image_eqI + max_kept th_kept the_preced_def) + qed + qed + also have "... = ?R" by (simp add: max_preced the_preced_def) + finally show ?thesis . qed -lemma tRAG_subtree_RAG: "subtree (tRAG s) x \ subtree (RAG s) x" +lemma th_cp_max[simp]: "Max (cp (t@s) ` threads (t@s)) = cp (t@s) th" + using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger + +lemma [simp]: "Max (cp (t@s) ` threads (t@s)) = Max (the_preced (t@s) ` threads (t@s))" + by (simp add: th_cp_max_preced) + +lemma [simp]: "Max (the_preced (t@s) ` threads (t@s)) = the_preced (t@s) th" + using max_kept th_kept the_preced_def by auto + +lemma [simp]: "the_preced (t@s) th = preced th (t@s)" + using the_preced_def by auto + +lemma [simp]: "preced th (t@s) = preced th s" + by (simp add: th_kept) + +lemma [simp]: "cp s th = preced th s" + by (simp add: eq_cp_s_th) + +lemma th_cp_preced [simp]: "cp (t@s) th = preced th s" + by (fold max_kept, unfold th_cp_max_preced, simp) + +lemma preced_less: + assumes th'_in: "th' \ threads s" + and neq_th': "th' \ th" + shows "preced th' s < preced th s" + using assms +by (metis Max.coboundedI finite_imageI highest not_le order.trans + preced_linorder rev_image_eqI threads_s vat_s.finite_threads + vat_s.le_cp) + +section {* The `blocking thread` *} + +text {* + + The purpose of PIP is to ensure that the most urgent thread @{term + th} is not blocked unreasonably. Therefore, below, we will derive + properties of the blocking thread. By blocking thread, we mean a + thread in running state t @ s, but is different from thread @{term + th}. + + The first lemmas shows that the @{term cp}-value of the blocking + thread @{text th'} equals to the highest precedence in the whole + system. + +*} + +lemma runing_preced_inversion: + assumes runing': "th' \ runing (t @ s)" + shows "cp (t @ s) th' = preced th s" proof - - { fix a - assume "a \ subtree (tRAG s) x" - hence "(a, x) \ (tRAG s)^*" by (auto simp:subtree_def) - with tRAG_star_RAG[of s] - have "(a, x) \ (RAG s)^*" by auto - hence "a \ subtree (RAG s) x" by (auto simp:subtree_def) - } thus ?thesis by auto + have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" + using assms by (unfold runing_def, auto) + also have "\ = preced th s" + by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) + finally show ?thesis . qed -lemma tRAG_trancl_eq: - "{th'. (Th th', Th th) \ (tRAG s)^+} = - {th'. (Th th', Th th) \ (RAG s)^+}" - (is "?L = ?R") -proof - - { fix th' - assume "th' \ ?L" - hence "(Th th', Th th) \ (tRAG s)^+" by auto - from tranclD[OF this] - obtain z where h: "(Th th', z) \ tRAG s" "(z, Th th) \ (tRAG s)\<^sup>*" by auto - from tRAG_subtree_RAG[of s] and this(2) - have "(z, Th th) \ (RAG s)^*" by (meson subsetCE tRAG_star_RAG) - moreover from h(1) have "(Th th', z) \ (RAG s)^+" using tRAG_alt_def by auto - ultimately have "th' \ ?R" by auto - } moreover - { fix th' - assume "th' \ ?R" - hence "(Th th', Th th) \ (RAG s)^+" by (auto) - from plus_rpath[OF this] - obtain xs where rp: "rpath (RAG s) (Th th') xs (Th th)" "xs \ []" by auto - hence "(Th th', Th th) \ (tRAG s)^+" - proof(induct xs arbitrary:th' th rule:length_induct) - case (1 xs th' th) - then obtain x1 xs1 where Cons1: "xs = x1#xs1" by (cases xs, auto) - show ?case - proof(cases "xs1") - case Nil - from 1(2)[unfolded Cons1 Nil] - have rp: "rpath (RAG s) (Th th') [x1] (Th th)" . - hence "(Th th', x1) \ (RAG s)" by (cases, simp) - then obtain cs where "x1 = Cs cs" - by (unfold s_RAG_def, auto) - from rpath_nnl_lastE[OF rp[unfolded this]] - show ?thesis by auto - next - case (Cons x2 xs2) - from 1(2)[unfolded Cons1[unfolded this]] - have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" . - from rpath_edges_on[OF this] - have eds: "edges_on (Th th' # x1 # x2 # xs2) \ RAG s" . - have "(Th th', x1) \ edges_on (Th th' # x1 # x2 # xs2)" - by (simp add: edges_on_unfold) - with eds have rg1: "(Th th', x1) \ RAG s" by auto - then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto) - have "(x1, x2) \ edges_on (Th th' # x1 # x2 # xs2)" - by (simp add: edges_on_unfold) - from this eds - have rg2: "(x1, x2) \ RAG s" by auto - from this[unfolded eq_x1] - obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto) - from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2] - have rt1: "(Th th', Th th1) \ tRAG s" by (unfold tRAG_alt_def, auto) - from rp have "rpath (RAG s) x2 xs2 (Th th)" - by (elim rpath_ConsE, simp) - from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" . - show ?thesis - proof(cases "xs2 = []") - case True - from rpath_nilE[OF rp'[unfolded this]] - have "th1 = th" by auto - from rt1[unfolded this] show ?thesis by auto - next - case False - from 1(1)[rule_format, OF _ rp' this, unfolded Cons1 Cons] - have "(Th th1, Th th) \ (tRAG s)\<^sup>+" by simp - with rt1 show ?thesis by auto - qed +text {* + + The next lemma shows how the counters for @{term "P"} and @{term + "V"} operations relate to the running threads in the states @{term + s} and @{term "t @ s"}: if a thread's @{term "P"}-count equals its + @{term "V"}-count (which means it no longer has any resource in its + possession), it cannot be a running thread. + + The proof is by contraction with the assumption @{text "th' \ th"}. + The key is the use of @{thm count_eq_dependants} to derive the + emptiness of @{text th'}s @{term dependants}-set from the balance of + its @{term P} and @{term V} counts. From this, it can be shown + @{text th'}s @{term cp}-value equals to its own precedence. + + On the other hand, since @{text th'} is running, by @{thm + runing_preced_inversion}, its @{term cp}-value equals to the + precedence of @{term th}. + + Combining the above two results we have that @{text th'} and @{term + th} have the same precedence. By uniqueness of precedences, we have + @{text "th' = th"}, which is in contradiction with the assumption + @{text "th' \ th"}. + +*} + +lemma eq_pv_blocked: (* ddd *) + assumes neq_th': "th' \ th" + and eq_pv: "cntP (t @ s) th' = cntV (t @ s) th'" + shows "th' \ runing (t @ s)" +proof + assume otherwise: "th' \ runing (t @ s)" + show False + proof - + have th'_in: "th' \ threads (t @ s)" + using otherwise readys_threads runing_def by auto + have "th' = th" + proof(rule preced_unique) + -- {* The proof goes like this: + it is first shown that the @{term preced}-value of @{term th'} + equals to that of @{term th}, then by uniqueness + of @{term preced}-values (given by lemma @{thm preced_unique}), + @{term th'} equals to @{term th}: *} + show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R") + proof - + -- {* Since the counts of @{term th'} are balanced, the subtree + of it contains only itself, so, its @{term cp}-value + equals its @{term preced}-value: *} + have "?L = cp (t @ s) th'" + by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp) + -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion}, + its @{term cp}-value equals @{term "preced th s"}, + which equals to @{term "?R"} by simplification: *} + also have "... = ?R" + using runing_preced_inversion[OF otherwise] by simp + finally show ?thesis . qed - qed - hence "th' \ ?L" by auto - } ultimately show ?thesis by blast + qed (auto simp: th'_in th_kept) + with `th' \ th` show ?thesis by simp + qed qed -lemma tRAG_trancl_eq_Th: - "{Th th' | th'. (Th th', Th th) \ (tRAG s)^+} = - {Th th' | th'. (Th th', Th th) \ (RAG s)^+}" - using tRAG_trancl_eq by auto - -lemma dependants_alt_def: - "dependants s th = {th'. (Th th', Th th) \ (tRAG s)^+}" - by (metis eq_RAG s_dependants_def tRAG_trancl_eq) - -context valid_trace -begin - -lemma count_eq_tRAG_plus: - assumes "cntP s th = cntV s th" - shows "{th'. (Th th', Th th) \ (tRAG s)^+} = {}" - using assms count_eq_dependants dependants_alt_def eq_dependants by auto +text {* + The following lemma is the extrapolation of @{thm eq_pv_blocked}. + It says if a thread, different from @{term th}, + does not hold any resource at the very beginning, + it will keep hand-emptied in the future @{term "t@s"}. +*} +lemma eq_pv_persist: (* ddd *) + assumes neq_th': "th' \ th" + and eq_pv: "cntP s th' = cntV s th'" + shows "cntP (t @ s) th' = cntV (t @ s) th'" +proof(induction rule: ind) + -- {* The nontrivial case is for the @{term Cons}: *} + case (Cons e t) + -- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *} + interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp + interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp + show ?case + proof - + -- {* It can be proved that @{term cntP}-value of @{term th'} does not change + by the happening of event @{term e}: *} + have "cntP ((e#t)@s) th' = cntP (t@s) th'" + proof(rule ccontr) -- {* Proof by contradiction. *} + -- {* Suppose @{term cntP}-value of @{term th'} is changed by @{term e}: *} + assume otherwise: "cntP ((e # t) @ s) th' \ cntP (t @ s) th'" + -- {* Then the actor of @{term e} must be @{term th'} and @{term e} + must be a @{term P}-event: *} + hence "isP e" "actor e = th'" by (auto simp:cntP_diff_inv) + with vat_t.actor_inv[OF Cons(2)] + -- {* According to @{thm actor_inv}, @{term th'} must be running at + the moment @{term "t@s"}: *} + have "th' \ runing (t@s)" by (cases e, auto) + -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis + shows @{term th'} can not be running at moment @{term "t@s"}: *} + moreover have "th' \ runing (t@s)" + using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . + -- {* Contradiction is finally derived: *} + ultimately show False by simp + qed + -- {* It can also be proved that @{term cntV}-value of @{term th'} does not change + by the happening of event @{term e}: *} + -- {* The proof follows exactly the same pattern as the case for @{term cntP}-value: *} + moreover have "cntV ((e#t)@s) th' = cntV (t@s) th'" + proof(rule ccontr) -- {* Proof by contradiction. *} + assume otherwise: "cntV ((e # t) @ s) th' \ cntV (t @ s) th'" + hence "isV e" "actor e = th'" by (auto simp:cntV_diff_inv) + with vat_t.actor_inv[OF Cons(2)] + have "th' \ runing (t@s)" by (cases e, auto) + moreover have "th' \ runing (t@s)" + using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . + ultimately show False by simp + qed + -- {* Finally, it can be shown that the @{term cntP} and @{term cntV} + value for @{term th'} are still in balance, so @{term th'} + is still hand-emptied after the execution of event @{term e}: *} + ultimately show ?thesis using Cons(5) by metis + qed +qed (auto simp:eq_pv) -lemma count_eq_RAG_plus: - assumes "cntP s th = cntV s th" - shows "{th'. (Th th', Th th) \ (RAG s)^+} = {}" - using assms count_eq_dependants cs_dependants_def eq_RAG by auto +text {* -lemma count_eq_RAG_plus_Th: - assumes "cntP s th = cntV s th" - shows "{Th th' | th'. (Th th', Th th) \ (RAG s)^+} = {}" - using count_eq_RAG_plus[OF assms] by auto + By combining @{thm eq_pv_blocked} and @{thm eq_pv_persist}, it can + be derived easily that @{term th'} can not be running in the future: + +*} -lemma count_eq_tRAG_plus_Th: - assumes "cntP s th = cntV s th" - shows "{Th th' | th'. (Th th', Th th) \ (tRAG s)^+} = {}" - using count_eq_tRAG_plus[OF assms] by auto +lemma eq_pv_blocked_persist: + assumes neq_th': "th' \ th" + and eq_pv: "cntP s th' = cntV s th'" + shows "th' \ runing (t @ s)" + using assms + by (simp add: eq_pv_blocked eq_pv_persist) + +text {* -end + The following lemma shows the blocking thread @{term th'} must hold + some resource in the very beginning. + +*} -lemma tRAG_subtree_eq: - "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th' \ (subtree (RAG s) (Th th))}" - (is "?L = ?R") +lemma runing_cntP_cntV_inv: (* ddd *) + assumes is_runing: "th' \ runing (t @ s)" + and neq_th': "th' \ th" + shows "cntP s th' > cntV s th'" + using assms proof - - { fix n - assume h: "n \ ?L" - hence "n \ ?R" - by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) - } moreover { - fix n - assume "n \ ?R" - then obtain th' where h: "n = Th th'" "(Th th', Th th) \ (RAG s)^*" - by (auto simp:subtree_def) - from rtranclD[OF this(2)] - have "n \ ?L" - proof - assume "Th th' \ Th th \ (Th th', Th th) \ (RAG s)\<^sup>+" - with h have "n \ {Th th' | th'. (Th th', Th th) \ (RAG s)^+}" by auto - thus ?thesis using subtree_def tRAG_trancl_eq by fastforce - qed (insert h, auto simp:subtree_def) - } ultimately show ?thesis by auto -qed - -lemma threads_set_eq: - "the_thread ` (subtree (tRAG s) (Th th)) = - {th'. Th th' \ (subtree (RAG s) (Th th))}" (is "?L = ?R") - by (auto intro:rev_image_eqI simp:tRAG_subtree_eq) - -lemma cp_alt_def1: - "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))" -proof - - have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) = - ((the_preced s \ the_thread) ` subtree (tRAG s) (Th th))" - by auto - thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto) -qed - -lemma cp_gen_def_cond: - assumes "x = Th th" - shows "cp s th = cp_gen s (Th th)" -by (unfold cp_alt_def1 cp_gen_def, simp) - -lemma cp_gen_over_set: - assumes "\ x \ A. \ th. x = Th th" - shows "cp_gen s ` A = (cp s \ the_thread) ` A" -proof(rule f_image_eq) - fix a - assume "a \ A" - from assms[rule_format, OF this] - obtain th where eq_a: "a = Th th" by auto - show "cp_gen s a = (cp s \ the_thread) a" - by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp) + -- {* First, it can be shown that the number of @{term P} and + @{term V} operations can not be equal for thred @{term th'} *} + have "cntP s th' \ cntV s th'" + proof + -- {* The proof goes by contradiction, suppose otherwise: *} + assume otherwise: "cntP s th' = cntV s th'" + -- {* By applying @{thm eq_pv_blocked_persist} to this: *} + from eq_pv_blocked_persist[OF neq_th' otherwise] + -- {* we have that @{term th'} can not be running at moment @{term "t@s"}: *} + have "th' \ runing (t@s)" . + -- {* This is obvious in contradiction with assumption @{thm is_runing} *} + thus False using is_runing by simp + qed + -- {* However, the number of @{term V} is always less or equal to @{term P}: *} + moreover have "cntV s th' \ cntP s th'" using vat_s.cnp_cnv_cncs by auto + -- {* Thesis is finally derived by combining the these two results: *} + ultimately show ?thesis by auto qed -context valid_trace -begin +text {* -lemma RAG_threads: - assumes "(Th th) \ Field (RAG s)" - shows "th \ threads s" - using assms - by (metis Field_def UnE dm_RAG_threads range_in vt) + The following lemmas shows the blocking thread @{text th'} must be + live at the very beginning, i.e. the moment (or state) @{term s}. + The proof is a simple combination of the results above: + +*} -lemma subtree_tRAG_thread: - assumes "th \ threads s" - shows "subtree (tRAG s) (Th th) \ Th ` threads s" (is "?L \ ?R") -proof - - have "?L = {Th th' |th'. Th th' \ subtree (RAG s) (Th th)}" - by (unfold tRAG_subtree_eq, simp) - also have "... \ ?R" - proof - fix x - assume "x \ {Th th' |th'. Th th' \ subtree (RAG s) (Th th)}" - then obtain th' where h: "x = Th th'" "Th th' \ subtree (RAG s) (Th th)" by auto - from this(2) - show "x \ ?R" - proof(cases rule:subtreeE) - case 1 - thus ?thesis by (simp add: assms h(1)) - next - case 2 - thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) - qed +lemma runing_threads_inv: + assumes runing': "th' \ runing (t@s)" + and neq_th': "th' \ th" + shows "th' \ threads s" +proof(rule ccontr) -- {* Proof by contradiction: *} + assume otherwise: "th' \ threads s" + have "th' \ runing (t @ s)" + proof - + from vat_s.cnp_cnv_eq[OF otherwise] + have "cntP s th' = cntV s th'" . + from eq_pv_blocked_persist[OF neq_th' this] + show ?thesis . qed - finally show ?thesis . + with runing' show False by simp qed -lemma readys_root: - assumes "th \ readys s" - shows "root (RAG s) (Th th)" -proof - - { fix x - assume "x \ ancestors (RAG s) (Th th)" - hence h: "(Th th, x) \ (RAG s)^+" by (auto simp:ancestors_def) - from tranclD[OF this] - obtain z where "(Th th, z) \ RAG s" by auto - with assms(1) have False - apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def) - by (fold wq_def, blast) - } thus ?thesis by (unfold root_def, auto) -qed +text {* + + The following lemma summarises the above lemmas to give an overall + characterisationof the blocking thread @{text "th'"}: + +*} -lemma readys_in_no_subtree: - assumes "th \ readys s" - and "th' \ th" - shows "Th th \ subtree (RAG s) (Th th')" -proof - assume "Th th \ subtree (RAG s) (Th th')" - thus False - proof(cases rule:subtreeE) - case 1 - with assms show ?thesis by auto - next - case 2 - with readys_root[OF assms(1)] - show ?thesis by (auto simp:root_def) - qed -qed - -lemma not_in_thread_isolated: - assumes "th \ threads s" - shows "(Th th) \ Field (RAG s)" -proof - assume "(Th th) \ Field (RAG s)" - with dm_RAG_threads and range_in assms - show False by (unfold Field_def, blast) -qed - -lemma wf_RAG: "wf (RAG s)" -proof(rule finite_acyclic_wf) - from finite_RAG show "finite (RAG s)" . +lemma runing_inversion: (* ddd, one of the main lemmas to present *) + assumes runing': "th' \ runing (t@s)" + and neq_th: "th' \ th" + shows "th' \ threads s" + and "\detached s th'" + and "cp (t@s) th' = preced th s" +proof - + from runing_threads_inv[OF assms] + show "th' \ threads s" . next - from acyclic_RAG show "acyclic (RAG s)" . + from runing_cntP_cntV_inv[OF runing' neq_th] + show "\detached s th'" using vat_s.detached_eq by simp +next + from runing_preced_inversion[OF runing'] + show "cp (t@s) th' = preced th s" . qed -lemma sgv_wRAG: "single_valued (wRAG s)" - using waiting_unique - by (unfold single_valued_def wRAG_def, auto) + +section {* The existence of `blocking thread` *} + +text {* -lemma sgv_hRAG: "single_valued (hRAG s)" - using holding_unique - by (unfold single_valued_def hRAG_def, auto) + Suppose @{term th} is not running, it is first shown that there is a + path in RAG leading from node @{term th} to another thread @{text + "th'"} in the @{term readys}-set (So @{text "th'"} is an ancestor of + @{term th}}). + + Now, since @{term readys}-set is non-empty, there must be one in it + which holds the highest @{term cp}-value, which, by definition, is + the @{term runing}-thread. However, we are going to show more: this + running thread is exactly @{term "th'"}. + +*} -lemma sgv_tRAG: "single_valued (tRAG s)" - by (unfold tRAG_def, rule single_valued_relcomp, - insert sgv_wRAG sgv_hRAG, auto) - -lemma acyclic_tRAG: "acyclic (tRAG s)" -proof(unfold tRAG_def, rule acyclic_compose) - show "acyclic (RAG s)" using acyclic_RAG . -next - show "wRAG s \ RAG s" unfolding RAG_split by auto -next - show "hRAG s \ RAG s" unfolding RAG_split by auto +lemma th_blockedE: (* ddd, the other main lemma to be presented: *) + assumes "th \ runing (t@s)" + obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" + "th' \ runing (t@s)" +proof - + -- {* According to @{thm vat_t.th_chain_to_ready}, either + @{term "th"} is in @{term "readys"} or there is path leading from it to + one thread in @{term "readys"}. *} + have "th \ readys (t @ s) \ (\th'. th' \ readys (t @ s) \ (Th th, Th th') \ (RAG (t @ s))\<^sup>+)" + using th_kept vat_t.th_chain_to_ready by auto + -- {* However, @{term th} can not be in @{term readys}, because otherwise, since + @{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *} + moreover have "th \ readys (t@s)" + using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto + -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in + term @{term readys}: *} + ultimately obtain th' where th'_in: "th' \ readys (t@s)" + and dp: "(Th th, Th th') \ (RAG (t @ s))\<^sup>+" by auto + -- {* We are going to show that this @{term th'} is running. *} + have "th' \ runing (t@s)" + proof - + -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *} + have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R") + proof - + have "?L = Max ((the_preced (t @ s) \ the_thread) ` subtree (tRAG (t @ s)) (Th th'))" + by (unfold cp_alt_def1, simp) + also have "... = (the_preced (t @ s) \ the_thread) (Th th)" + proof(rule image_Max_subset) + show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads) + next + show "subtree (tRAG (t @ s)) (Th th') \ Th ` threads (t @ s)" + by (metis Range.intros dp trancl_range vat_t.range_in vat_t.subtree_tRAG_thread) + next + show "Th th \ subtree (tRAG (t @ s)) (Th th')" using dp + by (unfold tRAG_subtree_eq, auto simp:subtree_def) + next + show "Max ((the_preced (t @ s) \ the_thread) ` Th ` threads (t @ s)) = + (the_preced (t @ s) \ the_thread) (Th th)" (is "Max ?L = _") + proof - + have "?L = the_preced (t @ s) ` threads (t @ s)" + by (unfold image_comp, rule image_cong, auto) + thus ?thesis using max_preced the_preced_def by auto + qed + qed + also have "... = ?R" + using th_cp_max th_cp_preced th_kept + the_preced_def vat_t.max_cp_readys_threads by auto + finally show ?thesis . + qed + -- {* Now, since @{term th'} holds the highest @{term cp} + and we have already show it is in @{term readys}, + it is @{term runing} by definition. *} + with `th' \ readys (t@s)` show ?thesis by (simp add: runing_def) + qed + -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *} + moreover have "Th th' \ ancestors (RAG (t @ s)) (Th th)" + using `(Th th, Th th') \ (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) + ultimately show ?thesis using that by metis qed -lemma sgv_RAG: "single_valued (RAG s)" - using unique_RAG by (auto simp:single_valued_def) - -lemma rtree_RAG: "rtree (RAG s)" - using sgv_RAG acyclic_RAG - by (unfold rtree_def rtree_axioms_def sgv_def, auto) +text {* -end -context valid_trace -begin + Now it is easy to see there is always a thread to run by case + analysis on whether thread @{term th} is running: if the answer is + yes, the the running thread is obviously @{term th} itself; + otherwise, the running thread is the @{text th'} given by lemma + @{thm th_blockedE}. -(* ddd *) -lemma cp_gen_rec: - assumes "x = Th th" - shows "cp_gen s x = Max ({the_preced s th} \ (cp_gen s) ` children (tRAG s) x)" -proof(cases "children (tRAG s) x = {}") - case True - show ?thesis - by (unfold True cp_gen_def subtree_children, simp add:assms) +*} + +lemma live: "runing (t@s) \ {}" +proof(cases "th \ runing (t@s)") + case True thus ?thesis by auto next case False - hence [simp]: "children (tRAG s) x \ {}" by auto - note fsbttRAGs.finite_subtree[simp] - have [simp]: "finite (children (tRAG s) x)" - by (intro rev_finite_subset[OF fsbttRAGs.finite_subtree], - rule children_subtree) - { fix r x - have "subtree r x \ {}" by (auto simp:subtree_def) - } note this[simp] - have [simp]: "\x\children (tRAG s) x. subtree (tRAG s) x \ {}" - proof - - from False obtain q where "q \ children (tRAG s) x" by blast - moreover have "subtree (tRAG s) q \ {}" by simp - ultimately show ?thesis by blast - qed - have h: "Max ((the_preced s \ the_thread) ` - ({x} \ \(subtree (tRAG s) ` children (tRAG s) x))) = - Max ({the_preced s th} \ cp_gen s ` children (tRAG s) x)" - (is "?L = ?R") - proof - - let "Max (?f ` (?A \ \ (?g ` ?B)))" = ?L - let "Max (_ \ (?h ` ?B))" = ?R - let ?L1 = "?f ` \(?g ` ?B)" - have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)" - proof - - have "?L1 = ?f ` (\ x \ ?B.(?g x))" by simp - also have "... = (\ x \ ?B. ?f ` (?g x))" by auto - finally have "Max ?L1 = Max ..." by simp - also have "... = Max (Max ` (\x. ?f ` subtree (tRAG s) x) ` ?B)" - by (subst Max_UNION, simp+) - also have "... = Max (cp_gen s ` children (tRAG s) x)" - by (unfold image_comp cp_gen_alt_def, simp) - finally show ?thesis . - qed - show ?thesis - proof - - have "?L = Max (?f ` ?A \ ?L1)" by simp - also have "... = max (the_preced s (the_thread x)) (Max ?L1)" - by (subst Max_Un, simp+) - also have "... = max (?f x) (Max (?h ` ?B))" - by (unfold eq_Max_L1, simp) - also have "... =?R" - by (rule max_Max_eq, (simp)+, unfold assms, simp) - finally show ?thesis . - qed - qed thus ?thesis - by (fold h subtree_children, unfold cp_gen_def, simp) + thus ?thesis using th_blockedE by auto qed -lemma cp_rec: - "cp s th = Max ({the_preced s th} \ - (cp s o the_thread) ` children (tRAG s) (Th th))" -proof - - have "Th th = Th th" by simp - note h = cp_gen_def_cond[OF this] cp_gen_rec[OF this] - show ?thesis - proof - - have "cp_gen s ` children (tRAG s) (Th th) = - (cp s \ the_thread) ` children (tRAG s) (Th th)" - proof(rule cp_gen_over_set) - show " \x\children (tRAG s) (Th th). \th. x = Th th" - by (unfold tRAG_alt_def, auto simp:children_def) - qed - thus ?thesis by (subst (1) h(1), unfold h(2), simp) - qed -qed end - end diff -r 2056d9f481e2 -r ed938e2246b9 log --- a/log Thu Jan 28 16:36:46 2016 +0800 +++ b/log Thu Jan 28 21:14:17 2016 +0800 @@ -1,5 +1,22 @@ +修改集: 89:2056d9f481e2 +标签: tip +用户: zhangx +日期: Thu Jan 28 16:36:46 2016 +0800 +摘要: Slightly modified ExtGG.thy and PrioG.thy. + +修改集: 88:83dd5345d5d0 +父亲: 83:d239aa953315 +父亲: 87:33cb65e00ac0 +用户: zhangx +日期: Thu Jan 28 16:33:49 2016 +0800 +摘要: Merged back ExtGG.thy and PrioG.thy. + +修改集: 87:33cb65e00ac0 +用户: zhangx +日期: Thu Jan 28 15:36:48 2016 +0800 +摘要: Tracking ExtGG.thy etc., so that a update to 83 is possible. + 修改集: 86:2106021bae53 -标签: tip 用户: zhangx 日期: Thu Jan 28 07:46:05 2016 +0800 摘要: Added PrioG.thy again