diff -r abe117821c32 -r da27bece9575 Implementation.thy --- a/Implementation.thy Fri Jun 09 15:08:54 2017 +0100 +++ b/Implementation.thy Fri Jun 23 00:27:16 2017 +0100 @@ -2,6 +2,13 @@ imports PIPBasics begin + +(* + 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 @@ -9,39 +16,83 @@ 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. *} + 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. -text {* - The following two lemmas are general about any valid system state, - but are used in the derivation in more specific system operations. + 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_trace begin -lemma readys_root: - assumes "th \ readys s" - shows "root (RAG s) (Th th)" - unfolding root_def ancestors_def - using readys_RAG assms -by (metis Collect_empty_eq Domain.DomainI trancl_domain) +text {* + To minimize the cost of the recalculation, we derived the following localized alternative + definition of @{term cp}: +*} -lemma readys_in_no_subtree: - assumes "th \ readys s" - and "th' \ th" - shows "Th th \ subtree (RAG s) (Th th')" -proof - assume "Th th \ subtree (RAG s) (Th th')" - thus False - proof(cases rule:subtreeE) - case 1 - with assms show ?thesis by auto - next - case 2 - with readys_root[OF assms(1)] - show ?thesis by (auto simp:root_def) - qed -qed +lemma cp_rec_tG: + "cp s th = Max (preceds {th} s \ cprecs (children (tG s) th) s)" +proof - + have [simp]: "(cp s \ the_thread \ Th) = cp s" by (rule ext, simp) + have [simp]: "(cp s \ 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 + by (unfold cp_rec cprecs_def, simp add:the_preced_def) +qed + +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}. +*} end @@ -73,11 +124,14 @@ 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"}. + 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: @@ -110,8 +164,8 @@ qed text {* - The following lemma shows that @{term "th"} is not in the - sub-tree of any other thread. + 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' \ th" @@ -122,26 +176,39 @@ 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"}. + 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' \ 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. +*} + end section {* The @{term V} operation *} text {* - The following @{text "step_v_cps"} is the locale for @{text "V"}-operation. + 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_v begin +text {* + 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] @@ -149,6 +216,10 @@ by (unfold root_def, simp) qed +text {* + 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) \ RAG s" proof - @@ -157,6 +228,10 @@ by (unfold s_RAG_def s_holding_abv, auto) qed +text {* + 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 - @@ -165,15 +240,11 @@ from this[unfolded ancestors_th] show ?thesis by simp qed -end - text {* - The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, - which represents the case when there is another thread @{text "th'"} - to take over the critical resource released by the initiating thread @{text "th"}. + As already said, all operations except @{text Set} may change precedence. + The following lemma confirms this fact of the @{text V}-operation: *} - -lemma (in valid_trace_v) +lemma the_preced_es: "the_preced (e#s) = the_preced s" proof fix th' @@ -181,14 +252,35 @@ by (unfold the_preced_def preced_def is_v, simp) qed +end + + +text {* + 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_n begin +text {* + 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)} \ 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 - @@ -199,11 +291,36 @@ thus ?thesis using ancestors_th ancestors_cs by auto qed +text {* + 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)}) \ {(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 \ {th, taker}" shows "subtree (RAG (e#s)) (Th th1) = @@ -211,6 +328,7 @@ proof - let ?RAG' = "(RAG s - {(Cs cs, Th th), (Th taker, Cs cs)})" let ?RAG'' = "?RAG' \ {(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)} \ subtree (RAG s) (Th th1) = {}" @@ -218,7 +336,7 @@ have "(Th th) \ subtree (RAG s) (Th th1)" proof(rule subtree_refute) show "Th th1 \ ancestors (RAG s) (Th th)" - by (unfold ancestors_th, simp) + by (unfold ancestors_th, simp) next from assms show "Th th1 \ Th th" by simp qed @@ -231,38 +349,84 @@ 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 subtree_insert_next) - show "Th taker \ subtree (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th th1)" - proof(rule subtree_refute) - show "Th th1 \ ancestors (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th taker)" + proof(rule subset_insert_subtree_outside) + show "Range {(Cs cs, Th taker)} \ + subtree (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th th1) = {}" + proof - + have "Th taker \ subtree (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th th1)" + proof(rule subtree_refute) + show "Th th1 \ ancestors (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th taker)" (is "_ \ ?R") - proof - + proof - have "?R \ ancestors (RAG s) (Th taker)" by (rule ancestors_mono, auto) moreover have "Th th1 \ ..." using ancestors_th' assms by simp ultimately show ?thesis by auto - qed - next - from assms show "Th th1 \ Th taker" by simp + qed + next + from assms show "Th th1 \ Th taker" by simp + qed + thus ?thesis by auto qed qed ultimately show ?thesis by (unfold RAG_s, simp) qed +text {* + 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 \ {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 \ 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 \ 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) + + end - +text {* + 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_e begin +text {* + 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 \ th" shows "subtree (RAG (e#s)) (Th th1) = subtree (RAG s) (Th th1)" @@ -280,11 +444,31 @@ qed qed +text {* + 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 \ 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 - @@ -308,7 +492,9 @@ } ultimately show ?thesis by auto qed - +text {* + 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) @@ -321,6 +507,10 @@ 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: shows "cp (e#s) th' = cp s th'" using cp_kept_1 cp_kept_2 @@ -328,15 +518,37 @@ end +section {* The @{term P} operation *} -section {* 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_p begin +text {* + 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' \ th" shows "Th th \ subtree (RAG s) (Th th')" @@ -352,6 +564,10 @@ qed qed +text {* + 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' @@ -361,10 +577,24 @@ end +text {* + 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_h begin +text {* + According to @{thm RAG_es}, the only change to @{text RAG} by + the @{text P}-operation is the addition of the edge @{text "(Cs cs, Th th)"}, + representing the newly acquisition of @{text cs} by @{text th}. + The following lemma shows that this newly added edge only change the sub-tree + of @{text th}, the reason is that @{text th} is in no other sub-trees. +*} + lemma subtree_kept: assumes "th' \ th" shows "subtree (RAG (e#s)) (Th th') = subtree (RAG s) (Th th')" @@ -373,6 +603,14 @@ show "Th th \ subtree (RAG s) (Th th')" . qed +text {* + With both sub-tree and precdences unchanged, the @{text cp}-values of + threads other than @{text th} are not changed. Therefore, the + only recalculation of @{text cp}-value happens at @{text th}, and + the recalculation can be done locally using the + {\em local recalculation principle}, because the @{text cp}-values + of its children are not changed. +*} lemma cp_kept: assumes "th' \ th" shows "cp (e#s) th' = cp s th'" @@ -385,6 +623,12 @@ end +text {* + 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_w begin @@ -396,6 +640,12 @@ "tRAG (e#s) = tRAG s \ {(Th th, Th holder)}" using RAG_tRAG_transfer[OF RAG_es cs_held] . +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'' \ ancestors (tRAG (e#s)) (Th th)" shows "cp (e#s) th'' = cp s th''" @@ -431,6 +681,15 @@ show ?thesis by (unfold cp_alt_def1 h preced_kept, simp) qed +text {* + 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 \ ancestors (tRAG (e#s)) (Th th)" and "cp_gen (e#s) u = cp_gen s u" @@ -558,6 +817,17 @@ qed qed +text {* + 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') \ ancestors (tRAG (e#s)) (Th th)" and "cp (e#s) th' = cp s th'" @@ -575,59 +845,86 @@ end +text {* + The following locale deals with the @{text Create}-operation. +*} + section {* The @{term Create} operation *} context valid_trace_create begin +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_kept, simp) + +text {* + The following lemma shows that @{text th} is completely isolated + from @{text RAG}. +*} +lemma th_not_in: "Th th \ 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 \ Field (tG s)" + using tG_threads th_not_live_s by blast + + +text {* + 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' \ th" shows "the_preced (e#s) th' = the_preced s th'" by (unfold the_preced_def preced_def is_create, insert assms, auto) -lemma th_not_in: "Th th \ Field (tRAG s)" - by (meson not_in_thread_isolated subsetCE tRAG_Field th_not_live_s) - +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' \ th" shows "cp (e#s) th' = cp s th'" proof - - have "(the_preced (e#s) \ the_thread) ` subtree (tRAG (e#s)) (Th th') = - (the_preced s \ the_thread) ` subtree (tRAG s) (Th th')" - proof(unfold tRAG_kept, rule f_image_eq) - fix a - assume a_in: "a \ subtree (tRAG s) (Th th')" - then obtain th_a where eq_a: "a = Th th_a" - proof(cases rule:subtreeE) - case 2 - from ancestors_Field[OF 2(2)] - and that show ?thesis by (unfold tRAG_alt_def, auto) - qed auto - have neq_th_a: "th_a \ th" - proof - - have "(Th th) \ subtree (tRAG s) (Th th')" - proof - assume "Th th \ subtree (tRAG s) (Th th')" - thus False - proof(cases rule:subtreeE) - case 2 - from ancestors_Field[OF this(2)] - and th_not_in[unfolded Field_def] - show ?thesis by auto - qed (insert assms, auto) - qed - with a_in[unfolded eq_a] show ?thesis by auto - qed - from preced_kept[OF this] - show "(the_preced (e#s) \ the_thread) a = (the_preced s \ the_thread) a" - by (unfold eq_a, simp) - qed - thus ?thesis by (unfold cp_alt_def1, simp) + have "(the_preced (e # s) ` subtree (tG (e # s)) th') = + (the_preced s ` subtree (tG s) th')" + proof - + { fix a + assume "a \ subtree (tG s) th'" + with th_not_in_tG have "a \ 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) qed +text {* + 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 @@ -638,24 +935,44 @@ } thus ?thesis by auto qed +text {* + 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)" by (unfold vat_es.cp_rec children_of_th, simp add:the_preced_def) end - +text {* + The following locale @{text valid_trace_exit} deals with the @{term Exit}-operation. +*} context valid_trace_exit begin +text {* + 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' \ 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_kept, simp) + lemma th_RAG: "Th th \ Field (RAG s)" proof - have "Th th \ Range (RAG s)" @@ -677,37 +994,40 @@ ultimately show ?thesis by (auto simp:Field_def) qed + lemma th_tRAG: "(Th th) \ Field (tRAG s)" using th_RAG tRAG_Field by auto + +text {* + Based on @{thm th_RAG}, it can be derived that @{text th} is also + isolated from @{text tG}. +*} +lemma th_not_in_tG: "th \ Field (tG s)" + using tG_kept vat_es.tG_threads by auto + +text {* + 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' \ th" shows "cp (e#s) th' = cp s th'" proof - - have "(the_preced (e#s) \ the_thread) ` subtree (tRAG (e#s)) (Th th') = - (the_preced s \ the_thread) ` subtree (tRAG s) (Th th')" - proof(unfold tRAG_kept, rule f_image_eq) - fix a - assume a_in: "a \ subtree (tRAG s) (Th th')" - then obtain th_a where eq_a: "a = Th th_a" - proof(cases rule:subtreeE) - case 2 - from ancestors_Field[OF 2(2)] - and that show ?thesis by (unfold tRAG_alt_def, auto) - qed auto - have neq_th_a: "th_a \ th" - proof - - from readys_in_no_subtree[OF th_ready_s assms] - have "(Th th) \ subtree (RAG s) (Th th')" . - with tRAG_subtree_RAG[of s "Th th'"] - have "(Th th) \ subtree (tRAG s) (Th th')" by auto - with a_in[unfolded eq_a] show ?thesis by auto - qed - from preced_kept[OF this] - show "(the_preced (e#s) \ the_thread) a = (the_preced s \ the_thread) a" - by (unfold eq_a, simp) - qed - thus ?thesis by (unfold cp_alt_def1, simp) + have "(the_preced (e # s) ` subtree (tG (e # s)) th') = + (the_preced s ` subtree (tG s) th')" + proof - + { fix a + assume "a \ subtree (tG s) th'" + with th_not_in_tG have "a \ 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) qed end