pip: comparison Implementation.thy

equal deleted inserted replaced

-:abe117821c32
+:da27bece9575
 theory Implementation
 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
 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. *}
+system operations, each explained in a separate section. To understand the relevant
+materials, one needs some acquaintance with locales, which are
-text {*
+used to as contexts for lemmas to situate, where lemmas with the same assumptions
-The following two lemmas are general about any valid system state,
+are grouped under the same locale.
-but are used in the derivation in more specific system operations.
-*}
+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_trace
 begin
-lemma readys_root:
+text {*
-assumes "th \<in> readys s"
+To minimize the cost of the recalculation, we derived the following localized alternative
-shows "root (RAG s) (Th th)"
+definition of @{term cp}:
-unfolding root_def ancestors_def
+*}
-using readys_RAG assms
-by (metis Collect_empty_eq Domain.DomainI trancl_domain)
+lemma cp_rec_tG:
+"cp s th = Max (preceds {th} s \<union> cprecs (children (tG s) th) s)"
-lemma readys_in_no_subtree:
+proof -
-assumes "th \<in> readys s"
+have [simp]: "(cp s \<circ> the_thread \<circ> Th) = cp s" by (rule ext, simp)
-and "th' \<noteq> th"
+have [simp]: "(cp s \<circ> the_thread) ` children (tRAG s) (Th th) =
-shows "Th th \<notin> subtree (RAG s) (Th th')"
+cp s ` children (tG s) th"
-proof
+apply (unfold tRAG_def_tG)
-assume "Th th \<in> subtree (RAG s) (Th th')"
+apply (subst fmap_children)
-thus False
+apply (rule injI, simp)
-proof(cases rule:subtreeE)
+by (unfold image_comp, simp)
-case 1
+have [simp]: "preceds {th} s = {the_preced s th}"
-with assms show ?thesis by auto
+by (unfold the_preced_def, simp)
-next
+show ?thesis
-case 2
+by (unfold cp_rec cprecs_def, simp add:the_preced_def)
-with readys_root[OF assms(1)]
+qed
-show ?thesis by (auto simp:root_def)
-qed
+text {*
-qed
+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
 section {* The @{term Set} operation *}
 using assms
 by (unfold the_preced_def, intro eq_preced, simp)
 text {* (* ddd *)
-Th following lemma @{text "eq_cp_pre"} says that the priority change of @{text "th"}
+According to @{thm RAG_es}, the @{text RAG} is not changed by @{text Set}-operation.
-only affects those threads, which as @{text "Th th"} in their sub-trees.
+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 proof of this lemma is simplified by using the alternative definition
+the subtree, which means the @{text cp}-value of the root thread is not changed.
-of @{text "cp"}.
+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'"
 qed
 thus ?thesis by (simp add:cp_alt_def)
 qed
 text {*
-The following lemma shows that @{term "th"} is not in the
+However, the following lemma shows that @{term "th"} is not in the
-sub-tree of any other thread.
+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 blast
 qed
 text {*
-By combining @{thm "eq_cp_pre"} and @{thm "th_in_no_subtree"},
+Combining the above two lemmas, it is concluded that the
-it is obvious that the change of priority only affects the @{text "cp"}-value
+recalculation of @{text "cp"}-value is needed only on @{text th}.
-of the initiating thread @{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.
+*}
 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]
 show ?thesis
 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) \<in> RAG s"
 proof -
 from holding_th_cs_s
 show ?thesis
 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 -
 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 simp
 qed
-end
+text {*
+As already said, all operations except @{text Set} may change precedence.
-text {*
+The following lemma confirms this fact of the @{text V}-operation:
-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'"}
+lemma
-to take over the critical resource released by the initiating thread @{text "th"}.
-*}
-lemma (in valid_trace_v)
 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)
 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)} \<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 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)}) \<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)
 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 subtree_insert_next)
+proof(rule subset_insert_subtree_outside)
-show "Th taker \<notin> subtree (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th th1)"
+show "Range {(Cs cs, Th taker)} \<inter>
-proof(rule subtree_refute)
+subtree (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th th1) = {}"
-show "Th th1 \<notin> ancestors (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th taker)"
+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)
 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 \<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)
 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 \<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) = {}"
 qed
 thus ?thesis by auto
 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 \<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> ?R"
 hence "n \<in> ?L" by (auto simp:subtree_def)
 } 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)
 from edge_of_th
 show "(Cs cs, Th th) \<in> edges_in (RAG s) (Th th)"
 lemma 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:
 shows "cp (e#s) th' = cp s th'"
 using cp_kept_1 cp_kept_2
 by (cases "th' = th", auto)
 end
+section {* The @{term P} operation *}
-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' \<noteq> th"
 shows "Th th \<notin> subtree (RAG s) (Th th')"
 proof
 assume "Th th \<in> subtree (RAG s) (Th th')"
 case 2
 with root_th show ?thesis by (auto simp:root_def)
 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'
 show "the_preced (e # s) th' = the_preced s th'"
 by (unfold the_preced_def is_p preced_def, simp)
 qed
 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' \<noteq> th"
 shows "subtree (RAG (e#s)) (Th th') = subtree (RAG s) (Th th')"
 proof(unfold RAG_es, rule subtree_insert_next)
 from in_no_others_subtree[OF assms]
 show "Th th \<notin> 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' \<noteq> th"
 shows "cp (e#s) th' = cp s th'"
 proof -
 have "(the_preced (e#s) ` {th'a. Th th'a \<in> subtree (RAG (e#s)) (Th th')}) =
 thus ?thesis by (unfold cp_alt_def, simp)
 qed
 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
 lemma cs_held: "(Cs cs, Th holder) \<in> RAG s"
 using holding_s_holder
 lemma tRAG_s:
 "tRAG (e#s) = tRAG s \<union> {(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'' \<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'')"
 from this[folded tRAG_s] show ?thesis .
 qed
 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 \<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"
 by (fold cp_gen_rec[OF eq_x], simp)
 finally show ?thesis .
 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') \<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''"
 show ?thesis by metis
 qed
 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 \<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 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' \<noteq> 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 \<notin> Field (tRAG s)"
+text {*
-by (meson not_in_thread_isolated subsetCE tRAG_Field th_not_live_s)
+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) \<circ> the_thread) ` subtree (tRAG (e#s)) (Th th') =
+have "(the_preced (e # s) ` subtree (tG (e # s)) th') =
-(the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th')"
+(the_preced s ` subtree (tG s) th')"
-proof(unfold tRAG_kept, rule f_image_eq)
+proof -
-fix a
+{ fix a
-assume a_in: "a \<in> subtree (tRAG s) (Th th')"
+assume "a \<in> subtree (tG s) th'"
-then obtain th_a where eq_a: "a = Th th_a"
+with th_not_in_tG have "a \<noteq> th"
-proof(cases rule:subtreeE)
+by (metis ancestors_Field dm_tG_threads neq_th subtree_ancestorsI th_not_live_s)
-case 2
+from preced_kept[OF this]
-from ancestors_Field[OF 2(2)]
+have "the_preced (e # s) a = the_preced s a" .
-and that show ?thesis by (unfold tRAG_alt_def, auto)
+}
-qed auto
+thus ?thesis by (unfold tG_kept, auto intro!:f_image_eq)
-have neq_th_a: "th_a \<noteq> th"
+qed
-proof -
+thus ?thesis by (unfold cp_alt_def2, simp)
-have "(Th th) \<notin> subtree (tRAG s) (Th th')"
+qed
-proof
-assume "Th th \<in> subtree (tRAG s) (Th th')"
+text {*
-thus False
+The following two lemmas deal with the @{text cp}-calculation of @{text th}.
-proof(cases rule:subtreeE)
+The first lemma @{text children_of_th} says @{text th} has no children.
-case 2
+The reason is simple, @{text th} is isolated from @{text "RAG"} before the
-from ancestors_Field[OF this(2)]
+@{term Create}-operation and @{text Create} does not change @{text RAG}, so
-and th_not_in[unfolded Field_def]
+@{text th} keeps isolated after the operation.
-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) \<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 (e#s)) (Th th) = {}"
 proof -
 { fix a
 assume "a \<in> RTree.children (tRAG (e#s)) (Th th)"
 with th_not_in have False
 by (unfold Field_def tRAG_kept, auto)
 } 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' \<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_kept, simp)
 lemma th_RAG: "Th th \<notin> Field (RAG s)"
 proof -
 have "Th th \<notin> Range (RAG s)"
 proof
 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)
 qed
 lemma th_tRAG: "(Th th) \<notin> 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 \<notin> 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' \<noteq> th"
 shows "cp (e#s) th' = cp s th'"
 proof -
-have "(the_preced (e#s) \<circ> the_thread) ` subtree (tRAG (e#s)) (Th th') =
+have "(the_preced (e # s) ` subtree (tG (e # s)) th') =
-(the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th')"
+(the_preced s ` subtree (tG s) th')"
-proof(unfold tRAG_kept, rule f_image_eq)
+proof -
-fix a
+{ fix a
-assume a_in: "a \<in> subtree (tRAG s) (Th th')"
+assume "a \<in> subtree (tG s) th'"
-then obtain th_a where eq_a: "a = Th th_a"
+with th_not_in_tG have "a \<noteq> th"
-proof(cases rule:subtreeE)
+by (metis ex_in_conv neq_th root_def root_readys_tG subtree_ancestorsI th_ready_s)
-case 2
+from preced_kept[OF this]
-from ancestors_Field[OF 2(2)]
+have "the_preced (e # s) a = the_preced s a" .
-and that show ?thesis by (unfold tRAG_alt_def, auto)
+}
-qed auto
+thus ?thesis by (unfold tG_kept, auto intro!:f_image_eq)
-have neq_th_a: "th_a \<noteq> th"
+qed
-proof -
+thus ?thesis by (unfold cp_alt_def2, simp)
-from readys_in_no_subtree[OF th_ready_s 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 (e#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

changeset 178	da27bece9575
parent 136	fb3f52fe99d1
child 179	f9e6c4166476