theory Implementationimports PIPBasicsbegin(* The use of dependants has been abandoned. Through a series of lemma named xxx_alt_def, lemma originally expressed using dependants is now expressed in terms of RAG, tRAG and tG.*) text {* This file contains lemmas used to guide the recalculation of current precedence after every step of execution (or system operation, or event), which is the most tricky part in the implementation of PIP. Following convention, lemmas are grouped into locales corresponding to system operations, each explained in a separate section. To understand the relevant materials, one needs some acquaintance with locales, which are used to as contexts for lemmas to situate, where lemmas with the same assumptions are grouped under the same locale. Locale @{text "valid_trace s"} assumes that @{text "s"} is a valid trace (or state) of PIP. Lemmas talking about general properties of valid states can be put under this locale. The locale @{text "valid_trace_e s e"} is an extension of @{text valid_trace} by introducing an event @{text e} and assuming @{text "e#s"} is also valid state. The purpose of @{text valid_trace_e} is to set a context to investigate one step execution of PIP, where @{text e} is a fixed but arbitrary action legitimate to happen under state @{text "s"}. General Properties about one step action of PIP are grouped under this locale. @{text "valid_trace_e"} is further extended to accommodate specific actions. For example, @{text "valid_trace_create s e th prio"} further assumes that the @{text "e"} action is @{text "Create th prio"}, and @{text "valid_trace_p s e th cs"} assumes that @{text "e"} is @{text "P th cs"}, etc. Since the recalculation of current precedence happens only when certain actions are taken, it is natural to put the lemmas about recalculation under the respective locales. In the following, each section corresponds one particular action of PIP, which, in turn, is developed under the locale corresponding to the specific action. By @{text cp_alt_def3}, the @{text cp}-value of one thread @{text th} is determined uniquely by static precedences of threads in its @{text "RAG"}-subtree (or @{text tRAG}-subtree, @{text "tG"}-subtree). Because of this, the decision where recalculation is needed is based on the change of @{text RAG} (@{text tRAG} or @{text tG}) as well the precedence of threads. Since most of PIP actions (except the @{text Set}-operation) only changes the formation of @{text RAG}, therefore, for non-@{text Set} operations, if the change of @{text RAG} does not affect the subtree of one thread, its @{text cp}-value may not change. In the following, the section corresponding to non-@{text Set} operations usually contain lemmas showing the subtrees of certain kind of threads are not changed. The proof of such lemmas is obvious based on the lemmas about the change of @{text RAG}, which have already been derived in theory @{text PIPBasics} all under the name @{text "RAG_es"} in the locale corresponding to different PIP operations.*}section {* The local recalculation principle for @{text cp}-value *}definition "cprecs Ths s = cp s ` Ths"context valid_tracebegintext {* To minimize the cost of the recalculation, we derived the following localized alternative definition of @{term cp}:*}lemma cp_rec_tG: "cp s th = Max (preceds {th} s \<union> cprecs (children (tG s) th) s)"proof - have [simp]: "(cp s \<circ> the_thread \<circ> Th) = cp s" by (rule ext, simp) have [simp]: "(cp s \<circ> the_thread) ` children (tRAG s) (Th th) = cp s ` children (tG s) th" apply (unfold tRAG_def_tG) apply (subst fmap_children) apply (rule injI, simp) by (unfold image_comp, simp) have [simp]: "preceds {th} s = {the_preced s th}" by (unfold the_preced_def, simp) show ?thesis unfolding cprecs_def apply(subst cp_rec) apply(simp add: the_preced_def) doneqed text {* According to this lemma, @{text cp}-value of one thread can be calculated by calling recursively the @{text cp} function on its @{text tG}-children. However, one thing to be noted is that the lemma also means the recursive call needs not to descend into lower levels if the @{text "cp"}-value of one child is not changed. In this way, the recalculation can be {\em localized} to those thread with changed @{text cp}-value. This is the reason why this lemma is called a {\em localized lemma}.*}endsection {* The @{term Set} operation *}context valid_trace_setbeginfind_theorems RAG "(e#s)" "_ = _"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' \<noteq> th" shows "preced th' (e#s) = preced th' s"proof - from assms show ?thesis by (unfold is_set, auto simp:preced_def)qedlemma eq_the_preced: assumes "th' \<noteq> th" shows "the_preced (e#s) th' = the_preced s th'" using assms by (unfold the_preced_def, intro eq_preced, simp)text {* (* ddd *) According to @{thm RAG_es}, the @{text RAG} is not changed by @{text Set}-operation. Moreover, because @{text th} is the only thread with precedence changed by @{text Set}, for any subtree, if it does not contain @{text th}, there will be no precedence change inside the subtree, which means the @{text cp}-value of the root thread is not changed. This means that the @{text "cp"}-value of one thread needs to be recalculated only when the subtree rooted by the threads contains @{text "th"}. This argument is encapsulated in the following lemma:*}lemma eq_cp_pre: assumes nd: "Th th \<notin> 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 \<in> subtree (RAG (e#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 RAG_es 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 (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)qedtext {* However, the following lemma shows that @{term "th"} is not in the subtree of any thread except itself. *}lemma th_in_no_subtree: assumes "th' \<noteq> th" shows "Th th \<notin> subtree (RAG s) (Th th')"proof - from readys_in_no_subtree[OF th_ready_s assms(1)] show ?thesis by blastqedtext {* Combining the above two lemmas, it is concluded that the recalculation of @{text "cp"}-value is needed only on @{text th}.*}lemma eq_cp: assumes "th' \<noteq> th" shows "cp (e#s) th' = cp s th'" by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]])text {* Under the local recalculation principle @{thm cp_rec_tG}, @{thm eq_cp} also means the recalculation of @{text cp} for @{text th} can be done locally by inspecting only @{text th} and its children.*}endsection {* The @{term V} operation *}text {* The following locale @{text "valid_trace_v"} is the locale for @{text "V"}-operation in general. The recalculation of @{text cp}-value needs to consider two more sub-case, each encapsulated into a sub-locale of @{text "valid_trace_v"}. But first, some general properties about the @{text V}-operation are derived:*}context valid_trace_vbegintext {* Because @{text th} is running in state @{text s}, it does not in waiting of any resource, therefore, it has no ancestor in @{text "RAG s"}:*}lemma ancestors_th: "ancestors (RAG s) (Th th) = {}"proof - from readys_root[OF th_ready_s] show ?thesis by (unfold root_def, simp)qedtext {* Since @{text th} is holding @{text cs} (the resource to be released by this @{text V}-operation), the edge @{text "(Cs cs, Th th)"} represents this fact.*}lemma edge_of_th: "(Cs cs, Th th) \<in> RAG s" proof - from holding_th_cs_s show ?thesis by (unfold s_RAG_def s_holding_abv, auto)qedtext {* Since @{text cs} is held by @{text th} which has no ancestors, @{text th} is the only ancestor of @{text cs}:*}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}" by (rule forest_RAG.ancestors_accum[OF edge_of_th]) from this[unfolded ancestors_th] show ?thesis by simpqedtext {* As already said, all operations except @{text Set} may change precedence. The following lemma confirms this fact of the @{text V}-operation:*}lemma the_preced_es: "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 preced_def is_v, simp)qedendtext {* The following sub-locale @{text "valid_trace_v_n"} deals with one of the sub-cases of @{text V}, which corresponds to the situation where there is another thread @{text "taker"} to take over the release resource @{text cs}.*}context valid_trace_v_nbegintext {* The following lemma shows the two edges in @{text "RAG s"} which links @{text cs} with @{text taker} and @{text th} to form a chain. The existence of this chain set the stage for the @{text V}-operation in question to happen.*}lemma sub_RAGs': "{(Cs cs, Th th), (Th taker, Cs cs)} \<subseteq> RAG s" using waiting_taker holding_th_cs_s by (unfold s_RAG_def, fold s_waiting_abv s_holding_abv, auto)text {* The following lemma shows that @{text taker} has only two the ancestors. The reason for this is very simple: The chain starting from @{text taker} stops at @{text th}, which, as shown by @{thm ancestors_th}, has no ancestor. *}lemma ancestors_th': "ancestors (RAG s) (Th taker) = {Th th, Cs cs}" proof - have "ancestors (RAG s) (Th taker) = ancestors (RAG s) (Cs cs) \<union> {Cs cs}" proof(rule forest_RAG.ancestors_accum) from sub_RAGs' show "(Th taker, Cs cs) \<in> RAG s" by auto qed thus ?thesis using ancestors_th ancestors_cs by autoqedtext {* By composing several existing results, the following lemma make clear the change of @{text RAG} where there is a @{text taker} to take over the resource @{text cs}. More specifically, the lemma says the change of @{text RAG} is by first removing the chain linking @{text taker}, @{text cs} and @{text th} and then adding in one edge from @{text cs} to @{text taker}. The added edge represents acquisition of @{text cs} by @{text taker}.*}lemma RAG_s: "RAG (e#s) = (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) \<union> {(Cs cs, Th taker)}" by (unfold RAG_es waiting_set_eq holding_set_eq, auto)text {* The above lemma @{thm RAG_s} shows the effect of the @{text V}-operation on @{text RAG} is the removal of two edges followed by the addition of one edge. Based on this, the following lemma will show that the sub-trees of threads other than @{text th} and @{text taker} are unchanged. The intuition behind this is rather simple: the edges added and removed are not in these sub-trees. Formally, an edge is said to be outside of a sub-tree if its end point is. Note that when a set of edges are represented as a binary relation, the set of their end points is essentially range of the relation (formally defined as @{term Range}). Therefore, a set of edges (represented as a relation) are outside of a sub-tree if its @{text Range}-set does not intersect with the sub-tree.*}lemma subtree_kept: (* ddd *) assumes "th1 \<notin> {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' \<union> {(Cs cs, Th taker)}" -- {* The first step is to show the deletion of edges does not change the sub-tree *} have "subtree ?RAG' (Th th1) = ?R" proof(rule subset_del_subtree_outside) show "Range {(Cs cs, Th th), (Th taker, 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 -- {* The second step is to show the addition of edges does not change the sub-tree *} moreover have "subtree ?RAG'' (Th th1) = subtree ?RAG' (Th th1)" proof(rule subset_insert_subtree_outside) show "Range {(Cs cs, Th taker)} \<inter> subtree (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th th1) = {}" proof - have "Th taker \<notin> subtree (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th th1)" proof(rule subtree_refute) show "Th th1 \<notin> ancestors (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th taker)" (is "_ \<notin> ?R") proof - have "?R \<subseteq> ancestors (RAG s) (Th taker)" 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 taker" by simp qed thus ?thesis by auto qed qed ultimately show ?thesis by (unfold RAG_s, simp)qedtext {* The following lemma shows threads not involved in the @{text V}-operation (i.e. threads other than @{text th} and @{text taker}) do not need to do any @{text cp}-recalculation. The reason is simple: according to @{thm subtree_kept}, the sub-trees of such threads are not changed , additionally, since the @{text V}-operation does not change any precedence, the @{text "cp"}-value of such threads are not changed.*}lemma cp_kept: assumes "th1 \<notin> {th, taker}" shows "cp (e#s) th1 = cp s th1" by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp)text {* Lemma @{thm cp_kept} also means @{text cp}-recalculation is needed only for @{text th} and @{text taker}. The following lemmas are to ensure that the recalculation can done locally using {\em local recalculation principle}. Since @{text taker} and @{text th} are the only threads with changed @{text cp}-values and neither one can not be a child of the other, it can be concluded that neither of these two threads has children with changed @{text cp}-value. It means the recursive calls in @{thm cp_rec_tG} will not descend when recalculating the @{text cp}-values for @{text th} and @{text taker}.*}lemma "taker \<notin> children (tG (e#s)) th" by (metis children_subtree empty_iff in_mono neq_taker_th root_def set_mp subtree_ancestorsI taker_ready_es vat_es.root_readys_tG)lemma "th \<notin> children (tG (e#s)) taker" by (metis children_subtree empty_iff neq_taker_th root_def subsetD subtree_ancestorsI th_ready_es vat_es.root_readys_tG)endtext {* The following locale @{text valid_trace_v_e} deals with the second sub-case of @{text V}-operation, where there is no thread to take over the release resource @{text cs}.*}context valid_trace_v_ebegintext {* Since no thread to take over @{text cs}, only the edge representing the holding of @{text cs} by @{text th} needs to be removed:*}lemma RAG_s: "RAG (e#s) = RAG s - {(Cs cs, Th th)}" by (unfold RAG_es waiting_set_eq holding_set_eq, simp)text {* Since @{text th} has no ancestors, the removal of the holding edge only affects the sub-tree of @{text th}:*}lemma subtree_kept: assumes "th1 \<noteq> 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)} \<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 qedqedtext {* From lemma @{thm subtree_kept} and the fact that no precedence are changed, it can be derived the @{text cp}-values of all threads (except @{text th}) are not changed and therefore need no recalculation:*}lemma cp_kept_1: assumes "th1 \<noteq> th" shows "cp (e#s) th1 = cp s th1" by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp)text {* The next several lemmas try to show that even the @{text cp}-value of @{text th} needs not be recalculated. Although the @{text V}-operation detaches the sub-tree of @{text cs} from the sub-tree of @{text th}, the @{text cp}-value of @{text th} is not affected. The reason is given by the following lemma @{text subtree_cs}, which says that the sub-tree of @{text cs} contains only itself. According to @{text subtree_cs}, the detached sub-tree contains no thread node and therefore makes no contribution to the @{text cp}-value of @{text th}, so its removal does not affect the @{text cp}-value neither, as confirmed by the lemma @{text cp_kept_2}.*}lemma subtree_cs: "subtree (RAG s) (Cs cs) = {Cs cs}" (is "?L = ?R")proof - { fix n assume "n \<in> ?L" hence "n \<in> ?R" proof(cases rule:subtreeE) case 2 from this(2) have "(n, Cs cs) \<in> (RAG s)^+" by (auto simp:ancestors_def) from tranclD2[OF this] obtain th' where "waiting s th' cs" by (auto simp:s_RAG_def s_waiting_abv) with no_waiter_before show ?thesis by simp qed simp } moreover { fix n assume "n \<in> ?R" hence "n \<in> ?L" by (auto simp:subtree_def) } ultimately show ?thesis by autoqedtext {* The following @{text "subtree_th"} is just a technical lemma.*}lemma subtree_th: "subtree (RAG (e#s)) (Th th) = subtree (RAG s) (Th th) - {Cs cs}"proof(unfold RAG_s, fold subtree_cs, rule forest_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)qedlemma cp_kept_2: shows "cp (e#s) th = cp s th" by (unfold cp_alt_def subtree_th the_preced_es, auto)text {* By combining @{thm cp_kept_1} and @{thm cp_kept_2}, it is shown that no @{text cp}-recalculation is needed at all for this sub-case of @{text V}-operation.*}lemma eq_cp_pre: shows "cp (e#s) th' = cp s th'" using cp_kept_1 cp_kept_2 by (cases "th' = th", auto)lemma eq_cp: shows "cp (e#s) = cp s" by (rule ext, unfold eq_cp_pre, simp)endsection {* The @{term P} operation *} text {* Like @{text V}-operation, the treatment of @{text P}-operation is also divided into tow sub-cases. If the requested resource is available, it is dealt with in sub-locale @{text valid_trace_p_h}, otherwise, it is dealt with in sub-locale @{text valid_trace_p_w}. *}text {* But first, the following base locale @{text valid_trace_p} contains some general properties of the @{text P}-operation:*}context valid_trace_pbegintext {* The following lemma shows that @{text th} is a root in the @{text RAG} graph, which means @{text th} has no ancestors in the graph. The reason is that: since @{text th} is in running state, it is in ready state, which means it is not waiting for any resource, therefore, it has no outbound edge. *}lemma root_th: "root (RAG s) (Th th)" by (simp add: ready_th_s readys_root)text {* For the same reason as @{thm root_th}, @{text th} is not in the sub-tree of any thread other than @{text th}:*}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) qedqedtext {* The following lemma confirms that the @{text P}-operation does not affect the precedence of any thread. *}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)qedendtext {* The following locale @{text valid_trace_p_h} deals with the sub-case of @{text P}-operation when the requested @{text cs} is available and @{text th} gets hold of it instantaneously with the @{text P}-operation.*}context valid_trace_p_hbegintext {* It can be shown that the @{text tG} is not changed by the @{text P}-action. The reason is that the edge added to @{text RAG} by the @{text P}-action, namely @{text "(Cs cs, Th th)"}, does not bring any new thread into graph @{text tG}, because the node of @{text cs} is isolated from the original @{text RAG}.*}thm RAG_eslemma tG_es: "tG (e # s) = tG s"proof - have [simp]: "\<And> th1. (Th th1, Cs cs) \<notin> RAG s" by (metis in_RAG_E no_holder node.simps(4) the_cs.simps waiting_holding) show ?thesis apply (unfold tG_def_tRAG tRAG_alt_def RAG_es) by (auto)qedtext {* Since both @{text tG} and precedences are not changed, it is easy to show that all @{text cp}-value are not changed, therefore, no @{text cp}-recalculation is needed:*}lemma cp_kept: "cp (e#s) = cp s" by (rule ext, simp add: cp_alt_def2 preced_kept tG_es)endtext {* The following locale @{text valid_trace_p_w} corresponds to the case when the requested resource @{text cs} is not available and thread @{text th} is blocked.*}context valid_trace_p_wbeginlemma cs_held: "(Cs cs, Th holder) \<in> RAG s" using holding_s_holder by (unfold s_RAG_def, fold s_holding_abv, auto)lemma tRAG_s: "tRAG (e#s) = tRAG s \<union> {(Th th, Th holder)}" using RAG_tRAG_transfer[OF RAG_es cs_held] .lemma tG_ancestors_tRAG_refute: assumes "th'' \<notin> ancestors (tG (e#s)) th" shows "Th th'' \<notin> ancestors (tRAG (e#s)) (Th th)" using assms using node.inject(1) tRAG_ancestorsE_tG by force text {* The following lemma shows only the ancestors of @{text th} (the initiating thread of the @{text P}-operation) may possibly need a @{text cp}-recalculation. All other threads (including @{text th} itself) do not need @{text cp}-recalculation. *}lemma cp_kept: assumes "Th th'' \<notin> 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 \<notin> subtree (tRAG s) (Th th'')" proof assume "Th holder \<in> 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'' \<in> ancestors (tRAG s) (Th holder)" moreover have "... \<subseteq> ancestors (tRAG (e#s)) (Th holder)" proof(rule ancestors_mono) show "tRAG s \<subseteq> tRAG (e#s)" by (unfold tRAG_s, auto) qed ultimately have "Th th'' \<in> ancestors (tRAG (e#s)) (Th holder)" by auto moreover have "Th holder \<in> ancestors (tRAG (e#s)) (Th th)" by (unfold tRAG_s, auto simp:ancestors_def) ultimately have "Th th'' \<in> 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 \<union> {(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)qedlemma cp_kept_tG: (* aaa *) assumes "th'' \<notin> ancestors (tG (e#s)) th" shows "cp (e#s) th'' = cp s th''" using cp_kept tG_ancestors_tRAG_refute assms by blasttext {* Lemma @{thm cp_kept} means that the @{text cp}-recalculation starts from the parent of @{text th}, going upwards along the chain of ancestors until one root (which is a thread in ready queue) is reached. Actually, recalculation can terminate earlier, as confirmed by the following two lemmas. The first lemma @{text cp_gen_update_stop} is a technical lemma used to prove the lemma that follows.*}lemma cp_gen_update_stop: (* ddd *) assumes "u \<in> ancestors (tRAG (e#s)) (Th th)" and "cp_gen (e#s) u = cp_gen s u" and "y \<in> 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} \<union> cp_gen (e#s) ` RTree.children (tRAG (e#s)) x)" . also have "... = Max ({the_preced s th2} \<union> 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) \<in> tRAG (e#s)" by (unfold tRAG_s, auto) note x_u = 1(2) show "x \<notin> Range {(Th th, Th holder)}" proof assume "x \<in> Range {(Th th, Th holder)}" hence eq_x: "x = Th holder" using RangeE by auto show False find_theorems ancestors tRAG proof(cases rule:vat_es.forest_s.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) \<in> (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 \<in> ?A" from 1(2) show "?f a = ?g a" proof(cases rule:vat_es.forest_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 (e#s)) (Th th)" proof assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)" have "a = u" proof(rule vat_es.forest_s.ancestors_children_unique) from a_in' a_in show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter> RTree.children (tRAG (e#s)) x" by auto next from assms(1) in_ch show "u \<in> ancestors (tRAG (e#s)) (Th th) \<inter> 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 \<in> ancestors (tRAG (e#s)) u" "z \<in> RTree.children (tRAG (e#s)) x" by auto show ?thesis proof(cases "a = z") case True from h(2) have zx_in: "(z, x) \<in> (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 \<notin> ancestors (tRAG (e#s)) (Th th)" proof assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)" have "a = z" proof(rule vat_es.forest_s.ancestors_children_unique) from assms(1) h(1) have "z \<in> ancestors (tRAG (e#s)) (Th th)" by (auto simp:ancestors_def) with h(2) show " z \<in> ancestors (tRAG (e#s)) (Th th) \<inter> RTree.children (tRAG (e#s)) x" by auto next from a_in a_in' show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter> 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 . qedqedtext {* The following lemma is about the possible early termination of @{text cp}-recalculation. The lemma says that @{text cp}-recalculation can terminate as soon as the recalculation yields an unchanged @{text cp}-value. The @{text th'} in the lemma is assumed to be the first ancestor of @{text th} encountered by the recalculation procedure which has an unchanged @{text cp}-value and the @{text th''} represents any thread upstream of @{text th'}. The lemma shows that the @{text "cp"}-value @{text "th''"} is not changed, therefore, needs no recalculation. It means the recalculation can be stop at @{text "th'"}.*}lemma cp_up: assumes "(Th th') \<in> ancestors (tRAG (e#s)) (Th th)" and "cp (e#s) th' = cp s th'" and "(Th th'') \<in> 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 metisqedlemma cp_up_tG: (* aaa *) assumes "th' \<in> ancestors (tG (e#s)) th" and "cp (e#s) th' = cp s th'" and "th'' \<in> ancestors (tG (e#s)) th'" shows "cp (e#s) th'' = cp s th''" using assms cp_up ancestors_tG_tRAG by blast endtext {* The following locale deals with the @{text Create}-operation.*}section {* The @{term Create} operation *}context valid_trace_createbegin text {* Since @{text Create}-operation does not change @{text RAG} (according to @{thm RAG_es}) and @{text tRAG} is determined uniquely by @{text RAG}, therefore, @{text tRAG} is not not changed by @{text Create} neither.*}lemma tRAG_kept: "tRAG (e#s) = tRAG s" by (unfold tRAG_alt_def RAG_es, auto)lemma tG_kept: "tG (e#s) = tG s" by (unfold tG_def_tRAG tRAG_kept, simp)text {* The following lemma shows that @{text th} is completely isolated from @{text RAG}.*}lemma th_not_in: "Th th \<notin> Field (tRAG s)" by (meson not_in_thread_isolated subsetCE tRAG_Field th_not_live_s)text {* Based on @{thm th_not_in}, it can be derived that @{text th} is also isolated from @{text RAG}.*}lemma th_not_in_tG: "th \<notin> Field (tG s)" using tG_threads th_not_live_s by blasttext {* The @{text Create}-operation does not change the precedences of other threads excepting sets a the initial precedence for the thread being created (i.e. @{text th}).*}lemma preced_kept: assumes "th' \<noteq> th" shows "the_preced (e#s) th' = the_preced s th'" by (unfold the_preced_def preced_def is_create, insert assms, auto)text {* The following lemma shows that the @{text cp}-values of all other threads need not be recalculated. The reason is twofold, first, since @{text tG} is not changed, sub-trees of these threads are not changed; second, the precedences of the threads in these sub-trees are not changed (because the only thread with a changed precedence is @{text th} and @{text th} is isolated from @{text tG}). *}lemma eq_cp: assumes neq_th: "th' \<noteq> th" shows "cp (e#s) th' = cp s th'"proof - have "(the_preced (e # s) ` subtree (tG (e # s)) th') = (the_preced s ` subtree (tG s) th')" proof - { fix a assume "a \<in> subtree (tG s) th'" with th_not_in_tG have "a \<noteq> th" by (metis ancestors_Field dm_tG_threads neq_th subtree_ancestorsI th_not_live_s) from preced_kept[OF this] have "the_preced (e # s) a = the_preced s a" . } thus ?thesis by (unfold tG_kept, auto intro!:f_image_eq) qed thus ?thesis by (unfold cp_alt_def2, simp)qedtext {* The following two lemmas deal with the @{text cp}-calculation of @{text th}. The first lemma @{text children_of_th} says @{text th} has no children. The reason is simple, @{text th} is isolated from @{text "RAG"} before the @{term Create}-operation and @{text Create} does not change @{text RAG}, so @{text th} keeps isolated after the operation.*}lemma children_of_th: "RTree.children (tRAG (e#s)) (Th th) = {}"proof - { fix a assume "a \<in> RTree.children (tRAG (e#s)) (Th th)" hence "(a, Th th) \<in> 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 autoqedtext {* Now, since @{term th} has no children, by definition its @{text cp} value equals its precedence:*}lemma eq_cp_th: "cp (e#s) th = preced th (e#s)" unfolding children_of_th apply(subst vat_es.cp_rec) apply(simp add:the_preced_def children_of_th) doneendtext {* The following locale @{text valid_trace_exit} deals with the @{term Exit}-operation.*}context valid_trace_exitbegintext {* The treatment of @{text Exit} is very similar to @{text Create}. First, the precedences of threads other than @{text th} are not changed.*}lemma preced_kept: assumes "th' \<noteq> th" shows "the_preced (e#s) th' = the_preced s th'" using assms by (unfold the_preced_def is_exit preced_def, simp)text {* Second, @{term tRAG} is not changed by @{text Exit} either.*}lemma tRAG_kept: "tRAG (e#s) = tRAG s" by (unfold tRAG_alt_def RAG_es, auto)text {* Since @{term tG} is defined in terms of @{term tRAG}, @{term tG} is not changed neither.*}lemma tG_kept: "tG (e#s) = tG s" by (unfold tG_def_tRAG tRAG_kept, simp)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 s th cs" by (simp add: holdents_RAG holdents_th_s) then show False by (unfold s_holding_abv, auto) qed moreover have "Th th \<notin> Domain (RAG s)" proof assume "Th th \<in> Domain (RAG s)" then obtain cs where "waiting s th cs" by (simp add: readys_RAG) then show False using RAG_es \<open>Th th \<in> Domain (RAG s)\<close> th_not_live_es valid_trace.dm_RAG_threads vat_es.valid_trace_axioms by blast qed ultimately show ?thesis by (auto simp:Field_def)qedlemma th_tRAG: "(Th th) \<notin> Field (tRAG s)" using th_RAG tRAG_Field by autotext {* Based on @{thm th_RAG}, it can be derived that @{text th} is also isolated from @{text tG}.*}lemma th_not_in_tG: "th \<notin> Field (tG s)" using tG_kept vat_es.tG_threads by autotext {* Because of @{thm preced_kept}, @{thm tG_kept} and @{thm th_tRAG}, the @{text cp}-values of all other threads are not changed. The reasoning is almost the same as that of @{term Create}:*}lemma eq_cp: assumes neq_th: "th' \<noteq> th" shows "cp (e#s) th' = cp s th'"proof - have "(the_preced (e # s) ` subtree (tG (e # s)) th') = (the_preced s ` subtree (tG s) th')" proof - { fix a assume "a \<in> subtree (tG s) th'" with th_not_in_tG have "a \<noteq> th" by (metis ex_in_conv neq_th root_def root_readys_tG subtree_ancestorsI th_ready_s) from preced_kept[OF this] have "the_preced (e # s) a = the_preced s a" . } thus ?thesis by (unfold tG_kept, auto intro!:f_image_eq) qed thus ?thesis by (unfold cp_alt_def2, simp)qedendend