diff -r c495eb16beb6 -r cfd644dfc3b4 ExtGG.thy~ --- a/ExtGG.thy~ Wed Jan 27 19:28:42 2016 +0800 +++ b/ExtGG.thy~ Wed Jan 27 23:34:23 2016 +0800 @@ -1,922 +1,920 @@ -theory ExtGG -imports PrioG CpsG +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 *} + +text {* (* ddd *) + The following locale @{text "step_set_cps"} investigates the recalculation + after the @{text "Set"} operation. +*} +locale step_set_cps = + fixes s' th prio s + -- {* @{text "s'"} is the system state before the operation *} + -- {* @{text "s"} is the system state after the operation *} + defines s_def : "s \<equiv> (Set th prio#s')" + -- {* @{text "s"} is assumed to be a legitimate state, from which + the legitimacy of @{text "s"} can be derived. *} + assumes vt_s: "vt s" + +sublocale step_set_cps < vat_s : valid_trace "s" +proof + from vt_s show "vt s" . +qed + +sublocale step_set_cps < vat_s' : valid_trace "s'" +proof + from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" . +qed + +context step_set_cps begin -text {* - The following two auxiliary lemmas are used to reason about @{term Max}. +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 image_Max_eqI: - assumes "finite B" - and "b \<in> B" - and "\<forall> x \<in> B. f x \<le> f b" - shows "Max (f ` B) = f b" + +lemma eq_preced: + assumes "th' \<noteq> th" + shows "preced th' s = preced th' s'" +proof - + from assms show ?thesis + by (unfold s_def, auto simp:preced_def) +qed + +lemma eq_the_preced: + assumes "th' \<noteq> th" + shows "the_preced s th' = the_preced s' th'" using assms - using Max_eqI by blast + by (unfold the_preced_def, intro eq_preced, simp) + +text {* + The following lemma assures that the resetting of priority does not change the RAG. +*} + +lemma eq_dep: "RAG s = RAG s'" + by (unfold s_def RAG_set_unchanged, auto) -lemma image_Max_subset: - assumes "finite A" - and "B \<subseteq> A" - and "a \<in> 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 \<in> B" using assms by simp -next - show "\<forall>x\<in>B. f x \<le> f a" - by (metis Max_ge assms(1) assms(2) assms(4) - finite_imageI image_eqI subsetCE) +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 \<notin> subtree (RAG s') (Th th')" + shows "cp 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 s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')}) = + Max (the_preced s' ` {th'a. Th th'a \<in> subtree (RAG s') (Th th')})" + (is "Max (?f ` ?S1) = Max (?g ` ?S2)") + proof - + -- {* The base sets are equal. *} + have "?S1 = ?S2" using eq_dep by simp + -- {* The function values on the base set are equal as well. *} + moreover have "\<forall> e \<in> ?S2. ?f e = ?g e" + proof + fix th1 + assume "th1 \<in> ?S2" + with nd have "th1 \<noteq> th" by (auto) + from eq_the_preced[OF this] + show "the_preced 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 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. + The following lemma shows that @{term "th"} is not in the + sub-tree of any other thread. *} -locale highest_gen = - fixes s th prio tm +lemma th_in_no_subtree: + assumes "th' \<noteq> th" + shows "Th th \<notin> subtree (RAG s') (Th th')" +proof - + have "th \<in> readys s'" + proof - + from step_back_step [OF vt_s[unfolded s_def]] + have "step s' (Set th prio)" . + hence "th \<in> runing s'" by (cases, simp) + thus ?thesis by (simp add:readys_def runing_def) + qed + from vat_s'.readys_in_no_subtree[OF this 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' \<noteq> th" + shows "cp 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. +*} + +locale step_v_cps = + -- {* @{text "th"} is the initiating thread *} + -- {* @{text "cs"} is the critical resource release by the @{text "V"}-operation *} + fixes s' th cs s -- {* @{text "s'"} is the state before operation*} + defines s_def : "s \<equiv> (V th cs#s')" -- {* @{text "s"} is the state after operation*} + -- {* @{text "s"} is assumed to be valid, which implies the validity of @{text "s'"} *} assumes vt_s: "vt s" - and threads_s: "th \<in> 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" + +sublocale step_v_cps < vat_s : valid_trace "s" +proof + from vt_s show "vt s" . +qed + +sublocale step_v_cps < vat_s' : valid_trace "s'" +proof + from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" . +qed + +context step_v_cps +begin + +lemma ready_th_s': "th \<in> readys s'" + using step_back_step[OF vt_s[unfolded s_def]] + by (cases, simp add:runing_def) + +lemma ancestors_th: "ancestors (RAG s') (Th th) = {}" +proof - + from vat_s'.readys_root[OF ready_th_s'] + show ?thesis + by (unfold root_def, simp) +qed + +lemma holding_th: "holding s' th cs" +proof - + from vt_s[unfolded s_def] + have " PIP s' (V th cs)" by (cases, simp) + thus ?thesis by (cases, auto) +qed --- {* @{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) +lemma edge_of_th: + "(Cs cs, Th th) \<in> RAG s'" +proof - + from holding_th + show ?thesis + by (unfold s_RAG_def holding_eq, auto) +qed -context highest_gen +lemma ancestors_cs: + "ancestors (RAG s') (Cs cs) = {Th th}" +proof - + have "ancestors (RAG s') (Cs cs) = ancestors (RAG s') (Th th) \<union> {Th th}" + proof(rule vat_s'.rtree_RAG.ancestors_accum) + from vt_s[unfolded s_def] + have " PIP s' (V th cs)" by (cases, simp) + thus "(Cs cs, Th th) \<in> RAG s'" + proof(cases) + assume "holding s' th cs" + from this[unfolded holding_eq] + show ?thesis by (unfold s_RAG_def, auto) + qed + qed + from this[unfolded ancestors_th] show ?thesis by simp +qed + +lemma preced_kept: "the_preced s = the_preced s'" + by (auto simp: s_def the_preced_def preced_def) + +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"}. +*} +locale step_v_cps_nt = step_v_cps + + fixes th' + -- {* @{text "th'"} is assumed to take over @{text "cs"} *} + assumes nt: "next_th s' th cs th'" + +context step_v_cps_nt 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 @{text "RAG_s"} confirms the change of RAG: + two edges removed and one added, as shown by the following diagram. *} -lemma lt_tm: "tm < length s" - by (insert preced_tm_lt[OF threads_s preced_th], simp) + +(* + RAG before the V-operation + th1 ----| + | + th' ----| + |----> cs -----| + th2 ----| | + | | + th3 ----| | + |------> th + th4 ----| | + | | + th5 ----| | + |----> cs'-----| + th6 ----| + | + th7 ----| + + RAG after the V-operation + th1 ----| + | + |----> cs ----> th' + th2 ----| + | + th3 ----| + + th4 ----| + | + th5 ----| + |----> cs'----> th + th6 ----| + | + th7 ----| +*) + +lemma sub_RAGs': "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s'" + using next_th_RAG[OF nt] . + +lemma ancestors_th': + "ancestors (RAG s') (Th th') = {Th th, Cs cs}" +proof - + have "ancestors (RAG s') (Th th') = ancestors (RAG s') (Cs cs) \<union> {Cs cs}" + proof(rule vat_s'.rtree_RAG.ancestors_accum) + from sub_RAGs' show "(Th th', Cs cs) \<in> RAG s'" by auto + qed + thus ?thesis using ancestors_th ancestors_cs by auto +qed + +lemma RAG_s: + "RAG s = (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union> + {(Cs cs, Th th')}" +proof - + from step_RAG_v[OF vt_s[unfolded s_def], folded s_def] + and nt show ?thesis by (auto intro:next_th_unique) +qed -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") +lemma subtree_kept: (* ddd *) + assumes "th1 \<notin> {th, th'}" + shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)" (is "_ = ?R") proof - - have "?L \<le> ?R" - by (unfold highest, rule Max_ge, - auto simp:threads_s finite_threads) - moreover have "?R \<le> ?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 + let ?RAG' = "(RAG s' - {(Cs cs, Th th), (Th th', Cs cs)})" + let ?RAG'' = "?RAG' \<union> {(Cs cs, Th th')}" + have "subtree ?RAG' (Th th1) = ?R" + proof(rule subset_del_subtree_outside) + show "Range {(Cs cs, Th th), (Th th', Cs cs)} \<inter> subtree (RAG s') (Th th1) = {}" + proof - + have "(Th th) \<notin> subtree (RAG s') (Th th1)" + proof(rule subtree_refute) + show "Th th1 \<notin> ancestors (RAG s') (Th th)" + by (unfold ancestors_th, simp) + next + from assms show "Th th1 \<noteq> Th th" by simp + qed + moreover have "(Cs cs) \<notin> subtree (RAG s') (Th th1)" + proof(rule subtree_refute) + show "Th th1 \<notin> ancestors (RAG s') (Cs cs)" + by (unfold ancestors_cs, insert assms, auto) + qed simp + ultimately have "{Th th, Cs cs} \<inter> 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 th' \<notin> subtree (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) (Th th1)" + proof(rule subtree_refute) + show "Th th1 \<notin> ancestors (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) (Th th')" + (is "_ \<notin> ?R") + proof - + have "?R \<subseteq> ancestors (RAG s') (Th th')" by (rule ancestors_mono, auto) + moreover have "Th th1 \<notin> ..." using ancestors_th' assms by simp + ultimately show ?thesis by auto + qed + next + from assms show "Th th1 \<noteq> Th th'" by simp + qed + qed + ultimately show ?thesis by (unfold RAG_s, simp) +qed + +lemma cp_kept: + assumes "th1 \<notin> {th, th'}" + shows "cp s th1 = cp s' th1" + by (unfold cp_alt_def preced_kept subtree_kept[OF assms], simp) + +end + +locale step_v_cps_nnt = step_v_cps + + assumes nnt: "\<And> th'. (\<not> next_th s' th cs th')" + +context step_v_cps_nnt +begin + +lemma RAG_s: "RAG s = RAG s' - {(Cs cs, Th th)}" +proof - + from nnt and step_RAG_v[OF vt_s[unfolded s_def], folded s_def] + show ?thesis by auto qed -(* ccc *) -lemma highest_cp_preced: "cp s th = Max ((\<lambda> th'. preced th' s) ` threads s)" - by (fold max_cp_eq, unfold eq_cp_s_th, insert highest, simp) +lemma subtree_kept: + assumes "th1 \<noteq> th" + shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)" +proof(unfold RAG_s, rule subset_del_subtree_outside) + show "Range {(Cs cs, Th th)} \<inter> subtree (RAG s') (Th th1) = {}" + proof - + have "(Th th) \<notin> subtree (RAG s') (Th th1)" + proof(rule subtree_refute) + show "Th th1 \<notin> ancestors (RAG s') (Th th)" + by (unfold ancestors_th, simp) + next + from assms show "Th th1 \<noteq> Th th" by simp + qed + thus ?thesis by auto + qed +qed + +lemma cp_kept_1: + assumes "th1 \<noteq> th" + shows "cp s th1 = cp s' th1" + by (unfold cp_alt_def preced_kept subtree_kept[OF assms], simp) + +lemma subtree_cs: "subtree (RAG s') (Cs cs) = {Cs cs}" +proof - + { fix n + have "(Cs cs) \<notin> ancestors (RAG s') n" + proof + assume "Cs cs \<in> ancestors (RAG s') n" + hence "(n, Cs cs) \<in> (RAG s')^+" by (auto simp:ancestors_def) + from tranclE[OF this] obtain nn where h: "(nn, Cs cs) \<in> 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) \<in> 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 this] + obtain th' where "next_th s' th cs th'" by auto + with nnt show False by auto + qed + } note h = this + { fix n + assume "n \<in> subtree (RAG s') (Cs cs)" + hence "n = (Cs cs)" + by (elim subtreeE, insert h, auto) + } moreover have "(Cs cs) \<in> subtree (RAG s') (Cs cs)" + by (auto simp:subtree_def) + ultimately show ?thesis by auto +qed + +lemma subtree_th: + "subtree (RAG s) (Th th) = subtree (RAG s') (Th th) - {Cs cs}" +proof(unfold RAG_s, fold subtree_cs, rule vat_s'.rtree_RAG.subtree_del_inside) + from edge_of_th + show "(Cs cs, Th th) \<in> edges_in (RAG s') (Th th)" + by (unfold edges_in_def, auto simp:subtree_def) +qed + +lemma cp_kept_2: + shows "cp s th = cp s' th" + by (unfold cp_alt_def subtree_th preced_kept, auto) + +lemma eq_cp: + shows "cp s th' = cp s' th'" + using cp_kept_1 cp_kept_2 + by (cases "th' = th", auto) +end + + +locale step_P_cps = + fixes s' th cs s + defines s_def : "s \<equiv> (P th cs#s')" + assumes vt_s: "vt s" -lemma highest_preced_thread: "preced th s = Max ((\<lambda> th'. preced th' s) ` threads s)" - by (fold eq_cp_s_th, unfold highest_cp_preced, simp) +sublocale step_P_cps < vat_s : valid_trace "s" +proof + from vt_s show "vt s" . +qed + +section {* The @{term P} operation *} + +sublocale step_P_cps < vat_s' : valid_trace "s'" +proof + from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" . +qed + +context step_P_cps +begin + +lemma readys_th: "th \<in> readys s'" +proof - + from step_back_step [OF vt_s[unfolded s_def]] + have "PIP s' (P th cs)" . + hence "th \<in> runing s'" by (cases, simp) + thus ?thesis by (simp add:readys_def runing_def) +qed + +lemma root_th: "root (RAG s') (Th th)" + using readys_root[OF readys_th] . -lemma highest': "cp s th = Max (cp s ` threads s)" +lemma in_no_others_subtree: + assumes "th' \<noteq> th" + shows "Th th \<notin> subtree (RAG s') (Th th')" +proof + assume "Th th \<in> 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 s = the_preced s'" + by (auto simp: s_def the_preced_def preced_def) + +end + +locale step_P_cps_ne =step_P_cps + + fixes th' + assumes ne: "wq s' cs \<noteq> []" + defines th'_def: "th' \<equiv> hd (wq s' cs)" + +locale step_P_cps_e =step_P_cps + + assumes ee: "wq s' cs = []" + +context step_P_cps_e +begin + +lemma RAG_s: "RAG s = RAG s' \<union> {(Cs cs, Th th)}" proof - - from highest_cp_preced max_cp_eq[symmetric] - show ?thesis by simp + from ee and step_RAG_p[OF vt_s[unfolded s_def], folded s_def] + show ?thesis by auto +qed + +lemma subtree_kept: + assumes "th' \<noteq> th" + shows "subtree (RAG s) (Th th') = subtree (RAG s') (Th th')" +proof(unfold RAG_s, rule subtree_insert_next) + from in_no_others_subtree[OF assms] + show "Th th \<notin> subtree (RAG s') (Th th')" . +qed + +lemma cp_kept: + assumes "th' \<noteq> th" + shows "cp s th' = cp s' th'" +proof - + have "(the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')}) = + (the_preced s' ` {th'a. Th th'a \<in> subtree (RAG s') (Th th')})" + by (unfold preced_kept subtree_kept[OF assms], simp) + thus ?thesis by (unfold cp_alt_def, simp) qed end -locale extend_highest_gen = highest_gen + - fixes t - assumes vt_t: "vt (t@s)" - and create_low: "Create th' prio' \<in> set t \<Longrightarrow> prio' \<le> prio" - and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio" - and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> 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) \<Longrightarrow> 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 +context step_P_cps_ne begin - lemma ind [consumes 0, case_names Nil Cons, induct type]: - assumes - h0: "R []" - and h2: "\<And> e t. \<lbrakk>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\<rbrakk> \<Longrightarrow> R (e#t)" - shows "R t" +lemma RAG_s: "RAG s = RAG s' \<union> {(Th th, Cs cs)}" +proof - + from step_RAG_p[OF vt_s[unfolded s_def]] and ne + show ?thesis by (simp add:s_def) +qed + +lemma cs_held: "(Cs cs, Th th') \<in> RAG s'" proof - - from vt_t extend_highest_gen_axioms show ?thesis - proof(induct t) - from h0 show "R []" . - next - case (Cons e t') - assume ih: "\<lbrakk>vt (t' @ s); extend_highest_gen s th prio tm t'\<rbrakk> \<Longrightarrow> 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 + have "(Cs cs, Th th') \<in> hRAG s'" + proof - + from ne + have " holding s' th' cs" + by (unfold th'_def holding_eq cs_holding_def, auto) + thus ?thesis + by (unfold hRAG_def, auto) qed + thus ?thesis by (unfold RAG_split, auto) qed +lemma tRAG_s: + "tRAG s = tRAG s' \<union> {(Th th, Th th')}" + using RAG_tRAG_transfer[OF RAG_s cs_held] . -lemma th_kept: "th \<in> threads (t @ s) \<and> - preced th (t@s) = preced th s" (is "?Q t") +lemma cp_kept: + assumes "Th th'' \<notin> ancestors (tRAG s) (Th th)" + shows "cp s th'' = cp s' th''" 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 \<noteq> 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 \<noteq> 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 \<noteq> 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) + have h: "subtree (tRAG s) (Th th'') = subtree (tRAG s') (Th th'')" + proof - + have "Th th' \<notin> subtree (tRAG s') (Th th'')" + proof + assume "Th th' \<in> subtree (tRAG s') (Th th'')" + thus False + proof(rule subtreeE) + assume "Th th' = Th th''" + from assms[unfolded tRAG_s ancestors_def, folded this] + show ?thesis by auto + next + assume "Th th'' \<in> ancestors (tRAG s') (Th th')" + moreover have "... \<subseteq> ancestors (tRAG s) (Th th')" + proof(rule ancestors_mono) + show "tRAG s' \<subseteq> tRAG s" by (unfold tRAG_s, auto) + qed + ultimately have "Th th'' \<in> ancestors (tRAG s) (Th th')" by auto + moreover have "Th th' \<in> ancestors (tRAG s) (Th th)" + by (unfold tRAG_s, auto simp:ancestors_def) + ultimately have "Th th'' \<in> ancestors (tRAG 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' \<union> {(Th th, Th th')}) (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 -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 (unfold the_preced_def, 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") +lemma cp_gen_update_stop: (* ddd *) + assumes "u \<in> ancestors (tRAG s) (Th th)" + and "cp_gen s u = cp_gen s' u" + and "y \<in> ancestors (tRAG s) u" + shows "cp_gen s y = cp_gen s' y" + using assms(3) +proof(induct rule:wf_induct[OF vat_s.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_s.cp_gen_rec[OF this] + have "?L = + Max ({the_preced s th2} \<union> cp_gen s ` RTree.children (tRAG s) x)" . + also have "... = + Max ({the_preced s' th2} \<union> cp_gen s' ` RTree.children (tRAG s') x)" + 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 \<in> ?A" using h_e.th_kept by auto - next - show "\<forall>x\<in>?A. ?f x \<le> ?f th" - proof - fix x - assume "x \<in> ?A" - hence "x = thread \<or> x \<in> threads (t@s)" by (auto simp:Create) - thus "?f x \<le> ?f th" + from preced_kept have "the_preced s th2 = the_preced s' th2" by simp + moreover have "cp_gen s ` RTree.children (tRAG s) x = + cp_gen s' ` RTree.children (tRAG s') x" + proof - + have "RTree.children (tRAG s) x = RTree.children (tRAG s') x" + proof(unfold tRAG_s, rule children_union_kept) + have start: "(Th th, Th th') \<in> tRAG s" + by (unfold tRAG_s, auto) + note x_u = 1(2) + show "x \<notin> Range {(Th th, Th 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 \<in> threads (t @ s)" - from Cons(2)[unfolded Create] - have "x \<noteq> 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 \<le> 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 . + assume "x \<in> Range {(Th th, Th th')}" + hence eq_x: "x = Th th'" using RangeE by auto + show False + proof(cases rule:vat_s.rtree_s.ancestors_headE[OF assms(1) start]) + case 1 + from x_u[folded this, unfolded eq_x] vat_s.acyclic_tRAG + show ?thesis by (auto simp:ancestors_def acyclic_def) + next + case 2 + with x_u[unfolded eq_x] + have "(Th th', Th th') \<in> (tRAG s)^+" by (auto simp:ancestors_def) + with vat_s.acyclic_tRAG show ?thesis by (auto simp:acyclic_def) + qed 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 \<in> ?A" using h_e.th_kept by auto - next - show "\<forall>x\<in>?A. ?f x \<le> ?f th" - proof - fix x - assume "x \<in> ?A" - hence "x \<in> threads (t@s)" by (simp add: Exit) - hence "?f x \<le> Max (?f ` threads (t@s))" - by (simp add: h_t.finite_threads) - also have "... \<le> ?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 \<le> ?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 \<in> ?A" using h_e.th_kept by auto - next - show "\<forall>x\<in>?A. ?f x \<le> ?f th" - proof - fix x - assume h: "x \<in> ?A" - show "?f x \<le> ?f th" - proof(cases "x = thread") - case True - moreover have "the_preced (Set thread prio' # t @ s) thread \<le> 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' \<le> prio" using Set h_e.set_diff_low by auto - ultimately show ?thesis by (insert lt_tm, auto simp:the_preced_def preced_def) + moreover have "cp_gen s ` RTree.children (tRAG s) x = + cp_gen s' ` RTree.children (tRAG s) x" (is "?f ` ?A = ?g ` ?A") + proof(rule f_image_eq) + fix a + assume a_in: "a \<in> ?A" + from 1(2) + show "?f a = ?g a" + proof(cases rule:vat_s.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 \<notin> ancestors (tRAG s) (Th th)" + proof + assume a_in': "a \<in> ancestors (tRAG s) (Th th)" + have "a = u" + proof(rule vat_s.rtree_s.ancestors_children_unique) + from a_in' a_in show "a \<in> ancestors (tRAG s) (Th th) \<inter> + RTree.children (tRAG s) x" by auto + next + from assms(1) in_ch show "u \<in> ancestors (tRAG s) (Th th) \<inter> + RTree.children (tRAG 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 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 \<in> ancestors (tRAG s) u" "z \<in> RTree.children (tRAG s) x" by auto + show ?thesis + proof(cases "a = z") + case True + from h(2) have zx_in: "(z, x) \<in> (tRAG s)" by (auto simp:RTree.children_def) + from 1(1)[rule_format, OF this h(1)] + have eq_cp_gen: "cp_gen 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 \<notin> ancestors (tRAG s) (Th th)" + proof + assume a_in': "a \<in> ancestors (tRAG s) (Th th)" + have "a = z" + proof(rule vat_s.rtree_s.ancestors_children_unique) + from assms(1) h(1) have "z \<in> ancestors (tRAG s) (Th th)" + by (auto simp:ancestors_def) + with h(2) show " z \<in> ancestors (tRAG s) (Th th) \<inter> + RTree.children (tRAG s) x" by auto + next + from a_in a_in' + show "a \<in> ancestors (tRAG s) (Th th) \<inter> RTree.children (tRAG s) x" + by auto + qed + with False show False by auto + qed + from cp_kept[OF this[unfolded eq_a]] + have "cp s th_a = cp s' th_a" . + from this[unfolded cp_gen_def_cond[OF eq_a], folded eq_a] + show ?thesis . 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 "... \<le> 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 + ultimately show ?thesis by metis qed - also have "... = ?t" using h_e.th_kept the_preced_def by auto - finally show ?thesis . - qed + ultimately show ?thesis by simp + qed + also have "... = ?R" + by (fold vat_s'.cp_gen_rec[OF eq_x], simp) + finally show ?thesis . 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' \<in> subtree (RAG (t @ s)) (Th th)}" - proof - - have "{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)} = - the_thread ` {n . n \<in> subtree (RAG (t @ s)) (Th th) \<and> - (\<exists> 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 \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}" - by (auto simp:subtree_def) - next - show "\<forall>x\<in>{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}. - the_preced (t @ s) x \<le> the_preced (t @ s) th" - proof - fix th' - assume "th' \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}" - hence "Th th' \<in> subtree (RAG (t @ s)) (Th th)" by auto - moreover have "... \<subseteq> Field (RAG (t @ s)) \<union> {Th th}" - by (meson subtree_Field) - ultimately have "Th th' \<in> ..." by auto - hence "th' \<in> threads (t@s)" - proof - assume "Th th' \<in> {Th th}" - thus ?thesis using th_kept by auto - next - assume "Th th' \<in> Field (RAG (t @ s))" - thus ?thesis using vat_t.not_in_thread_isolated by blast - qed - thus "the_preced (t @ s) th' \<le> 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: "cp (t@s) th = Max (cp (t@s) ` threads (t@s))" - using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger - -lemma th_cp_preced: "cp (t@s) th = preced th s" - by (fold max_kept, unfold th_cp_max_preced, simp) - -lemma preced_less: - assumes th'_in: "th' \<in> threads s" - and neq_th': "th' \<noteq> 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) - -text {* - Counting of the number of @{term "P"} and @{term "V"} operations - is the cornerstone of a large number of the following proofs. - The reason is that this counting is quite easy to calculate and - convenient to use in the reasoning. - - The following lemma shows that the counting controls whether - a thread is running or not. -*} - -lemma pv_blocked_pre: - assumes th'_in: "th' \<in> threads (t@s)" - and neq_th': "th' \<noteq> th" - and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" - shows "th' \<notin> runing (t@s)" -proof - assume otherwise: "th' \<in> runing (t@s)" - show False - proof - - have "th' = th" - proof(rule preced_unique) - show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R") - proof - - have "?L = cp (t@s) th'" - by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp) - also have "... = cp (t @ s) th" using otherwise - by (metis (mono_tags, lifting) mem_Collect_eq - runing_def th_cp_max vat_t.max_cp_readys_threads) - also have "... = ?R" by (metis th_cp_preced th_kept) - finally show ?thesis . - qed - qed (auto simp: th'_in th_kept) - moreover have "th' \<noteq> th" using neq_th' . - ultimately show ?thesis by simp - qed -qed - -lemmas pv_blocked = pv_blocked_pre[folded detached_eq] - -lemma runing_precond_pre: - fixes th' - assumes th'_in: "th' \<in> threads s" - and eq_pv: "cntP s th' = cntV s th'" - and neq_th': "th' \<noteq> th" - shows "th' \<in> threads (t@s) \<and> - cntP (t@s) th' = cntV (t@s) th'" -proof(induct rule:ind) - case (Cons e t) - interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp - interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp - show ?case - proof(cases e) - case (P thread cs) - show ?thesis - proof - - have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" - proof - - have "thread \<noteq> th'" - proof - - have "step (t@s) (P thread cs)" using Cons P by auto - thus ?thesis - proof(cases) - assume "thread \<in> runing (t@s)" - moreover have "th' \<notin> runing (t@s)" using Cons(5) - by (metis neq_th' vat_t.pv_blocked_pre) - ultimately show ?thesis by auto - qed - qed with Cons show ?thesis - by (unfold P, simp add:cntP_def cntV_def count_def) - qed - moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold P, simp) - ultimately show ?thesis by auto - qed - next - case (V thread cs) - show ?thesis - proof - - have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" - proof - - have "thread \<noteq> th'" - proof - - have "step (t@s) (V thread cs)" using Cons V by auto - thus ?thesis - proof(cases) - assume "thread \<in> runing (t@s)" - moreover have "th' \<notin> runing (t@s)" using Cons(5) - by (metis neq_th' vat_t.pv_blocked_pre) - ultimately show ?thesis by auto - qed - qed with Cons show ?thesis - by (unfold V, simp add:cntP_def cntV_def count_def) - qed - moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold V, simp) - ultimately show ?thesis by auto - qed - next - case (Create thread prio') - show ?thesis - proof - - have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" - proof - - have "thread \<noteq> th'" - proof - - have "step (t@s) (Create thread prio')" using Cons Create by auto - thus ?thesis using Cons(5) by (cases, auto) - qed with Cons show ?thesis - by (unfold Create, simp add:cntP_def cntV_def count_def) - qed - moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold Create, simp) - ultimately show ?thesis by auto - qed - next - case (Exit thread) - show ?thesis - proof - - have neq_thread: "thread \<noteq> th'" - proof - - have "step (t@s) (Exit thread)" using Cons Exit by auto - thus ?thesis apply (cases) using Cons(5) - by (metis neq_th' vat_t.pv_blocked_pre) - qed - hence "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" using Cons - by (unfold Exit, simp add:cntP_def cntV_def count_def) - moreover have "th' \<in> threads ((e # t) @ s)" using Cons neq_thread - by (unfold Exit, simp) - ultimately show ?thesis by auto - qed - next - case (Set thread prio') - with Cons - show ?thesis - by (auto simp:cntP_def cntV_def count_def) - qed -next - case Nil - with assms - show ?case by auto -qed - -text {* Changing counting balance to detachedness *} -lemmas runing_precond_pre_dtc = runing_precond_pre - [folded vat_t.detached_eq vat_s.detached_eq] - -lemma runing_precond: - fixes th' - assumes th'_in: "th' \<in> threads s" - and neq_th': "th' \<noteq> th" - and is_runing: "th' \<in> runing (t@s)" - shows "cntP s th' > cntV s th'" - using assms -proof - - have "cntP s th' \<noteq> cntV s th'" - by (metis is_runing neq_th' pv_blocked_pre runing_precond_pre th'_in) - moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto - ultimately show ?thesis by auto -qed - -lemma moment_blocked_pre: - assumes neq_th': "th' \<noteq> th" - and th'_in: "th' \<in> threads ((moment i t)@s)" - and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" - shows "cntP ((moment (i+j) t)@s) th' = cntV ((moment (i+j) t)@s) th' \<and> - th' \<in> threads ((moment (i+j) t)@s)" +lemma cp_up: + assumes "(Th th') \<in> ancestors (tRAG s) (Th th)" + and "cp s th' = cp s' th'" + and "(Th th'') \<in> ancestors (tRAG s) (Th th')" + shows "cp s th'' = cp s' th''" proof - - interpret h_i: red_extend_highest_gen _ _ _ _ _ i - by (unfold_locales) - interpret h_j: red_extend_highest_gen _ _ _ _ _ "i+j" - by (unfold_locales) - interpret h: extend_highest_gen "((moment i t)@s)" th prio tm "moment j (restm i t)" - proof(unfold_locales) - show "vt (moment i t @ s)" by (metis h_i.vt_t) - next - show "th \<in> threads (moment i t @ s)" by (metis h_i.th_kept) - next - show "preced th (moment i t @ s) = - Max (cp (moment i t @ s) ` threads (moment i t @ s))" - by (metis h_i.th_cp_max h_i.th_cp_preced h_i.th_kept) - next - show "preced th (moment i t @ s) = Prc prio tm" by (metis h_i.th_kept preced_th) - next - show "vt (moment j (restm i t) @ moment i t @ s)" - using moment_plus_split by (metis add.commute append_assoc h_j.vt_t) - next - fix th' prio' - assume "Create th' prio' \<in> set (moment j (restm i t))" - thus "prio' \<le> prio" using assms - by (metis Un_iff add.commute h_j.create_low moment_plus_split set_append) - next - fix th' prio' - assume "Set th' prio' \<in> set (moment j (restm i t))" - thus "th' \<noteq> th \<and> prio' \<le> prio" - by (metis Un_iff add.commute h_j.set_diff_low moment_plus_split set_append) - next - fix th' - assume "Exit th' \<in> set (moment j (restm i t))" - thus "th' \<noteq> th" - by (metis Un_iff add.commute h_j.exit_diff moment_plus_split set_append) - qed - show ?thesis - by (metis add.commute append_assoc eq_pv h.runing_precond_pre - moment_plus_split neq_th' th'_in) -qed - -lemma moment_blocked_eqpv: - assumes neq_th': "th' \<noteq> th" - and th'_in: "th' \<in> threads ((moment i t)@s)" - and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" - and le_ij: "i \<le> j" - shows "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th' \<and> - th' \<in> threads ((moment j t)@s) \<and> - th' \<notin> runing ((moment j t)@s)" -proof - - from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij - have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'" - and h2: "th' \<in> threads ((moment j t)@s)" by auto - moreover have "th' \<notin> runing ((moment j t)@s)" - proof - - interpret h: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) - show ?thesis - using h.pv_blocked_pre h1 h2 neq_th' by auto + have "cp_gen 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 s (Th th') = cp_gen s' (Th th')" by metis qed - ultimately show ?thesis by auto -qed - -(* The foregoing two lemmas are preparation for this one, but - in long run can be combined. Maybe I am wrong. -*) -lemma moment_blocked: - assumes neq_th': "th' \<noteq> th" - and th'_in: "th' \<in> threads ((moment i t)@s)" - and dtc: "detached (moment i t @ s) th'" - and le_ij: "i \<le> j" - shows "detached (moment j t @ s) th' \<and> - th' \<in> threads ((moment j t)@s) \<and> - th' \<notin> runing ((moment j t)@s)" -proof - - interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales) - interpret h_j: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) - have cnt_i: "cntP (moment i t @ s) th' = cntV (moment i t @ s) th'" - by (metis dtc h_i.detached_elim) - from moment_blocked_eqpv[OF neq_th' th'_in cnt_i le_ij] - show ?thesis by (metis h_j.detached_intro) -qed - -lemma runing_preced_inversion: - assumes runing': "th' \<in> 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 "\<dots> = ?R" - by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) - finally show ?thesis . -qed - -text {* - The situation when @{term "th"} is blocked is analyzed by the following lemmas. -*} - -text {* - The following lemmas shows the running thread @{text "th'"}, if it is different from - @{term th}, must be live at the very beginning. By the term {\em the very beginning}, - we mean the moment where the formal investigation starts, i.e. the moment (or state) - @{term s}. -*} - -lemma runing_inversion_0: - assumes neq_th': "th' \<noteq> th" - and runing': "th' \<in> runing (t@s)" - shows "th' \<in> threads s" -proof - - -- {* The proof is by contradiction: *} - { assume otherwise: "\<not> ?thesis" - have "th' \<notin> runing (t @ s)" - proof - - -- {* Since @{term "th'"} is running at time @{term "t@s"}, so it exists that time. *} - have th'_in: "th' \<in> threads (t@s)" using runing' by (simp add:runing_def readys_def) - -- {* However, @{text "th'"} does not exist at very beginning. *} - have th'_notin: "th' \<notin> threads (moment 0 t @ s)" using otherwise - by (metis append.simps(1) moment_zero) - -- {* Therefore, there must be a moment during @{text "t"}, when - @{text "th'"} came into being. *} - -- {* Let us suppose the moment being @{text "i"}: *} - from p_split_gen[OF th'_in th'_notin] - obtain i where lt_its: "i < length t" - and le_i: "0 \<le> i" - and pre: " th' \<notin> threads (moment i t @ s)" (is "th' \<notin> threads ?pre") - and post: "(\<forall>i'>i. th' \<in> threads (moment i' t @ s))" by (auto) - interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales) - interpret h_i': red_extend_highest_gen _ _ _ _ _ "(Suc i)" by (unfold_locales) - from lt_its have "Suc i \<le> length t" by auto - -- {* Let us also suppose the event which makes this change is @{text e}: *} - from moment_head[OF this] obtain e where - eq_me: "moment (Suc i) t = e # moment i t" by blast - hence "vt (e # (moment i t @ s))" by (metis append_Cons h_i'.vt_t) - hence "PIP (moment i t @ s) e" by (cases, simp) - -- {* It can be derived that this event @{text "e"}, which - gives birth to @{term "th'"} must be a @{term "Create"}: *} - from create_pre[OF this, of th'] - obtain prio where eq_e: "e = Create th' prio" - by (metis append_Cons eq_me lessI post pre) - have h1: "th' \<in> threads (moment (Suc i) t @ s)" using post by auto - have h2: "cntP (moment (Suc i) t @ s) th' = cntV (moment (Suc i) t@ s) th'" - proof - - have "cntP (moment i t@s) th' = cntV (moment i t@s) th'" - by (metis h_i.cnp_cnv_eq pre) - thus ?thesis by (simp add:eq_me eq_e cntP_def cntV_def count_def) - qed - show ?thesis - using moment_blocked_eqpv [OF neq_th' h1 h2, of "length t"] lt_its moment_ge - by auto - qed - with `th' \<in> runing (t@s)` - have False by simp - } thus ?thesis by auto -qed - -text {* - The second lemma says, if the running thread @{text th'} is different from - @{term th}, then this @{text th'} must in the possession of some resources - at the very beginning. - - To ease the reasoning of resource possession of one particular thread, - we used two auxiliary functions @{term cntV} and @{term cntP}, - which are the counters of @{term P}-operations and - @{term V}-operations respectively. - If the number of @{term V}-operation is less than the number of - @{term "P"}-operations, the thread must have some unreleased resource. -*} - -lemma runing_inversion_1: (* ddd *) - assumes neq_th': "th' \<noteq> th" - and runing': "th' \<in> runing (t@s)" - -- {* thread @{term "th'"} is a live on in state @{term "s"} and - it has some unreleased resource. *} - shows "th' \<in> threads s \<and> cntV s th' < cntP s th'" -proof - - -- {* The proof is a simple composition of @{thm runing_inversion_0} and - @{thm runing_precond}: *} - -- {* By applying @{thm runing_inversion_0} to assumptions, - it can be shown that @{term th'} is live in state @{term s}: *} - have "th' \<in> threads s" using runing_inversion_0[OF assms(1,2)] . - -- {* Then the thesis is derived easily by applying @{thm runing_precond}: *} - with runing_precond [OF this neq_th' runing'] show ?thesis by simp -qed - -text {* - The following lemma is just a rephrasing of @{thm runing_inversion_1}: -*} -lemma runing_inversion_2: - assumes runing': "th' \<in> runing (t@s)" - shows "th' = th \<or> (th' \<noteq> th \<and> th' \<in> threads s \<and> cntV s th' < cntP s th')" -proof - - from runing_inversion_1[OF _ runing'] - show ?thesis by auto -qed - -lemma runing_inversion_3: - assumes runing': "th' \<in> runing (t@s)" - and neq_th: "th' \<noteq> th" - shows "th' \<in> threads s \<and> (cntV s th' < cntP s th' \<and> cp (t@s) th' = preced th s)" - by (metis neq_th runing' runing_inversion_2 runing_preced_inversion) - -lemma runing_inversion_4: - assumes runing': "th' \<in> runing (t@s)" - and neq_th: "th' \<noteq> th" - shows "th' \<in> threads s" - and "\<not>detached s th'" - and "cp (t@s) th' = preced th s" - apply (metis neq_th runing' runing_inversion_2) - apply (metis neq_th pv_blocked runing' runing_inversion_2 runing_precond_pre_dtc) - by (metis neq_th runing' runing_inversion_3) - - -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 *) - assumes "th \<notin> runing (t@s)" - obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" - "th' \<in> 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 \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (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 \<notin> 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' \<in> readys (t@s)" - and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto - -- {* We are going to show that this @{term th'} is running. *} - have "th' \<in> 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) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th'))" - by (unfold cp_alt_def1, simp) - also have "... = (the_preced (t @ s) \<circ> 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') \<subseteq> Th ` threads (t @ s)" - by (metis Range.intros dp trancl_range vat_t.range_in vat_t.subtree_tRAG_thread) - next - show "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp - by (unfold tRAG_subtree_eq, auto simp:subtree_def) - next - show "Max ((the_preced (t @ s) \<circ> the_thread) ` Th ` threads (t @ s)) = - (the_preced (t @ s) \<circ> 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' \<in> 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' \<in> ancestors (RAG (t @ s)) (Th th)" - using `(Th th, Th th') \<in> (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) \<noteq> {}" -proof(cases "th \<in> runing (t@s)") - case True thus ?thesis by auto -next - case False - thus ?thesis using th_blockedE by auto + with cp_gen_def_cond[OF refl[of "Th th''"]] + show ?thesis by metis qed end + +section {* The @{term Create} operation *} + +locale step_create_cps = + fixes s' th prio s + defines s_def : "s \<equiv> (Create th prio#s')" + assumes vt_s: "vt s" + +sublocale step_create_cps < vat_s: valid_trace "s" + by (unfold_locales, insert vt_s, simp) + +sublocale step_create_cps < vat_s': valid_trace "s'" + by (unfold_locales, insert step_back_vt[OF vt_s[unfolded s_def]], simp) + +context step_create_cps +begin + +lemma RAG_kept: "RAG s = RAG s'" + by (unfold s_def RAG_create_unchanged, auto) + +lemma tRAG_kept: "tRAG s = tRAG s'" + by (unfold tRAG_alt_def RAG_kept, auto) + +lemma preced_kept: + assumes "th' \<noteq> th" + shows "the_preced s th' = the_preced s' th'" + by (unfold s_def the_preced_def preced_def, insert assms, auto) + +lemma th_not_in: "Th th \<notin> Field (tRAG s')" +proof - + from vt_s[unfolded s_def] + have "PIP s' (Create th prio)" by (cases, simp) + hence "th \<notin> threads s'" by(cases, simp) + from vat_s'.not_in_thread_isolated[OF this] + have "Th th \<notin> Field (RAG s')" . + with tRAG_Field show ?thesis by auto +qed + +lemma eq_cp: + assumes neq_th: "th' \<noteq> th" + shows "cp s th' = cp s' th'" +proof - + have "(the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th') = + (the_preced s' \<circ> the_thread) ` subtree (tRAG s') (Th th')" + proof(unfold tRAG_kept, rule f_image_eq) + fix a + assume a_in: "a \<in> 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 \<noteq> th" + proof - + have "(Th th) \<notin> subtree (tRAG s') (Th th')" + proof + assume "Th th \<in> 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 s \<circ> the_thread) a = (the_preced s' \<circ> 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 s) (Th th) = {}" +proof - + { fix a + assume "a \<in> RTree.children (tRAG s) (Th th)" + hence "(a, Th th) \<in> tRAG 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 s th = preced th s" + by (unfold vat_s.cp_rec children_of_th, simp add:the_preced_def) + end +locale step_exit_cps = + fixes s' th prio s + defines s_def : "s \<equiv> Exit th # s'" + assumes vt_s: "vt s" +sublocale step_exit_cps < vat_s: valid_trace "s" + by (unfold_locales, insert vt_s, simp) +sublocale step_exit_cps < vat_s': valid_trace "s'" + by (unfold_locales, insert step_back_vt[OF vt_s[unfolded s_def]], simp) + +context step_exit_cps +begin + +lemma preced_kept: + assumes "th' \<noteq> th" + shows "the_preced s th' = the_preced s' th'" + by (unfold s_def the_preced_def preced_def, insert assms, auto) + +lemma RAG_kept: "RAG s = RAG s'" + by (unfold s_def RAG_exit_unchanged, auto) + +lemma tRAG_kept: "tRAG s = tRAG s'" + by (unfold tRAG_alt_def RAG_kept, auto) + +lemma th_ready: "th \<in> readys s'" +proof - + from vt_s[unfolded s_def] + have "PIP s' (Exit th)" by (cases, simp) + hence h: "th \<in> runing s' \<and> holdents s' th = {}" by (cases, metis) + thus ?thesis by (unfold runing_def, auto) +qed + +lemma th_holdents: "holdents s' th = {}" +proof - + from vt_s[unfolded s_def] + have "PIP s' (Exit th)" by (cases, simp) + thus ?thesis by (cases, metis) +qed + +lemma th_RAG: "Th th \<notin> Field (RAG s')" +proof - + have "Th th \<notin> Range (RAG s')" + proof + assume "Th th \<in> Range (RAG s')" + then obtain cs where "holding (wq s') th cs" + by (unfold Range_iff s_RAG_def, auto) + with th_holdents[unfolded holdents_def] + show False by (unfold eq_holding, auto) + qed + moreover have "Th th \<notin> Domain (RAG s')" + proof + assume "Th th \<in> Domain (RAG s')" + then obtain cs where "waiting (wq s') th cs" + by (unfold Domain_iff s_RAG_def, auto) + with th_ready show False by (unfold readys_def eq_waiting, auto) + qed + ultimately show ?thesis by (auto simp:Field_def) +qed + +lemma th_tRAG: "(Th th) \<notin> Field (tRAG s')" + using th_RAG tRAG_Field[of s'] by auto + +lemma eq_cp: + assumes neq_th: "th' \<noteq> th" + shows "cp s th' = cp s' th'" +proof - + have "(the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th') = + (the_preced s' \<circ> the_thread) ` subtree (tRAG s') (Th th')" + proof(unfold tRAG_kept, rule f_image_eq) + fix a + assume a_in: "a \<in> 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 \<noteq> th" + proof - + from vat_s'.readys_in_no_subtree[OF th_ready assms] + have "(Th th) \<notin> subtree (RAG s') (Th th')" . + with tRAG_subtree_RAG[of s' "Th th'"] + have "(Th th) \<notin> 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 s \<circ> the_thread) a = (the_preced s' \<circ> the_thread) a" + by (unfold eq_a, simp) + qed + thus ?thesis by (unfold cp_alt_def1, simp) +qed + +end + +end +