# HG changeset patch # User Christian Urban # Date 1466153185 -3600 # Node ID 0f124691c1919175ca085f439787830256a93f64 # Parent e3cf792db636213a4feeb652dbb14e12a8bf2125 updated diff -r e3cf792db636 -r 0f124691c191 Attic/ExtGG.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Attic/ExtGG.thy Fri Jun 17 09:46:25 2016 +0100 @@ -0,0 +1,702 @@ +section {* + This file contains lemmas used to guide the recalculation of current precedence + after every system call (or system operation) +*} +theory Implementation +imports PIPBasics +begin + +text {* (* ddd *) + One beauty of our modelling is that we follow the definitional extension tradition of HOL. + The benefit of such a concise and miniature model is that large number of intuitively + obvious facts are derived as lemmas, rather than asserted as axioms. +*} + +text {* + However, the lemmas in the forthcoming several locales are no longer + obvious. These lemmas show how the current precedences should be recalculated + after every execution step (in our model, every step is represented by an event, + which in turn, represents a system call, or operation). Each operation is + treated in a separate locale. + + The complication of current precedence recalculation comes + because the changing of RAG needs to be taken into account, + in addition to the changing of precedence. + + The reason RAG changing affects current precedence is that, + according to the definition, current precedence + of a thread is the maximum of the precedences of every threads in its subtree, + where the notion of sub-tree in RAG is defined in RTree.thy. + + Therefore, for each operation, lemmas about the change of precedences + and RAG are derived first, on which lemmas about current precedence + recalculation are based on. +*} + +section {* The @{term Set} operation *} + +context valid_trace_set +begin + +text {* (* ddd *) + The following two lemmas confirm that @{text "Set"}-operation + only changes the precedence of the initiating thread (or actor) + of the operation (or event). +*} + + +lemma eq_preced: + assumes "th' \ th" + shows "preced th' (e#s) = preced th' s" +proof - + from assms show ?thesis + by (unfold is_set, auto simp:preced_def) +qed + +lemma eq_the_preced: + assumes "th' \ th" + shows "the_preced (e#s) th' = the_preced s th'" + using assms + by (unfold the_preced_def, intro eq_preced, simp) + + +text {* (* ddd *) + Th following lemma @{text "eq_cp_pre"} says that the priority change of @{text "th"} + only affects those threads, which as @{text "Th th"} in their sub-trees. + + The proof of this lemma is simplified by using the alternative definition + of @{text "cp"}. +*} + +lemma eq_cp_pre: + assumes nd: "Th th \ subtree (RAG s) (Th th')" + shows "cp (e#s) th' = cp s th'" +proof - + -- {* After unfolding using the alternative definition, elements + affecting the @{term "cp"}-value of threads become explicit. + We only need to prove the following: *} + have "Max (the_preced (e#s) ` {th'a. Th th'a \ subtree (RAG (e#s)) (Th th')}) = + Max (the_preced s ` {th'a. Th th'a \ subtree (RAG s) (Th th')})" + (is "Max (?f ` ?S1) = Max (?g ` ?S2)") + proof - + -- {* The base sets are equal. *} + have "?S1 = ?S2" using RAG_unchanged by simp + -- {* The function values on the base set are equal as well. *} + moreover have "\ e \ ?S2. ?f e = ?g e" + proof + fix th1 + assume "th1 \ ?S2" + with nd have "th1 \ th" by (auto) + from eq_the_preced[OF this] + show "the_preced (e#s) th1 = the_preced s th1" . + qed + -- {* Therefore, the image of the functions are equal. *} + ultimately have "(?f ` ?S1) = (?g ` ?S2)" by (auto intro!:f_image_eq) + thus ?thesis by simp + qed + thus ?thesis by (simp add:cp_alt_def) +qed + +text {* + The following lemma shows that @{term "th"} is not in the + sub-tree of any other thread. +*} +lemma th_in_no_subtree: + assumes "th' \ th" + shows "Th th \ subtree (RAG s) (Th th')" +proof - + from readys_in_no_subtree[OF th_ready_s assms(1)] + show ?thesis by blast +qed + +text {* + By combining @{thm "eq_cp_pre"} and @{thm "th_in_no_subtree"}, + it is obvious that the change of priority only affects the @{text "cp"}-value + of the initiating thread @{text "th"}. +*} +lemma eq_cp: + assumes "th' \ th" + shows "cp (e#s) th' = cp s th'" + by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]]) + +end + +section {* The @{term V} operation *} + +text {* + The following @{text "step_v_cps"} is the locale for @{text "V"}-operation. +*} + + +context valid_trace_v +begin + +lemma ancestors_th: "ancestors (RAG s) (Th th) = {}" +proof - + from readys_root[OF th_ready_s] + show ?thesis + by (unfold root_def, simp) +qed + +lemma edge_of_th: + "(Cs cs, Th th) \ RAG s" +proof - + from holding_th_cs_s + show ?thesis + by (unfold s_RAG_def holding_eq, auto) +qed + +lemma ancestors_cs: + "ancestors (RAG s) (Cs cs) = {Th th}" +proof - + have "ancestors (RAG s) (Cs cs) = ancestors (RAG s) (Th th) \ {Th th}" + by (rule rtree_RAG.ancestors_accum[OF edge_of_th]) + from this[unfolded ancestors_th] show ?thesis by simp +qed + +end + +text {* + The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, + which represents the case when there is another thread @{text "th'"} + to take over the critical resource released by the initiating thread @{text "th"}. +*} + +context valid_trace_v_n +begin + +lemma sub_RAGs': + "{(Cs cs, Th th), (Th taker, Cs cs)} \ RAG s" + using next_th_RAG[OF next_th_taker] . + +lemma ancestors_th': + "ancestors (RAG s) (Th taker) = {Th th, Cs cs}" +proof - + have "ancestors (RAG s) (Th taker) = ancestors (RAG s) (Cs cs) \ {Cs cs}" + proof(rule rtree_RAG.ancestors_accum) + from sub_RAGs' show "(Th taker, Cs cs) \ RAG s" by auto + qed + thus ?thesis using ancestors_th ancestors_cs by auto +qed + +lemma RAG_s: + "RAG (e#s) = (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) \ + {(Cs cs, Th taker)}" + by (unfold RAG_es waiting_set_eq holding_set_eq, auto) + +lemma subtree_kept: (* ddd *) + assumes "th1 \ {th, taker}" + shows "subtree (RAG (e#s)) (Th th1) = + subtree (RAG s) (Th th1)" (is "_ = ?R") +proof - + let ?RAG' = "(RAG s - {(Cs cs, Th th), (Th taker, Cs cs)})" + let ?RAG'' = "?RAG' \ {(Cs cs, Th taker)}" + have "subtree ?RAG' (Th th1) = ?R" + proof(rule subset_del_subtree_outside) + show "Range {(Cs cs, Th th), (Th taker, Cs cs)} \ subtree (RAG s) (Th th1) = {}" + proof - + have "(Th th) \ subtree (RAG s) (Th th1)" + proof(rule subtree_refute) + show "Th th1 \ ancestors (RAG s) (Th th)" + by (unfold ancestors_th, simp) + next + from assms show "Th th1 \ Th th" by simp + qed + moreover have "(Cs cs) \ subtree (RAG s) (Th th1)" + proof(rule subtree_refute) + show "Th th1 \ ancestors (RAG s) (Cs cs)" + by (unfold ancestors_cs, insert assms, auto) + qed simp + ultimately have "{Th th, Cs cs} \ subtree (RAG s) (Th th1) = {}" by auto + thus ?thesis by simp + qed + qed + moreover have "subtree ?RAG'' (Th th1) = subtree ?RAG' (Th th1)" + proof(rule subtree_insert_next) + show "Th taker \ subtree (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th th1)" + proof(rule subtree_refute) + show "Th th1 \ ancestors (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th taker)" + (is "_ \ ?R") + proof - + have "?R \ ancestors (RAG s) (Th taker)" by (rule ancestors_mono, auto) + moreover have "Th th1 \ ..." using ancestors_th' assms by simp + ultimately show ?thesis by auto + qed + next + from assms show "Th th1 \ Th taker" by simp + qed + qed + ultimately show ?thesis by (unfold RAG_s, simp) +qed + +lemma cp_kept: + assumes "th1 \ {th, taker}" + shows "cp (e#s) th1 = cp s th1" + by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp) + +end + + +context valid_trace_v_e +begin + +find_theorems RAG s e + +lemma RAG_s: "RAG (e#s) = RAG s - {(Cs cs, Th th)}" + by (unfold RAG_es waiting_set_eq holding_set_eq, simp) + +lemma subtree_kept: + assumes "th1 \ th" + shows "subtree (RAG (e#s)) (Th th1) = subtree (RAG s) (Th th1)" +proof(unfold RAG_s, rule subset_del_subtree_outside) + show "Range {(Cs cs, Th th)} \ subtree (RAG s) (Th th1) = {}" + proof - + have "(Th th) \ subtree (RAG s) (Th th1)" + proof(rule subtree_refute) + show "Th th1 \ ancestors (RAG s) (Th th)" + by (unfold ancestors_th, simp) + next + from assms show "Th th1 \ Th th" by simp + qed + thus ?thesis by auto + qed +qed + +lemma cp_kept_1: + assumes "th1 \ th" + shows "cp (e#s) th1 = cp s th1" + by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp) + +lemma subtree_cs: "subtree (RAG s) (Cs cs) = {Cs cs}" +proof - + { fix n + have "(Cs cs) \ ancestors (RAG s) n" + proof + assume "Cs cs \ ancestors (RAG s) n" + hence "(n, Cs cs) \ (RAG s)^+" by (auto simp:ancestors_def) + from tranclE[OF this] obtain nn where h: "(nn, Cs cs) \ RAG s" by auto + then obtain th' where "nn = Th th'" + by (unfold s_RAG_def, auto) + from h[unfolded this] have "(Th th', Cs cs) \ RAG s" . + from this[unfolded s_RAG_def] + have "waiting (wq s) th' cs" by auto + from this[unfolded cs_waiting_def] + have "1 < length (wq s cs)" + by (cases "wq s cs", auto) + from holding_next_thI[OF holding_th_cs_s this] + obtain th' where "next_th s th cs th'" by auto + thus False using no_taker by blast + qed + } note h = this + { fix n + assume "n \ subtree (RAG s) (Cs cs)" + hence "n = (Cs cs)" + by (elim subtreeE, insert h, auto) + } moreover have "(Cs cs) \ subtree (RAG s) (Cs cs)" + by (auto simp:subtree_def) + ultimately show ?thesis by auto +qed + +lemma subtree_th: + "subtree (RAG (e#s)) (Th th) = subtree (RAG s) (Th th) - {Cs cs}" +proof(unfold RAG_s, fold subtree_cs, rule rtree_RAG.subtree_del_inside) + from edge_of_th + show "(Cs cs, Th th) \ edges_in (RAG s) (Th th)" + by (unfold edges_in_def, auto simp:subtree_def) +qed + +lemma cp_kept_2: + shows "cp (e#s) th = cp s th" + by (unfold cp_alt_def subtree_th the_preced_es, auto) + +lemma eq_cp: + shows "cp (e#s) th' = cp s th'" + using cp_kept_1 cp_kept_2 + by (cases "th' = th", auto) + +end + + +section {* The @{term P} operation *} + +context valid_trace_p +begin + +lemma root_th: "root (RAG s) (Th th)" + by (simp add: ready_th_s readys_root) + +lemma in_no_others_subtree: + assumes "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 root_th show ?thesis by (auto simp:root_def) + qed +qed + +lemma preced_kept: "the_preced (e#s) = the_preced s" +proof + fix th' + show "the_preced (e # s) th' = the_preced s th'" + by (unfold the_preced_def is_p preced_def, simp) +qed + +end + + +context valid_trace_p_h +begin + +lemma subtree_kept: + assumes "th' \ th" + shows "subtree (RAG (e#s)) (Th th') = subtree (RAG s) (Th th')" +proof(unfold RAG_es, rule subtree_insert_next) + from in_no_others_subtree[OF assms] + show "Th th \ subtree (RAG s) (Th th')" . +qed + +lemma cp_kept: + assumes "th' \ th" + shows "cp (e#s) th' = cp s th'" +proof - + have "(the_preced (e#s) ` {th'a. Th th'a \ subtree (RAG (e#s)) (Th th')}) = + (the_preced s ` {th'a. Th th'a \ subtree (RAG s) (Th th')})" + by (unfold preced_kept subtree_kept[OF assms], simp) + thus ?thesis by (unfold cp_alt_def, simp) +qed + +end + +context valid_trace_p_w +begin + +lemma cs_held: "(Cs cs, Th holder) \ RAG s" + using holding_s_holder + by (unfold s_RAG_def, fold holding_eq, auto) + +lemma tRAG_s: + "tRAG (e#s) = tRAG s \ {(Th th, Th holder)}" + using local.RAG_tRAG_transfer[OF RAG_es cs_held] . + +lemma cp_kept: + assumes "Th th'' \ ancestors (tRAG (e#s)) (Th th)" + shows "cp (e#s) th'' = cp s th''" +proof - + have h: "subtree (tRAG (e#s)) (Th th'') = subtree (tRAG s) (Th th'')" + proof - + have "Th holder \ subtree (tRAG s) (Th th'')" + proof + assume "Th holder \ subtree (tRAG s) (Th th'')" + thus False + proof(rule subtreeE) + assume "Th holder = Th th''" + from assms[unfolded tRAG_s ancestors_def, folded this] + show ?thesis by auto + next + assume "Th th'' \ ancestors (tRAG s) (Th holder)" + moreover have "... \ ancestors (tRAG (e#s)) (Th holder)" + proof(rule ancestors_mono) + show "tRAG s \ tRAG (e#s)" by (unfold tRAG_s, auto) + qed + ultimately have "Th th'' \ ancestors (tRAG (e#s)) (Th holder)" by auto + moreover have "Th holder \ ancestors (tRAG (e#s)) (Th th)" + by (unfold tRAG_s, auto simp:ancestors_def) + ultimately have "Th th'' \ ancestors (tRAG (e#s)) (Th th)" + by (auto simp:ancestors_def) + with assms show ?thesis by auto + qed + qed + from subtree_insert_next[OF this] + have "subtree (tRAG s \ {(Th th, Th holder)}) (Th th'') = subtree (tRAG s) (Th th'')" . + from this[folded tRAG_s] show ?thesis . + qed + show ?thesis by (unfold cp_alt_def1 h preced_kept, simp) +qed + +lemma cp_gen_update_stop: (* ddd *) + assumes "u \ ancestors (tRAG (e#s)) (Th th)" + and "cp_gen (e#s) u = cp_gen s u" + and "y \ ancestors (tRAG (e#s)) u" + shows "cp_gen (e#s) y = cp_gen s y" + using assms(3) +proof(induct rule:wf_induct[OF vat_es.fsbttRAGs.wf]) + case (1 x) + show ?case (is "?L = ?R") + proof - + from tRAG_ancestorsE[OF 1(2)] + obtain th2 where eq_x: "x = Th th2" by blast + from vat_es.cp_gen_rec[OF this] + have "?L = + Max ({the_preced (e#s) th2} \ cp_gen (e#s) ` RTree.children (tRAG (e#s)) x)" . + also have "... = + Max ({the_preced s th2} \ cp_gen s ` RTree.children (tRAG s) x)" + proof - + from preced_kept have "the_preced (e#s) th2 = the_preced s th2" by simp + moreover have "cp_gen (e#s) ` RTree.children (tRAG (e#s)) x = + cp_gen s ` RTree.children (tRAG s) x" + proof - + have "RTree.children (tRAG (e#s)) x = RTree.children (tRAG s) x" + proof(unfold tRAG_s, rule children_union_kept) + have start: "(Th th, Th holder) \ tRAG (e#s)" + by (unfold tRAG_s, auto) + note x_u = 1(2) + show "x \ Range {(Th th, Th holder)}" + proof + assume "x \ Range {(Th th, Th holder)}" + hence eq_x: "x = Th holder" using RangeE by auto + show False + proof(cases rule:vat_es.ancestors_headE[OF assms(1) start]) + case 1 + from x_u[folded this, unfolded eq_x] vat_es.acyclic_tRAG + show ?thesis by (auto simp:ancestors_def acyclic_def) + next + case 2 + with x_u[unfolded eq_x] + have "(Th holder, Th holder) \ (tRAG (e#s))^+" by (auto simp:ancestors_def) + with vat_es.acyclic_tRAG show ?thesis by (auto simp:acyclic_def) + qed + qed + qed + moreover have "cp_gen (e#s) ` RTree.children (tRAG (e#s)) x = + cp_gen s ` RTree.children (tRAG (e#s)) x" (is "?f ` ?A = ?g ` ?A") + proof(rule f_image_eq) + fix a + assume a_in: "a \ ?A" + from 1(2) + show "?f a = ?g a" + proof(cases rule:vat_es.rtree_s.ancestors_childrenE[case_names in_ch out_ch]) + case in_ch + show ?thesis + proof(cases "a = u") + case True + from assms(2)[folded this] show ?thesis . + next + case False + have a_not_in: "a \ ancestors (tRAG (e#s)) (Th th)" + proof + assume a_in': "a \ ancestors (tRAG (e#s)) (Th th)" + have "a = u" + proof(rule vat_es.rtree_s.ancestors_children_unique) + from a_in' a_in show "a \ ancestors (tRAG (e#s)) (Th th) \ + RTree.children (tRAG (e#s)) x" by auto + next + from assms(1) in_ch show "u \ ancestors (tRAG (e#s)) (Th th) \ + RTree.children (tRAG (e#s)) x" by auto + qed + with False show False by simp + qed + from a_in obtain th_a where eq_a: "a = Th th_a" + by (unfold RTree.children_def tRAG_alt_def, auto) + from cp_kept[OF a_not_in[unfolded eq_a]] + have "cp (e#s) th_a = cp s th_a" . + from this [unfolded cp_gen_def_cond[OF eq_a], folded eq_a] + show ?thesis . + qed + next + case (out_ch z) + hence h: "z \ ancestors (tRAG (e#s)) u" "z \ RTree.children (tRAG (e#s)) x" by auto + show ?thesis + proof(cases "a = z") + case True + from h(2) have zx_in: "(z, x) \ (tRAG (e#s))" by (auto simp:RTree.children_def) + from 1(1)[rule_format, OF this h(1)] + have eq_cp_gen: "cp_gen (e#s) z = cp_gen s z" . + with True show ?thesis by metis + next + case False + from a_in obtain th_a where eq_a: "a = Th th_a" + by (auto simp:RTree.children_def tRAG_alt_def) + have "a \ ancestors (tRAG (e#s)) (Th th)" + proof + assume a_in': "a \ ancestors (tRAG (e#s)) (Th th)" + have "a = z" + proof(rule vat_es.rtree_s.ancestors_children_unique) + from assms(1) h(1) have "z \ ancestors (tRAG (e#s)) (Th th)" + by (auto simp:ancestors_def) + with h(2) show " z \ ancestors (tRAG (e#s)) (Th th) \ + RTree.children (tRAG (e#s)) x" by auto + next + from a_in a_in' + show "a \ ancestors (tRAG (e#s)) (Th th) \ RTree.children (tRAG (e#s)) x" + by auto + qed + with False show False by auto + qed + from cp_kept[OF this[unfolded eq_a]] + have "cp (e#s) th_a = cp s th_a" . + from this[unfolded cp_gen_def_cond[OF eq_a], folded eq_a] + show ?thesis . + qed + qed + qed + ultimately show ?thesis by metis + qed + ultimately show ?thesis by simp + qed + also have "... = ?R" + by (fold cp_gen_rec[OF eq_x], simp) + finally show ?thesis . + qed +qed + +lemma cp_up: + assumes "(Th th') \ ancestors (tRAG (e#s)) (Th th)" + and "cp (e#s) th' = cp s th'" + and "(Th th'') \ ancestors (tRAG (e#s)) (Th th')" + shows "cp (e#s) th'' = cp s th''" +proof - + have "cp_gen (e#s) (Th th'') = cp_gen s (Th th'')" + proof(rule cp_gen_update_stop[OF assms(1) _ assms(3)]) + from assms(2) cp_gen_def_cond[OF refl[of "Th th'"]] + show "cp_gen (e#s) (Th th') = cp_gen s (Th th')" by metis + qed + with cp_gen_def_cond[OF refl[of "Th th''"]] + show ?thesis by metis +qed + +end + +section {* The @{term Create} operation *} + +context valid_trace_create +begin + +lemma tRAG_kept: "tRAG (e#s) = tRAG s" + by (unfold tRAG_alt_def RAG_unchanged, auto) + +lemma preced_kept: + assumes "th' \ th" + shows "the_preced (e#s) th' = the_preced s th'" + by (unfold the_preced_def preced_def is_create, insert assms, auto) + +lemma th_not_in: "Th th \ Field (tRAG s)" + by (meson not_in_thread_isolated subsetCE tRAG_Field th_not_live_s) + +lemma eq_cp: + assumes neq_th: "th' \ th" + shows "cp (e#s) th' = cp s th'" +proof - + have "(the_preced (e#s) \ the_thread) ` subtree (tRAG (e#s)) (Th th') = + (the_preced s \ the_thread) ` subtree (tRAG s) (Th th')" + proof(unfold tRAG_kept, rule f_image_eq) + fix a + assume a_in: "a \ subtree (tRAG s) (Th th')" + then obtain th_a where eq_a: "a = Th th_a" + proof(cases rule:subtreeE) + case 2 + from ancestors_Field[OF 2(2)] + and that show ?thesis by (unfold tRAG_alt_def, auto) + qed auto + have neq_th_a: "th_a \ th" + proof - + have "(Th th) \ subtree (tRAG s) (Th th')" + proof + assume "Th th \ subtree (tRAG s) (Th th')" + thus False + proof(cases rule:subtreeE) + case 2 + from ancestors_Field[OF this(2)] + and th_not_in[unfolded Field_def] + show ?thesis by auto + qed (insert assms, auto) + qed + with a_in[unfolded eq_a] show ?thesis by auto + qed + from preced_kept[OF this] + show "(the_preced (e#s) \ the_thread) a = (the_preced s \ the_thread) a" + by (unfold eq_a, simp) + qed + thus ?thesis by (unfold cp_alt_def1, simp) +qed + +lemma children_of_th: "RTree.children (tRAG (e#s)) (Th th) = {}" +proof - + { fix a + assume "a \ RTree.children (tRAG (e#s)) (Th th)" + hence "(a, Th th) \ tRAG (e#s)" by (auto simp:RTree.children_def) + with th_not_in have False + by (unfold Field_def tRAG_kept, auto) + } thus ?thesis by auto +qed + +lemma eq_cp_th: "cp (e#s) th = preced th (e#s)" + by (unfold vat_es.cp_rec children_of_th, simp add:the_preced_def) + +end + + +context valid_trace_exit +begin + +lemma preced_kept: + assumes "th' \ th" + shows "the_preced (e#s) th' = the_preced s th'" + using assms + by (unfold the_preced_def is_exit preced_def, simp) + +lemma tRAG_kept: "tRAG (e#s) = tRAG s" + by (unfold tRAG_alt_def RAG_unchanged, auto) + +lemma th_RAG: "Th th \ Field (RAG s)" +proof - + have "Th th \ Range (RAG s)" + proof + assume "Th th \ Range (RAG s)" + then obtain cs where "holding (wq s) th cs" + by (unfold Range_iff s_RAG_def, auto) + with holdents_th_s[unfolded holdents_def] + show False by (unfold holding_eq, auto) + qed + moreover have "Th th \ Domain (RAG s)" + proof + assume "Th th \ Domain (RAG s)" + then obtain cs where "waiting (wq s) th cs" + by (unfold Domain_iff s_RAG_def, auto) + with th_ready_s show False by (unfold readys_def waiting_eq, auto) + qed + ultimately show ?thesis by (auto simp:Field_def) +qed + +lemma th_tRAG: "(Th th) \ Field (tRAG s)" + using th_RAG tRAG_Field by auto + +lemma eq_cp: + assumes neq_th: "th' \ th" + shows "cp (e#s) th' = cp s th'" +proof - + have "(the_preced (e#s) \ the_thread) ` subtree (tRAG (e#s)) (Th th') = + (the_preced s \ the_thread) ` subtree (tRAG s) (Th th')" + proof(unfold tRAG_kept, rule f_image_eq) + fix a + assume a_in: "a \ subtree (tRAG s) (Th th')" + then obtain th_a where eq_a: "a = Th th_a" + proof(cases rule:subtreeE) + case 2 + from ancestors_Field[OF 2(2)] + and that show ?thesis by (unfold tRAG_alt_def, auto) + qed auto + have neq_th_a: "th_a \ th" + proof - + from readys_in_no_subtree[OF th_ready_s assms] + have "(Th th) \ subtree (RAG s) (Th th')" . + with tRAG_subtree_RAG[of s "Th th'"] + have "(Th th) \ subtree (tRAG s) (Th th')" by auto + with a_in[unfolded eq_a] show ?thesis by auto + qed + from preced_kept[OF this] + show "(the_preced (e#s) \ the_thread) a = (the_preced s \ the_thread) a" + by (unfold eq_a, simp) + qed + thus ?thesis by (unfold cp_alt_def1, simp) +qed + +end + +end + diff -r e3cf792db636 -r 0f124691c191 Attic/PrioG.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Attic/PrioG.thy Fri Jun 17 09:46:25 2016 +0100 @@ -0,0 +1,797 @@ +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, 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 - + 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 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. + + 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 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: *} + also have "... = ?R" + thm runing_preced_inversion + 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 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 + interpret vat_es: valid_trace_e "t@s" e using Cons(1,2) by (unfold_locales, auto) + 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_es.actor_inv + -- {* According to @{thm vat_es.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_es.actor_inv + 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 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 {* + 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.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) + 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 e3cf792db636 -r 0f124691c191 Correctness.thy --- a/Correctness.thy Tue Jun 14 15:06:16 2016 +0100 +++ b/Correctness.thy Fri Jun 17 09:46:25 2016 +0100 @@ -558,7 +558,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_def eq_dependants vat_t.eq_pv_dependants[OF eq_pv], simp) + by (simp add: detached_cp_preced eq_pv vat_t.detached_intro) -- {* Since @{term "th'"} is running, by @{thm running_preced_inversion}, its @{term cp}-value equals @{term "preced th s"}, which equals to @{term "?R"} by simplification: *} diff -r e3cf792db636 -r 0f124691c191 ExtGG.thy --- a/ExtGG.thy Tue Jun 14 15:06:16 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,702 +0,0 @@ -section {* - This file contains lemmas used to guide the recalculation of current precedence - after every system call (or system operation) -*} -theory Implementation -imports PIPBasics -begin - -text {* (* ddd *) - One beauty of our modelling is that we follow the definitional extension tradition of HOL. - The benefit of such a concise and miniature model is that large number of intuitively - obvious facts are derived as lemmas, rather than asserted as axioms. -*} - -text {* - However, the lemmas in the forthcoming several locales are no longer - obvious. These lemmas show how the current precedences should be recalculated - after every execution step (in our model, every step is represented by an event, - which in turn, represents a system call, or operation). Each operation is - treated in a separate locale. - - The complication of current precedence recalculation comes - because the changing of RAG needs to be taken into account, - in addition to the changing of precedence. - - The reason RAG changing affects current precedence is that, - according to the definition, current precedence - of a thread is the maximum of the precedences of every threads in its subtree, - where the notion of sub-tree in RAG is defined in RTree.thy. - - Therefore, for each operation, lemmas about the change of precedences - and RAG are derived first, on which lemmas about current precedence - recalculation are based on. -*} - -section {* The @{term Set} operation *} - -context valid_trace_set -begin - -text {* (* ddd *) - The following two lemmas confirm that @{text "Set"}-operation - only changes the precedence of the initiating thread (or actor) - of the operation (or event). -*} - - -lemma eq_preced: - assumes "th' \ th" - shows "preced th' (e#s) = preced th' s" -proof - - from assms show ?thesis - by (unfold is_set, auto simp:preced_def) -qed - -lemma eq_the_preced: - assumes "th' \ th" - shows "the_preced (e#s) th' = the_preced s th'" - using assms - by (unfold the_preced_def, intro eq_preced, simp) - - -text {* (* ddd *) - Th following lemma @{text "eq_cp_pre"} says that the priority change of @{text "th"} - only affects those threads, which as @{text "Th th"} in their sub-trees. - - The proof of this lemma is simplified by using the alternative definition - of @{text "cp"}. -*} - -lemma eq_cp_pre: - assumes nd: "Th th \ subtree (RAG s) (Th th')" - shows "cp (e#s) th' = cp s th'" -proof - - -- {* After unfolding using the alternative definition, elements - affecting the @{term "cp"}-value of threads become explicit. - We only need to prove the following: *} - have "Max (the_preced (e#s) ` {th'a. Th th'a \ subtree (RAG (e#s)) (Th th')}) = - Max (the_preced s ` {th'a. Th th'a \ subtree (RAG s) (Th th')})" - (is "Max (?f ` ?S1) = Max (?g ` ?S2)") - proof - - -- {* The base sets are equal. *} - have "?S1 = ?S2" using RAG_unchanged by simp - -- {* The function values on the base set are equal as well. *} - moreover have "\ e \ ?S2. ?f e = ?g e" - proof - fix th1 - assume "th1 \ ?S2" - with nd have "th1 \ th" by (auto) - from eq_the_preced[OF this] - show "the_preced (e#s) th1 = the_preced s th1" . - qed - -- {* Therefore, the image of the functions are equal. *} - ultimately have "(?f ` ?S1) = (?g ` ?S2)" by (auto intro!:f_image_eq) - thus ?thesis by simp - qed - thus ?thesis by (simp add:cp_alt_def) -qed - -text {* - The following lemma shows that @{term "th"} is not in the - sub-tree of any other thread. -*} -lemma th_in_no_subtree: - assumes "th' \ th" - shows "Th th \ subtree (RAG s) (Th th')" -proof - - from readys_in_no_subtree[OF th_ready_s assms(1)] - show ?thesis by blast -qed - -text {* - By combining @{thm "eq_cp_pre"} and @{thm "th_in_no_subtree"}, - it is obvious that the change of priority only affects the @{text "cp"}-value - of the initiating thread @{text "th"}. -*} -lemma eq_cp: - assumes "th' \ th" - shows "cp (e#s) th' = cp s th'" - by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]]) - -end - -section {* The @{term V} operation *} - -text {* - The following @{text "step_v_cps"} is the locale for @{text "V"}-operation. -*} - - -context valid_trace_v -begin - -lemma ancestors_th: "ancestors (RAG s) (Th th) = {}" -proof - - from readys_root[OF th_ready_s] - show ?thesis - by (unfold root_def, simp) -qed - -lemma edge_of_th: - "(Cs cs, Th th) \ RAG s" -proof - - from holding_th_cs_s - show ?thesis - by (unfold s_RAG_def holding_eq, auto) -qed - -lemma ancestors_cs: - "ancestors (RAG s) (Cs cs) = {Th th}" -proof - - have "ancestors (RAG s) (Cs cs) = ancestors (RAG s) (Th th) \ {Th th}" - by (rule rtree_RAG.ancestors_accum[OF edge_of_th]) - from this[unfolded ancestors_th] show ?thesis by simp -qed - -end - -text {* - The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, - which represents the case when there is another thread @{text "th'"} - to take over the critical resource released by the initiating thread @{text "th"}. -*} - -context valid_trace_v_n -begin - -lemma sub_RAGs': - "{(Cs cs, Th th), (Th taker, Cs cs)} \ RAG s" - using next_th_RAG[OF next_th_taker] . - -lemma ancestors_th': - "ancestors (RAG s) (Th taker) = {Th th, Cs cs}" -proof - - have "ancestors (RAG s) (Th taker) = ancestors (RAG s) (Cs cs) \ {Cs cs}" - proof(rule rtree_RAG.ancestors_accum) - from sub_RAGs' show "(Th taker, Cs cs) \ RAG s" by auto - qed - thus ?thesis using ancestors_th ancestors_cs by auto -qed - -lemma RAG_s: - "RAG (e#s) = (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) \ - {(Cs cs, Th taker)}" - by (unfold RAG_es waiting_set_eq holding_set_eq, auto) - -lemma subtree_kept: (* ddd *) - assumes "th1 \ {th, taker}" - shows "subtree (RAG (e#s)) (Th th1) = - subtree (RAG s) (Th th1)" (is "_ = ?R") -proof - - let ?RAG' = "(RAG s - {(Cs cs, Th th), (Th taker, Cs cs)})" - let ?RAG'' = "?RAG' \ {(Cs cs, Th taker)}" - have "subtree ?RAG' (Th th1) = ?R" - proof(rule subset_del_subtree_outside) - show "Range {(Cs cs, Th th), (Th taker, Cs cs)} \ subtree (RAG s) (Th th1) = {}" - proof - - have "(Th th) \ subtree (RAG s) (Th th1)" - proof(rule subtree_refute) - show "Th th1 \ ancestors (RAG s) (Th th)" - by (unfold ancestors_th, simp) - next - from assms show "Th th1 \ Th th" by simp - qed - moreover have "(Cs cs) \ subtree (RAG s) (Th th1)" - proof(rule subtree_refute) - show "Th th1 \ ancestors (RAG s) (Cs cs)" - by (unfold ancestors_cs, insert assms, auto) - qed simp - ultimately have "{Th th, Cs cs} \ subtree (RAG s) (Th th1) = {}" by auto - thus ?thesis by simp - qed - qed - moreover have "subtree ?RAG'' (Th th1) = subtree ?RAG' (Th th1)" - proof(rule subtree_insert_next) - show "Th taker \ subtree (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th th1)" - proof(rule subtree_refute) - show "Th th1 \ ancestors (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th taker)" - (is "_ \ ?R") - proof - - have "?R \ ancestors (RAG s) (Th taker)" by (rule ancestors_mono, auto) - moreover have "Th th1 \ ..." using ancestors_th' assms by simp - ultimately show ?thesis by auto - qed - next - from assms show "Th th1 \ Th taker" by simp - qed - qed - ultimately show ?thesis by (unfold RAG_s, simp) -qed - -lemma cp_kept: - assumes "th1 \ {th, taker}" - shows "cp (e#s) th1 = cp s th1" - by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp) - -end - - -context valid_trace_v_e -begin - -find_theorems RAG s e - -lemma RAG_s: "RAG (e#s) = RAG s - {(Cs cs, Th th)}" - by (unfold RAG_es waiting_set_eq holding_set_eq, simp) - -lemma subtree_kept: - assumes "th1 \ th" - shows "subtree (RAG (e#s)) (Th th1) = subtree (RAG s) (Th th1)" -proof(unfold RAG_s, rule subset_del_subtree_outside) - show "Range {(Cs cs, Th th)} \ subtree (RAG s) (Th th1) = {}" - proof - - have "(Th th) \ subtree (RAG s) (Th th1)" - proof(rule subtree_refute) - show "Th th1 \ ancestors (RAG s) (Th th)" - by (unfold ancestors_th, simp) - next - from assms show "Th th1 \ Th th" by simp - qed - thus ?thesis by auto - qed -qed - -lemma cp_kept_1: - assumes "th1 \ th" - shows "cp (e#s) th1 = cp s th1" - by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp) - -lemma subtree_cs: "subtree (RAG s) (Cs cs) = {Cs cs}" -proof - - { fix n - have "(Cs cs) \ ancestors (RAG s) n" - proof - assume "Cs cs \ ancestors (RAG s) n" - hence "(n, Cs cs) \ (RAG s)^+" by (auto simp:ancestors_def) - from tranclE[OF this] obtain nn where h: "(nn, Cs cs) \ RAG s" by auto - then obtain th' where "nn = Th th'" - by (unfold s_RAG_def, auto) - from h[unfolded this] have "(Th th', Cs cs) \ RAG s" . - from this[unfolded s_RAG_def] - have "waiting (wq s) th' cs" by auto - from this[unfolded cs_waiting_def] - have "1 < length (wq s cs)" - by (cases "wq s cs", auto) - from holding_next_thI[OF holding_th_cs_s this] - obtain th' where "next_th s th cs th'" by auto - thus False using no_taker by blast - qed - } note h = this - { fix n - assume "n \ subtree (RAG s) (Cs cs)" - hence "n = (Cs cs)" - by (elim subtreeE, insert h, auto) - } moreover have "(Cs cs) \ subtree (RAG s) (Cs cs)" - by (auto simp:subtree_def) - ultimately show ?thesis by auto -qed - -lemma subtree_th: - "subtree (RAG (e#s)) (Th th) = subtree (RAG s) (Th th) - {Cs cs}" -proof(unfold RAG_s, fold subtree_cs, rule rtree_RAG.subtree_del_inside) - from edge_of_th - show "(Cs cs, Th th) \ edges_in (RAG s) (Th th)" - by (unfold edges_in_def, auto simp:subtree_def) -qed - -lemma cp_kept_2: - shows "cp (e#s) th = cp s th" - by (unfold cp_alt_def subtree_th the_preced_es, auto) - -lemma eq_cp: - shows "cp (e#s) th' = cp s th'" - using cp_kept_1 cp_kept_2 - by (cases "th' = th", auto) - -end - - -section {* The @{term P} operation *} - -context valid_trace_p -begin - -lemma root_th: "root (RAG s) (Th th)" - by (simp add: ready_th_s readys_root) - -lemma in_no_others_subtree: - assumes "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 root_th show ?thesis by (auto simp:root_def) - qed -qed - -lemma preced_kept: "the_preced (e#s) = the_preced s" -proof - fix th' - show "the_preced (e # s) th' = the_preced s th'" - by (unfold the_preced_def is_p preced_def, simp) -qed - -end - - -context valid_trace_p_h -begin - -lemma subtree_kept: - assumes "th' \ th" - shows "subtree (RAG (e#s)) (Th th') = subtree (RAG s) (Th th')" -proof(unfold RAG_es, rule subtree_insert_next) - from in_no_others_subtree[OF assms] - show "Th th \ subtree (RAG s) (Th th')" . -qed - -lemma cp_kept: - assumes "th' \ th" - shows "cp (e#s) th' = cp s th'" -proof - - have "(the_preced (e#s) ` {th'a. Th th'a \ subtree (RAG (e#s)) (Th th')}) = - (the_preced s ` {th'a. Th th'a \ subtree (RAG s) (Th th')})" - by (unfold preced_kept subtree_kept[OF assms], simp) - thus ?thesis by (unfold cp_alt_def, simp) -qed - -end - -context valid_trace_p_w -begin - -lemma cs_held: "(Cs cs, Th holder) \ RAG s" - using holding_s_holder - by (unfold s_RAG_def, fold holding_eq, auto) - -lemma tRAG_s: - "tRAG (e#s) = tRAG s \ {(Th th, Th holder)}" - using local.RAG_tRAG_transfer[OF RAG_es cs_held] . - -lemma cp_kept: - assumes "Th th'' \ ancestors (tRAG (e#s)) (Th th)" - shows "cp (e#s) th'' = cp s th''" -proof - - have h: "subtree (tRAG (e#s)) (Th th'') = subtree (tRAG s) (Th th'')" - proof - - have "Th holder \ subtree (tRAG s) (Th th'')" - proof - assume "Th holder \ subtree (tRAG s) (Th th'')" - thus False - proof(rule subtreeE) - assume "Th holder = Th th''" - from assms[unfolded tRAG_s ancestors_def, folded this] - show ?thesis by auto - next - assume "Th th'' \ ancestors (tRAG s) (Th holder)" - moreover have "... \ ancestors (tRAG (e#s)) (Th holder)" - proof(rule ancestors_mono) - show "tRAG s \ tRAG (e#s)" by (unfold tRAG_s, auto) - qed - ultimately have "Th th'' \ ancestors (tRAG (e#s)) (Th holder)" by auto - moreover have "Th holder \ ancestors (tRAG (e#s)) (Th th)" - by (unfold tRAG_s, auto simp:ancestors_def) - ultimately have "Th th'' \ ancestors (tRAG (e#s)) (Th th)" - by (auto simp:ancestors_def) - with assms show ?thesis by auto - qed - qed - from subtree_insert_next[OF this] - have "subtree (tRAG s \ {(Th th, Th holder)}) (Th th'') = subtree (tRAG s) (Th th'')" . - from this[folded tRAG_s] show ?thesis . - qed - show ?thesis by (unfold cp_alt_def1 h preced_kept, simp) -qed - -lemma cp_gen_update_stop: (* ddd *) - assumes "u \ ancestors (tRAG (e#s)) (Th th)" - and "cp_gen (e#s) u = cp_gen s u" - and "y \ ancestors (tRAG (e#s)) u" - shows "cp_gen (e#s) y = cp_gen s y" - using assms(3) -proof(induct rule:wf_induct[OF vat_es.fsbttRAGs.wf]) - case (1 x) - show ?case (is "?L = ?R") - proof - - from tRAG_ancestorsE[OF 1(2)] - obtain th2 where eq_x: "x = Th th2" by blast - from vat_es.cp_gen_rec[OF this] - have "?L = - Max ({the_preced (e#s) th2} \ cp_gen (e#s) ` RTree.children (tRAG (e#s)) x)" . - also have "... = - Max ({the_preced s th2} \ cp_gen s ` RTree.children (tRAG s) x)" - proof - - from preced_kept have "the_preced (e#s) th2 = the_preced s th2" by simp - moreover have "cp_gen (e#s) ` RTree.children (tRAG (e#s)) x = - cp_gen s ` RTree.children (tRAG s) x" - proof - - have "RTree.children (tRAG (e#s)) x = RTree.children (tRAG s) x" - proof(unfold tRAG_s, rule children_union_kept) - have start: "(Th th, Th holder) \ tRAG (e#s)" - by (unfold tRAG_s, auto) - note x_u = 1(2) - show "x \ Range {(Th th, Th holder)}" - proof - assume "x \ Range {(Th th, Th holder)}" - hence eq_x: "x = Th holder" using RangeE by auto - show False - proof(cases rule:vat_es.ancestors_headE[OF assms(1) start]) - case 1 - from x_u[folded this, unfolded eq_x] vat_es.acyclic_tRAG - show ?thesis by (auto simp:ancestors_def acyclic_def) - next - case 2 - with x_u[unfolded eq_x] - have "(Th holder, Th holder) \ (tRAG (e#s))^+" by (auto simp:ancestors_def) - with vat_es.acyclic_tRAG show ?thesis by (auto simp:acyclic_def) - qed - qed - qed - moreover have "cp_gen (e#s) ` RTree.children (tRAG (e#s)) x = - cp_gen s ` RTree.children (tRAG (e#s)) x" (is "?f ` ?A = ?g ` ?A") - proof(rule f_image_eq) - fix a - assume a_in: "a \ ?A" - from 1(2) - show "?f a = ?g a" - proof(cases rule:vat_es.rtree_s.ancestors_childrenE[case_names in_ch out_ch]) - case in_ch - show ?thesis - proof(cases "a = u") - case True - from assms(2)[folded this] show ?thesis . - next - case False - have a_not_in: "a \ ancestors (tRAG (e#s)) (Th th)" - proof - assume a_in': "a \ ancestors (tRAG (e#s)) (Th th)" - have "a = u" - proof(rule vat_es.rtree_s.ancestors_children_unique) - from a_in' a_in show "a \ ancestors (tRAG (e#s)) (Th th) \ - RTree.children (tRAG (e#s)) x" by auto - next - from assms(1) in_ch show "u \ ancestors (tRAG (e#s)) (Th th) \ - RTree.children (tRAG (e#s)) x" by auto - qed - with False show False by simp - qed - from a_in obtain th_a where eq_a: "a = Th th_a" - by (unfold RTree.children_def tRAG_alt_def, auto) - from cp_kept[OF a_not_in[unfolded eq_a]] - have "cp (e#s) th_a = cp s th_a" . - from this [unfolded cp_gen_def_cond[OF eq_a], folded eq_a] - show ?thesis . - qed - next - case (out_ch z) - hence h: "z \ ancestors (tRAG (e#s)) u" "z \ RTree.children (tRAG (e#s)) x" by auto - show ?thesis - proof(cases "a = z") - case True - from h(2) have zx_in: "(z, x) \ (tRAG (e#s))" by (auto simp:RTree.children_def) - from 1(1)[rule_format, OF this h(1)] - have eq_cp_gen: "cp_gen (e#s) z = cp_gen s z" . - with True show ?thesis by metis - next - case False - from a_in obtain th_a where eq_a: "a = Th th_a" - by (auto simp:RTree.children_def tRAG_alt_def) - have "a \ ancestors (tRAG (e#s)) (Th th)" - proof - assume a_in': "a \ ancestors (tRAG (e#s)) (Th th)" - have "a = z" - proof(rule vat_es.rtree_s.ancestors_children_unique) - from assms(1) h(1) have "z \ ancestors (tRAG (e#s)) (Th th)" - by (auto simp:ancestors_def) - with h(2) show " z \ ancestors (tRAG (e#s)) (Th th) \ - RTree.children (tRAG (e#s)) x" by auto - next - from a_in a_in' - show "a \ ancestors (tRAG (e#s)) (Th th) \ RTree.children (tRAG (e#s)) x" - by auto - qed - with False show False by auto - qed - from cp_kept[OF this[unfolded eq_a]] - have "cp (e#s) th_a = cp s th_a" . - from this[unfolded cp_gen_def_cond[OF eq_a], folded eq_a] - show ?thesis . - qed - qed - qed - ultimately show ?thesis by metis - qed - ultimately show ?thesis by simp - qed - also have "... = ?R" - by (fold cp_gen_rec[OF eq_x], simp) - finally show ?thesis . - qed -qed - -lemma cp_up: - assumes "(Th th') \ ancestors (tRAG (e#s)) (Th th)" - and "cp (e#s) th' = cp s th'" - and "(Th th'') \ ancestors (tRAG (e#s)) (Th th')" - shows "cp (e#s) th'' = cp s th''" -proof - - have "cp_gen (e#s) (Th th'') = cp_gen s (Th th'')" - proof(rule cp_gen_update_stop[OF assms(1) _ assms(3)]) - from assms(2) cp_gen_def_cond[OF refl[of "Th th'"]] - show "cp_gen (e#s) (Th th') = cp_gen s (Th th')" by metis - qed - with cp_gen_def_cond[OF refl[of "Th th''"]] - show ?thesis by metis -qed - -end - -section {* The @{term Create} operation *} - -context valid_trace_create -begin - -lemma tRAG_kept: "tRAG (e#s) = tRAG s" - by (unfold tRAG_alt_def RAG_unchanged, auto) - -lemma preced_kept: - assumes "th' \ th" - shows "the_preced (e#s) th' = the_preced s th'" - by (unfold the_preced_def preced_def is_create, insert assms, auto) - -lemma th_not_in: "Th th \ Field (tRAG s)" - by (meson not_in_thread_isolated subsetCE tRAG_Field th_not_live_s) - -lemma eq_cp: - assumes neq_th: "th' \ th" - shows "cp (e#s) th' = cp s th'" -proof - - have "(the_preced (e#s) \ the_thread) ` subtree (tRAG (e#s)) (Th th') = - (the_preced s \ the_thread) ` subtree (tRAG s) (Th th')" - proof(unfold tRAG_kept, rule f_image_eq) - fix a - assume a_in: "a \ subtree (tRAG s) (Th th')" - then obtain th_a where eq_a: "a = Th th_a" - proof(cases rule:subtreeE) - case 2 - from ancestors_Field[OF 2(2)] - and that show ?thesis by (unfold tRAG_alt_def, auto) - qed auto - have neq_th_a: "th_a \ th" - proof - - have "(Th th) \ subtree (tRAG s) (Th th')" - proof - assume "Th th \ subtree (tRAG s) (Th th')" - thus False - proof(cases rule:subtreeE) - case 2 - from ancestors_Field[OF this(2)] - and th_not_in[unfolded Field_def] - show ?thesis by auto - qed (insert assms, auto) - qed - with a_in[unfolded eq_a] show ?thesis by auto - qed - from preced_kept[OF this] - show "(the_preced (e#s) \ the_thread) a = (the_preced s \ the_thread) a" - by (unfold eq_a, simp) - qed - thus ?thesis by (unfold cp_alt_def1, simp) -qed - -lemma children_of_th: "RTree.children (tRAG (e#s)) (Th th) = {}" -proof - - { fix a - assume "a \ RTree.children (tRAG (e#s)) (Th th)" - hence "(a, Th th) \ tRAG (e#s)" by (auto simp:RTree.children_def) - with th_not_in have False - by (unfold Field_def tRAG_kept, auto) - } thus ?thesis by auto -qed - -lemma eq_cp_th: "cp (e#s) th = preced th (e#s)" - by (unfold vat_es.cp_rec children_of_th, simp add:the_preced_def) - -end - - -context valid_trace_exit -begin - -lemma preced_kept: - assumes "th' \ th" - shows "the_preced (e#s) th' = the_preced s th'" - using assms - by (unfold the_preced_def is_exit preced_def, simp) - -lemma tRAG_kept: "tRAG (e#s) = tRAG s" - by (unfold tRAG_alt_def RAG_unchanged, auto) - -lemma th_RAG: "Th th \ Field (RAG s)" -proof - - have "Th th \ Range (RAG s)" - proof - assume "Th th \ Range (RAG s)" - then obtain cs where "holding (wq s) th cs" - by (unfold Range_iff s_RAG_def, auto) - with holdents_th_s[unfolded holdents_def] - show False by (unfold holding_eq, auto) - qed - moreover have "Th th \ Domain (RAG s)" - proof - assume "Th th \ Domain (RAG s)" - then obtain cs where "waiting (wq s) th cs" - by (unfold Domain_iff s_RAG_def, auto) - with th_ready_s show False by (unfold readys_def waiting_eq, auto) - qed - ultimately show ?thesis by (auto simp:Field_def) -qed - -lemma th_tRAG: "(Th th) \ Field (tRAG s)" - using th_RAG tRAG_Field by auto - -lemma eq_cp: - assumes neq_th: "th' \ th" - shows "cp (e#s) th' = cp s th'" -proof - - have "(the_preced (e#s) \ the_thread) ` subtree (tRAG (e#s)) (Th th') = - (the_preced s \ the_thread) ` subtree (tRAG s) (Th th')" - proof(unfold tRAG_kept, rule f_image_eq) - fix a - assume a_in: "a \ subtree (tRAG s) (Th th')" - then obtain th_a where eq_a: "a = Th th_a" - proof(cases rule:subtreeE) - case 2 - from ancestors_Field[OF 2(2)] - and that show ?thesis by (unfold tRAG_alt_def, auto) - qed auto - have neq_th_a: "th_a \ th" - proof - - from readys_in_no_subtree[OF th_ready_s assms] - have "(Th th) \ subtree (RAG s) (Th th')" . - with tRAG_subtree_RAG[of s "Th th'"] - have "(Th th) \ subtree (tRAG s) (Th th')" by auto - with a_in[unfolded eq_a] show ?thesis by auto - qed - from preced_kept[OF this] - show "(the_preced (e#s) \ the_thread) a = (the_preced s \ the_thread) a" - by (unfold eq_a, simp) - qed - thus ?thesis by (unfold cp_alt_def1, simp) -qed - -end - -end - diff -r e3cf792db636 -r 0f124691c191 Implementation.thy --- a/Implementation.thy Tue Jun 14 15:06:16 2016 +0100 +++ b/Implementation.thy Fri Jun 17 09:46:25 2016 +0100 @@ -154,7 +154,7 @@ proof - from holding_th_cs_s show ?thesis - by (unfold s_RAG_def holding_eq, auto) + by (unfold s_RAG_def s_holding_abv, auto) qed lemma ancestors_cs: @@ -187,7 +187,7 @@ lemma sub_RAGs': "{(Cs cs, Th th), (Th taker, Cs cs)} \ RAG s" using waiting_taker holding_th_cs_s - by (unfold s_RAG_def, fold waiting_eq holding_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv s_holding_abv, auto) lemma ancestors_th': "ancestors (RAG s) (Th taker) = {Th th, Cs cs}" @@ -297,7 +297,7 @@ by (auto simp:ancestors_def) from tranclD2[OF this] obtain th' where "waiting s th' cs" - by (auto simp:s_RAG_def waiting_eq) + by (auto simp:s_RAG_def s_waiting_abv) with no_waiter_before show ?thesis by simp qed simp @@ -390,7 +390,7 @@ lemma cs_held: "(Cs cs, Th holder) \ RAG s" using holding_s_holder - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) lemma tRAG_s: "tRAG (e#s) = tRAG s \ {(Th th, Th holder)}" @@ -662,7 +662,7 @@ assume "Th th \ Range (RAG s)" then obtain cs where "holding s th cs" by (simp add: holdents_RAG holdents_th_s) - then show False by (unfold holding_eq, auto) + then show False by (unfold s_holding_abv, auto) qed moreover have "Th th \ Domain (RAG s)" proof diff -r e3cf792db636 -r 0f124691c191 Journal/Paper.thy --- a/Journal/Paper.thy Tue Jun 14 15:06:16 2016 +0100 +++ b/Journal/Paper.thy Fri Jun 17 09:46:25 2016 +0100 @@ -33,18 +33,21 @@ vt ("valid'_state") and Prc ("'(_, _')") and holding_raw ("holds") and - holding ("Holds") and + holding ("holds") and waiting_raw ("waits") and - waiting ("Waits") and + waiting ("waits") and dependants_raw ("dependants") and - dependants ("Dependants") and + dependants ("dependants") and + RAG_raw ("RAG") and + RAG ("RAG") and Th ("T") and Cs ("C") and readys ("ready") and preced ("prec") and preceds ("precs") and cpreced ("cprec") and - cp ("cprec") and + wq_fun ("wq") and + cprec_fun ("cp") and holdents ("resources") and DUMMY ("\<^raw:\mbox{$\_\!\_$}>") and cntP ("c\<^bsub>P\<^esub>") and @@ -455,7 +458,7 @@ \noindent Using @{term "holding_raw"} and @{term waiting_raw}, we can introduce \emph{Resource Allocation Graphs} (RAG), which represent the dependencies between threads and resources. - We represent RAGs as relations using pairs of the form + We choose to represent RAGs as relations using pairs of the form \begin{isabelle}\ \ \ \ \ %%% @{term "(Th th, Cs cs)"} \hspace{5mm}{\rm and}\hspace{5mm} @@ -524,8 +527,6 @@ that the resource is locked. In this way we can always start at a thread waiting for a resource and ``chase'' outgoing arrows leading to a single root of a tree. - - The use of relations for representing RAGs allows us to conveniently define the notion of the \emph{dependants} of a thread using the transitive closure operation for relations, written ~@{term "trancl DUMMY"}. This gives @@ -545,14 +546,14 @@ there is a circle of dependencies in a RAG, then clearly we have a deadlock. Therefore when a thread requests a resource, we must ensure that the resulting RAG is not circular. In practice, the - programmer has to ensure this. - + programmer has to ensure this. Our model will assume that critical + reseources can only be requested provided no circularity can arise. Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a state @{text s}. It is defined as \begin{isabelle}\ \ \ \ \ %%% - @{thm cpreced_def2}\hfill\numbered{cpreced} + @{thm cpreced_def}\hfill\numbered{cpreced} \end{isabelle} \noindent @@ -568,13 +569,17 @@ lowered prematurely. We again introduce an abbreviation for current precedeces of a set of threads, written @{term "cprecs wq s ths"}. + \begin{isabelle}\ \ \ \ \ %%% + @{thm cpreceds_def} + \end{isabelle} + The next function, called @{term schs}, defines the behaviour of the scheduler. It will be defined by recursion on the state (a list of events); this function returns a \emph{schedule state}, which we represent as a record consisting of two functions: \begin{isabelle}\ \ \ \ \ %%% - @{text "\wq_fun, cprec_fun\"} + @{text "\wq, cp\"} \end{isabelle} \noindent diff -r e3cf792db636 -r 0f124691c191 PIPBasics.thy --- a/PIPBasics.thy Tue Jun 14 15:06:16 2016 +0100 +++ b/PIPBasics.thy Fri Jun 17 09:46:25 2016 +0100 @@ -1,5 +1,5 @@ theory PIPBasics -imports PIPDefs +imports PIPDefs RTree begin text {* (* ddd *) @@ -147,7 +147,7 @@ obtain th' where "th' \ set (wq s cs)" "th' = hd (wq s cs)" by (metis empty_iff hd_in_set list.set(1)) hence "holding s th' cs" - by (unfold s_holding_def, fold wq_def, auto) + unfolding s_holding_def by auto from that[OF this] show ?thesis . qed @@ -159,7 +159,7 @@ *} lemma children_RAG_alt_def: "children (RAG (s::state)) (Th th) = Cs ` {cs. holding s th cs}" - by (unfold s_RAG_def, auto simp:children_def holding_eq) + by (unfold s_RAG_def, auto simp:children_def s_holding_abv) text {* The following two lemmas relate @{term holdents} and @{term cntCS} @@ -279,8 +279,8 @@ lemma in_RAG_E: assumes "(n1, n2) \ RAG (s::state)" obtains (waiting) th cs where "n1 = Th th" "n2 = Cs cs" "waiting s th cs" - | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs" - using assms[unfolded s_RAG_def, folded waiting_eq holding_eq] + | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs" + using assms[unfolded s_RAG_def, folded s_waiting_abv s_holding_abv] by auto text {* @@ -584,8 +584,8 @@ thus ?thesis by simp qed thus ?thesis - by (metis (no_types, lifting) cp_eq cpreced_def eq_dependants - f_image_eq the_preced_def) + by (metis (no_types, lifting) cp_eq cpreced_def2 f_image_eq + s_dependants_abv the_preced_def) qed text {* @@ -625,7 +625,7 @@ from h1 have "cs' = cs" by simp from assms(2) cs_in[unfolded this] have "holding s th'' cs" "holding s th2 cs" - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) from held_unique[OF this] show ?thesis by simp qed @@ -990,9 +990,9 @@ obtain rest where eq_wq: "wq s cs = th#rest" by blast with otherwise have "holding s th cs" - by (unfold s_holding_def, fold wq_def, simp) + unfolding s_holding_def by auto hence cs_th_RAG: "(Cs cs, Th th) \ RAG s" - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) from pip_e[unfolded is_p] show False proof(cases) @@ -1033,8 +1033,8 @@ proof(cases) case (thread_V) from this(2) show ?thesis - by (unfold rest_def s_holding_def, fold wq_def, - metis empty_iff list.collapse list.set(1)) + unfolding s_holding_def + by (metis empty_iff empty_set hd_Cons_tl rest_def) qed qed @@ -1168,8 +1168,9 @@ proof - from pip_e[unfolded is_exit] show ?thesis - by (cases, unfold holdents_def s_holding_def, fold wq_def, - auto elim!:running_wqE) + apply(cases) + unfolding holdents_def s_holding_def + by (metis (mono_tags, lifting) empty_iff list.sel(1) mem_Collect_eq running_wqE) qed lemma wq_threads_kept: @@ -1562,7 +1563,7 @@ proof - from assms(1) have "wq (e#s) c = wq s c" by auto from assms(2)[unfolded s_holding_def, folded wq_def, - folded this, unfolded wq_def, folded s_holding_def] + folded this, folded s_holding_def] show ?thesis . qed @@ -1624,7 +1625,7 @@ lemma holding_taker: shows "holding (e#s) taker cs" - by (unfold s_holding_def, fold wq_def, unfold wq_es_cs, + by (unfold s_holding_def, unfold wq_es_cs, auto simp:neq_wq' taker_def) lemma waiting_esI2: @@ -1692,7 +1693,7 @@ case False hence "wq (e#s) c = wq s c" by auto from assms[unfolded s_holding_def, folded wq_def, - unfolded this, unfolded wq_def, folded s_holding_def] + unfolded this, folded s_holding_def] have "holding s t c" . from that(2)[OF False this] show ?thesis . qed @@ -1795,7 +1796,7 @@ case False hence "wq (e#s) c = wq s c" by auto from assms[unfolded s_holding_def, folded wq_def, - unfolded this, unfolded wq_def, folded s_holding_def] + unfolded this, folded s_holding_def] have "holding s t c" . from that[OF False this] show ?thesis . qed @@ -1829,13 +1830,13 @@ with waiting(1,2) show ?thesis by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, - fold waiting_eq, auto) + fold s_waiting_abv, auto) next case 2 with waiting(1,2) show ?thesis by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, - fold waiting_eq, auto) + fold s_waiting_abv, auto) qed next case True @@ -1848,7 +1849,7 @@ with waiting(1,2) show ?thesis by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def, - fold waiting_eq, auto) + fold s_waiting_abv, auto) qed qed next @@ -1865,13 +1866,13 @@ with holding(1,2) show ?thesis by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, - fold waiting_eq, auto) + fold s_waiting_abv, auto) next case 2 with holding(1,2) show ?thesis by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, - fold holding_eq, auto) + fold s_holding_abv, auto) qed next case True @@ -1884,7 +1885,7 @@ with holding(1,2) show ?thesis by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def, - fold holding_eq, auto) + fold s_holding_abv, auto) qed qed qed @@ -1906,7 +1907,7 @@ assume "n2 = Th h_n.taker \ n1 = Cs cs" with h_n.holding_taker show ?thesis - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) next assume h: "(n1, n2) \ RAG s \ (n1 \ Cs cs \ n2 \ Th th) \ (n1 \ Th h_n.taker \ n2 \ Cs cs)" @@ -1935,7 +1936,7 @@ qed qed thus ?thesis using waiting(1,2) - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) next case (holding th' cs') from h this(1,2) @@ -1951,7 +1952,7 @@ show ?thesis . qed thus ?thesis using holding(1,2) - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) qed qed next @@ -1967,7 +1968,7 @@ case (waiting th' cs') from h_e.waiting_esI2[OF this(3)] show ?thesis using waiting(1,2) - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) next case (holding th' cs') with h_s(2) @@ -1977,12 +1978,12 @@ assume neq_cs: "cs' \ cs" from holding_esI2[OF this holding(3)] show ?thesis using holding(1,2) - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) next assume "th' \ th" from holding_esI1[OF holding(3) this] show ?thesis using holding(1,2) - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) qed qed qed @@ -2006,7 +2007,7 @@ proof(cases "cs' = cs") case False hence "wq (e#s) cs' = wq s cs'" by simp - with assms show ?thesis unfolding holding_raw_def holding_eq by auto + with assms show ?thesis unfolding holding_raw_def s_holding_abv by auto next case True from assms[unfolded s_holding_def, folded wq_def] @@ -2015,7 +2016,7 @@ hence "wq (e#s) cs' = th'#(rest@[th])" by (simp add: True wq_es_cs) thus ?thesis - by (simp add: holding_raw_def holding_eq) + by (simp add: holding_raw_def s_holding_abv) qed end @@ -2038,11 +2039,11 @@ proof - from wq_es_cs' have "th \ set (wq (e#s) cs)" "th = hd (wq (e#s) cs)" by auto - thus ?thesis unfolding holding_raw_def holding_eq by blast + thus ?thesis unfolding holding_raw_def s_holding_abv by blast qed lemma RAG_edge: "(Cs cs, Th th) \ RAG (e#s)" - by (unfold s_RAG_def, fold holding_eq, insert holding_es_th_cs, auto) + by (unfold s_RAG_def, fold s_holding_abv, insert holding_es_th_cs, auto) lemma waiting_esE: assumes "waiting (e#s) th' cs'" @@ -2063,7 +2064,7 @@ next case False have "holding s th' cs'" using assms - using False unfolding holding_raw_def holding_eq by auto + using False unfolding holding_raw_def s_holding_abv by auto from that(1)[OF False this] show ?thesis . qed @@ -2079,7 +2080,7 @@ proof(cases rule:waiting_esE) case 1 thus ?thesis using waiting(1,2) - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) qed next case (holding th' cs') @@ -2088,7 +2089,7 @@ proof(cases rule:holding_esE) case 1 with holding(1,2) - show ?thesis by (unfold s_RAG_def, fold holding_eq, auto) + show ?thesis by (unfold s_RAG_def, fold s_holding_abv, auto) next case 2 with holding(1,2) show ?thesis by auto @@ -2106,18 +2107,18 @@ case (waiting th' cs') from waiting_kept[OF this(3)] show ?thesis using waiting(1,2) - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) next case (holding th' cs') from holding_kept[OF this(3)] show ?thesis using holding(1,2) - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) qed next assume "n1 = Cs cs \ n2 = Th th" with holding_es_th_cs show ?thesis - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) qed qed @@ -2133,11 +2134,12 @@ by (simp add: wq_es_cs wq_s_cs) lemma waiting_es_th_cs: "waiting (e#s) th cs" - using th_not_in_wq waiting_eq wq_es_cs' wq_s_cs - by (simp add: s_waiting_def wq_def wq_es_cs) + using th_not_in_wq s_waiting_abv wq_es_cs' wq_s_cs + using Un_iff list.sel(1) list.set_intros(1) s_waiting_def + set_append wq_def wq_es_cs by auto lemma RAG_edge: "(Th th, Cs cs) \ RAG (e#s)" - by (unfold s_RAG_def, fold waiting_eq, insert waiting_es_th_cs, auto) + by (unfold s_RAG_def, fold s_waiting_abv, insert waiting_es_th_cs, auto) lemma holding_esE: assumes "holding (e#s) th' cs'" @@ -2187,7 +2189,7 @@ proof(cases rule:waiting_esE) case 1 thus ?thesis using waiting(1,2) - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) next case 2 thus ?thesis using waiting(1,2) by auto @@ -2199,7 +2201,7 @@ proof(cases rule:holding_esE) case 1 with holding(1,2) - show ?thesis by (unfold s_RAG_def, fold holding_eq, auto) + show ?thesis by (unfold s_RAG_def, fold s_holding_abv, auto) qed qed next @@ -2214,12 +2216,12 @@ case (waiting th' cs') from waiting_kept[OF this(3)] show ?thesis using waiting(1,2) - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) next case (holding th' cs') from holding_kept[OF this(3)] show ?thesis using holding(1,2) - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) qed next assume "n1 = Th th \ n2 = Cs cs" @@ -2620,7 +2622,7 @@ "(Th taker, Cs cs') \ RAG s" by (unfold s_RAG_def, auto) from this(2) have "waiting s taker cs'" - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) from waiting_unique[OF this waiting_taker] have "cs' = cs" . from h(1)[unfolded this] show False by auto @@ -2655,7 +2657,7 @@ obtain cs' where h: "(Th th, Cs cs') \ RAG s" by (unfold s_RAG_def, auto) hence "waiting s th cs'" - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) with th_not_waiting show False by auto qed ultimately show ?thesis by auto @@ -2784,7 +2786,7 @@ begin lemma unique_RAG: "\(n, n1) \ RAG s; (n, n2) \ RAG s\ \ n1 = n2" - apply(unfold s_RAG_def, auto, fold waiting_eq holding_eq) + apply(unfold s_RAG_def, auto, fold s_waiting_abv s_holding_abv) by(auto elim:waiting_unique held_unique) lemma sgv_RAG: "single_valued (RAG s)" @@ -2962,11 +2964,11 @@ obtain n where "(n, b) \ RAG s" by auto from this[unfolded Cs] obtain th1 where "waiting s th1 cs" - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) from waiting_holding[OF this] obtain th2 where "holding s th2 cs" . hence "(Cs cs, Th th2) \ RAG s" - by (unfold s_RAG_def, fold holding_eq, auto) + by (unfold s_RAG_def, fold s_holding_abv, auto) with h_b(2)[unfolded Cs, rule_format] have False by auto thus ?thesis by auto @@ -2975,7 +2977,7 @@ proof - from h_b(2)[unfolded eq_b] have "\cs. \ waiting s th' cs" - by (unfold s_RAG_def, fold waiting_eq, auto) + by (unfold s_RAG_def, fold s_waiting_abv, auto) moreover have "th' \ threads s" proof(rule rg_RAG_threads) from tranclD[OF h_b(1), unfolded eq_b] @@ -3123,7 +3125,7 @@ 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) + by (unfold s_RAG_def, fold s_waiting_abv, auto) with running_1 show False by (unfold running_def readys_def, auto) qed @@ -3139,7 +3141,7 @@ 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) + by (unfold s_RAG_def, fold s_waiting_abv, auto) with running_2 show False by (unfold running_def readys_def, auto) qed @@ -3232,7 +3234,7 @@ obtain z where "(Th th1, z) \ RAG s" by auto from this[unfolded s_RAG_def, folded wq_def] obtain cs' where "waiting s th1 cs'" - by (auto simp:waiting_eq) + by (auto simp:s_waiting_abv) with assms(1) show False by (auto simp:readys_def) qed next @@ -3251,7 +3253,7 @@ obtain z where "(Th th2, z) \ RAG s" by auto from this[unfolded s_RAG_def, folded wq_def] obtain cs' where "waiting s th2 cs'" - by (auto simp:waiting_eq) + by (auto simp:s_waiting_abv) with assms(2) show False by (auto simp:readys_def) qed qed @@ -3425,10 +3427,10 @@ begin lemma holding_s_holder: "holding s holder cs" - by (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto) + by (unfold s_holding_def, unfold wq_s_cs, auto) lemma holding_es_holder: "holding (e#s) holder cs" - by (unfold s_holding_def, fold wq_def, unfold wq_es_cs wq_s_cs, auto) + by (unfold s_holding_def, unfold wq_es_cs wq_s_cs, auto) lemma holdents_es: shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") @@ -3448,7 +3450,7 @@ hence "wq (e#s) cs' = wq s cs'" by simp from h[unfolded s_holding_def, folded wq_def, unfolded this] show ?thesis - by (unfold s_holding_def, fold wq_def, auto) + by (unfold s_holding_def, auto) qed hence "cs' \ ?R" by (auto simp:holdents_def) } moreover { @@ -3467,7 +3469,7 @@ hence "wq s cs' = wq (e#s) cs'" by simp from h[unfolded s_holding_def, folded wq_def, unfolded this] show ?thesis - by (unfold s_holding_def, fold wq_def, auto) + by (unfold s_holding_def, auto) qed hence "cs' \ ?L" by (auto simp:holdents_def) } ultimately show ?thesis by auto @@ -3598,7 +3600,7 @@ from h_e[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp[OF this]] have "th' \ set (wq s cs') \ th' = hd (wq s cs')" . hence "cs' \ ?R" - by (unfold holdents_def s_holding_def, fold wq_def, auto) + by (unfold holdents_def s_holding_def, auto) } moreover { fix cs' assume "cs' \ ?R" @@ -3738,7 +3740,7 @@ lemma holding_th_cs_s: "holding s th cs" - by (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto) + by (unfold s_holding_def, unfold wq_s_cs, auto) lemma th_ready_s [simp]: "th \ readys s" using running_th_s @@ -3931,7 +3933,7 @@ from h have "holding (e#s) th' cs'" by (auto simp:holdents_def) from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq] show ?thesis - by (unfold holdents_def s_holding_def, fold wq_def, auto) + by (unfold holdents_def s_holding_def, auto) next case True from h[unfolded this] @@ -3950,7 +3952,7 @@ from h have "holding s th' cs'" by (auto simp:holdents_def) from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq] show ?thesis - by (unfold holdents_def s_holding_def, fold wq_def, insert eq_wq, simp) + by (unfold holdents_def s_holding_def, insert eq_wq, simp) next case True from h[unfolded this] @@ -4107,7 +4109,7 @@ from h have "holding (e#s) th' cs'" by (auto simp:holdents_def) from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq] show ?thesis - by (unfold holdents_def s_holding_def, fold wq_def, auto) + by (unfold holdents_def s_holding_def, auto) next case True from h[unfolded this] @@ -4126,7 +4128,7 @@ from h have "holding s th' cs'" by (auto simp:holdents_def) from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq] show ?thesis - by (unfold holdents_def s_holding_def, fold wq_def, insert eq_wq, simp) + by (unfold holdents_def s_holding_def, insert eq_wq, simp) next case True from h[unfolded this] @@ -4315,14 +4317,12 @@ { fix cs' assume h: "cs' \ ?L" hence "cs' \ ?R" - by (unfold holdents_def s_holding_def, fold wq_def, - unfold wq_kept, auto) + by (unfold holdents_def s_holding_def, unfold wq_kept, auto) } moreover { fix cs' assume h: "cs' \ ?R" hence "cs' \ ?L" - by (unfold holdents_def s_holding_def, fold wq_def, - unfold wq_kept, auto) + by (unfold holdents_def s_holding_def, unfold wq_kept, auto) } ultimately show ?thesis by auto qed @@ -4432,7 +4432,7 @@ assume "holding (e # s) th cs'" from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept] have "holding s th cs'" - by (unfold s_holding_def, fold wq_def, auto) + by (unfold s_holding_def, auto) with not_holding_th_s show False by simp qed @@ -4462,14 +4462,12 @@ { fix cs' assume h: "cs' \ ?L" hence "cs' \ ?R" - by (unfold holdents_def s_holding_def, fold wq_def, - unfold wq_kept, auto) + by (unfold holdents_def s_holding_def, unfold wq_kept, auto) } moreover { fix cs' assume h: "cs' \ ?R" hence "cs' \ ?L" - by (unfold holdents_def s_holding_def, fold wq_def, - unfold wq_kept, auto) + by (unfold holdents_def s_holding_def, unfold wq_kept, auto) } ultimately show ?thesis by auto qed @@ -4567,14 +4565,12 @@ { fix cs' assume h: "cs' \ ?L" hence "cs' \ ?R" - by (unfold holdents_def s_holding_def, fold wq_def, - unfold wq_kept, auto) + by (unfold holdents_def s_holding_def, unfold wq_kept, auto) } moreover { fix cs' assume h: "cs' \ ?R" hence "cs' \ ?L" - by (unfold holdents_def s_holding_def, fold wq_def, - unfold wq_kept, auto) + by (unfold holdents_def s_holding_def, unfold wq_kept, auto) } ultimately show ?thesis by auto qed @@ -4639,8 +4635,8 @@ proof(induct rule:ind) case Nil thus ?case - by (unfold cntP_def cntV_def pvD_def cntCS_def holdents_def - s_holding_def, simp) + unfolding cntP_def cntV_def pvD_def cntCS_def holdents_def s_holding_def + by(simp add: wq_def) next case (Cons s e) interpret vt_e: valid_trace_e s e using Cons by simp @@ -4772,7 +4768,7 @@ 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 + using assms count_eq_RAG_plus dependants_alt_def s_dependants_def by blast lemma count_eq_tRAG_plus_Th: assumes "cntP s th = cntV s th" @@ -4880,7 +4876,7 @@ 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) + auto simp:s_waiting_abv s_RAG_def) with cncs_z show ?thesis using cnp_cnv_cncs by (simp add:pvD_def) next case False diff -r e3cf792db636 -r 0f124691c191 PIPDefs.thy --- a/PIPDefs.thy Tue Jun 14 15:06:16 2016 +0100 +++ b/PIPDefs.thy Fri Jun 17 09:46:25 2016 +0100 @@ -1,6 +1,6 @@ (*<*) theory PIPDefs -imports Precedence_ord RTree Max +imports Precedence_ord Max begin (*>*) @@ -8,8 +8,8 @@ text {* - In this section, the formal model of Priority Inheritance Protocol (PIP) - is presented. The model is based on Paulson's inductive protocol + In this chapter, the formal model of the Priority Inheritance Protocol + (PIP) is presented. The model is based on Paulson's inductive protocol verification method, where the state of the system is modelled as a list of events (trace) happened so far with the latest event put at the head. *} @@ -18,12 +18,12 @@ To define events, the identifiers of {\em threads}, {\em priority} and {\em critical resources } (abbreviated as @{text "cs"}) need to be - represented. All three are represetned using standard Isabelle/HOL type + represented. All three are represented using standard Isabelle/HOL type @{typ "nat"}: *} -type_synonym thread = nat -- {* Type for thread identifiers. *} +type_synonym thread = nat -- {* Type for thread identifiers. *} type_synonym priority = nat -- {* Type for priorities. *} -type_synonym cs = nat -- {* Type for critical sections (or critical resources). *} +type_synonym cs = nat -- {* Type for critical sections (or critical resources). *} text {* @@ -38,33 +38,13 @@ | V thread cs -- {* Thread @{text "thread"} releasing critical resource @{text "cs"}. *} | Set thread priority -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *} -fun actor where - "actor (Exit th) = th" | - "actor (P th cs) = th" | - "actor (V th cs) = th" | - "actor (Set th pty) = th" | - "actor (Create th prio) = th" --- {* The actions of a set of threads *} -definition "actions_of ths s = filter (\ e. actor e \ ths) s" - -fun isCreate :: "event \ bool" where - "isCreate (Create th pty) = True" | - "isCreate _ = False" - -fun isP :: "event \ bool" where - "isP (P th cs) = True" | - "isP _ = False" - -fun isV :: "event \ bool" where - "isV (V th cs) = True" | - "isV _ = False" text {* - As mentioned earlier, in Paulson's inductive method, the states of system - are represented as lists of events, which is defined by the following type - @{text "state"}: *} + As mentioned earlier, in Paulson's inductive method, the states of the + system are represented as lists of events, which is defined by the + following type @{text "state"}: *} type_synonym state = "event list" @@ -91,7 +71,7 @@ function}s which forms the very basis of Paulson's inductive protocol verification method. Each observation function {\em observes} one particular aspect (or attribute) of the system. For example, the attribute - observed by @{text "threads s"} is the set of threads living in state + observed by @{text "threads s"} is the set of threads being live in state @{text "s"}. The protocol being modelled The decision made the protocol being modelled is based on the {\em observation}s returned by {\em observation function}s. Since {\observation function}s forms the very @@ -102,11 +82,10 @@ text {* - \noindent Observation @{text "priority th s"} is the {\em original - priority} of thread @{text "th"} in state @{text "s"}. The {\em original - priority} is the priority assigned to a thread when it is created or when - it is reset by system call (represented by event @{text "Set thread - priority"}). *} + Observation @{text "priority th s"} is the {\em original priority} of + thread @{text "th"} in state @{text "s"}. The {\em original priority} is + the priority assigned to a thread when it is created or when it is reset + by system call (represented by event @{text "Set thread priority"}). *} fun priority :: "thread \ state \ priority" where @@ -209,10 +188,10 @@ text {* - \begin{minipage}{0.9\textwidth} The following @{text "dependants wq th"} - represents the set of threads which are RAGing on thread @{text "th"} in - Resource Allocation Graph @{text "RAG wq"}. Here, "RAGing" means waiting - directly or indirectly on the critical resource. \end{minipage} *} + \noindent The following @{text "dependants wq th"} represents the set of + threads which are waiting on thread @{text "th"} in Resource Allocation + Graph @{text "RAG wq"}. Here, "waiting" means waiting directly or + indirectly on the critical resource. *} definition dependants_raw :: "(cs \ thread list) \ thread \ thread set" @@ -233,7 +212,9 @@ definition cpreced :: "(cs \ thread list) \ state \ thread \ precedence" where - "cpreced wq s th = Max ((\th'. preced th' s) ` ({th} \ dependants_raw wq th))" + "cpreced wq s th \ Max ({preced th s} \ preceds (dependants_raw wq th) s)" + + text {* @@ -245,12 +226,18 @@ from. *} lemma cpreced_def2: - "cpreced wq s th \ Max ({preced th s} \ preceds (dependants_raw wq th) s)" + "cpreced wq s th \ Max ((\th'. preced th' s) ` ({th} \ dependants_raw wq th))" unfolding cpreced_def image_def preceds_def apply(rule eq_reflection) apply(rule_tac f="Max" in arg_cong) by (auto) +definition + cpreceds :: "(cs \ thread list) \ state \ thread set \ precedence set" + where + "cpreceds wq s ths \ {cpreced wq s th | th. th \ ths}" + + text {* \noindent Assuming @{text "qs"} be the waiting queue of a critical @@ -392,7 +379,7 @@ apply(rule ext) apply(simp add: cpreced_def) apply(simp add: dependants_raw_def RAG_raw_def waiting_raw_def holding_raw_def) -apply(simp add: preced_def) +apply(simp add: preced_def preceds_def) done text {* @@ -420,37 +407,19 @@ definition s_holding_abv: - "holding (s::state) \ holding_raw (wq_fun (schs s))" + "holding (s::state) \ holding_raw (wq s)" definition s_waiting_abv: - "waiting (s::state) \ waiting_raw (wq_fun (schs s))" + "waiting (s::state) \ waiting_raw (wq s)" definition s_RAG_abv: - "RAG (s::state) \ RAG_raw (wq_fun (schs s))" + "RAG (s::state) \ RAG_raw (wq s)" definition s_dependants_abv: - "dependants (s::state) \ dependants_raw (wq_fun (schs s))" - -text {* - - The following four lemmas relate the @{term wq} and non-@{term wq} - versions of @{term waiting}, @{term holding}, @{term dependants} and - @{term cp}. *} - -lemma waiting_eq: - shows "waiting s th cs = waiting_raw (wq s) th cs" - by (simp add: s_waiting_abv wq_def) - -lemma holding_eq: - shows "holding s th cs = holding_raw (wq s) th cs" - by (simp add: s_holding_abv wq_def) - -lemma eq_dependants: - shows "dependants_raw (wq s) = dependants s" - by (simp add: s_dependants_abv wq_def) + "dependants (s::state) \ dependants_raw (wq s)" lemma cp_eq: shows "cp s th = cpreced (wq s) s th" @@ -472,8 +441,8 @@ lemma s_holding_def: - "holding (s::state) th cs \ (th \ set (wq_fun (schs s) cs) \ th = hd (wq_fun (schs s) cs))" - by (auto simp:s_holding_abv wq_def holding_raw_def) + "holding (s::state) th cs \ (th \ set (wq s cs) \ th = hd (wq s cs))" + by(simp add: s_holding_abv holding_raw_def) lemma s_waiting_def: "waiting (s::state) th cs \ (th \ set (wq_fun (schs s) cs) \ th \ hd (wq_fun (schs s) cs))" @@ -721,14 +690,37 @@ 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 RAG_raw_def, auto) +using hRAG_def s_RAG_def s_holding_abv s_waiting_abv wRAG_def wq_def by auto 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) + +fun actor where + "actor (Exit th) = th" | + "actor (P th cs) = th" | + "actor (V th cs) = th" | + "actor (Set th pty) = th" | + "actor (Create th prio) = th" + +-- {* The actions of a set of threads *} +definition "actions_of ths s = filter (\ e. actor e \ ths) s" + +fun isCreate :: "event \ bool" where + "isCreate (Create th pty) = True" | + "isCreate _ = False" + +fun isP :: "event \ bool" where + "isP (P th cs) = True" | + "isP _ = False" + +fun isV :: "event \ bool" where + "isV (V th cs) = True" | + "isV _ = False" + + (*<*) end diff -r e3cf792db636 -r 0f124691c191 PrioG.thy --- a/PrioG.thy Tue Jun 14 15:06:16 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,797 +0,0 @@ -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, 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 - - 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 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. - - 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 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: *} - also have "... = ?R" - thm runing_preced_inversion - 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 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 - interpret vat_es: valid_trace_e "t@s" e using Cons(1,2) by (unfold_locales, auto) - 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_es.actor_inv - -- {* According to @{thm vat_es.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_es.actor_inv - 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 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 {* - 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.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) - 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 e3cf792db636 -r 0f124691c191 journal.pdf Binary file journal.pdf has changed