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. 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_trace
begin
text {*
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
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
section {* The @{term Set} operation *}
context valid_trace_set
begin
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)
qed
lemma 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)
qed
text {*
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 blast
qed
text {*
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 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
text {*
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)
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)
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)
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) = {}"
proof -
have "(Th th) \<notin> subtree (RAG s) (Th th1)"
proof(rule subtree_refute)
show "Th th1 \<notin> ancestors (RAG s) (Th th)"
by (unfold ancestors_th, simp)
next
from assms show "Th th1 \<noteq> Th th" by simp
qed
thus ?thesis by auto
qed
qed
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> ?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 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)"
by (unfold edges_in_def, auto simp:subtree_def)
qed
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 *}
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')"
thus False
proof(cases rule:subtreeE)
case 1
with assms show ?thesis by auto
next
case 2
with root_th show ?thesis by (auto simp:root_def)
qed
qed
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')}) =
(the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')})"
by (unfold preced_kept subtree_kept[OF assms], simp)
thus ?thesis by (unfold cp_alt_def, simp)
qed
end
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
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] .
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)
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"
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 .
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''"
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 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 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)
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)
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
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 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 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)
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) ` 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
end