--- 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 \<in> 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 \<in> readys s"
- and "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 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 \<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
+ 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' \<noteq> 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' \<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]
@@ -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) \<in> 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)} \<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 -
@@ -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)}) \<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) =
@@ -211,6 +328,7 @@
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) = {}"
@@ -218,7 +336,7 @@
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)
+ by (unfold ancestors_th, simp)
next
from assms show "Th th1 \<noteq> 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 \<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)"
+ 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 -
+ 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
+ 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)"
@@ -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 \<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 -
@@ -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' \<noteq> th"
shows "Th th \<notin> 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' \<noteq> th"
shows "subtree (RAG (e#s)) (Th th') = subtree (RAG s) (Th th')"
@@ -373,6 +603,14 @@
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'"
@@ -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 \<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''"
@@ -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 \<in> 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') \<in> 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 \<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)"
- 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' \<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') =
- (the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th')"
- proof(unfold tRAG_kept, rule f_image_eq)
- fix a
- assume a_in: "a \<in> subtree (tRAG s) (Th th')"
- then obtain th_a where eq_a: "a = Th th_a"
- proof(cases rule:subtreeE)
- case 2
- from ancestors_Field[OF 2(2)]
- and that show ?thesis by (unfold tRAG_alt_def, auto)
- qed auto
- have neq_th_a: "th_a \<noteq> th"
- proof -
- have "(Th th) \<notin> subtree (tRAG s) (Th th')"
- proof
- assume "Th th \<in> subtree (tRAG s) (Th th')"
- thus False
- proof(cases rule:subtreeE)
- case 2
- from ancestors_Field[OF this(2)]
- and th_not_in[unfolded Field_def]
- show ?thesis by auto
- qed (insert assms, auto)
- qed
- with a_in[unfolded eq_a] show ?thesis by auto
- qed
- from preced_kept[OF this]
- show "(the_preced (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)
+ 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)
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' \<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)"
@@ -677,37 +994,40 @@
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') =
- (the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th')"
- proof(unfold tRAG_kept, rule f_image_eq)
- fix a
- assume a_in: "a \<in> subtree (tRAG s) (Th th')"
- then obtain th_a where eq_a: "a = Th th_a"
- proof(cases rule:subtreeE)
- case 2
- from ancestors_Field[OF 2(2)]
- and that show ?thesis by (unfold tRAG_alt_def, auto)
- qed auto
- have neq_th_a: "th_a \<noteq> th"
- proof -
- from 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)
+ 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)
qed
end