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 +
−
    unfolding cprecs_def+
−
    apply(subst cp_rec)+
−
    apply(simp add: the_preced_def)  +
−
    done+
−
      +
−
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+
−
+
−
find_theorems RAG "(e#s)" "_ = _"+
−
+
−
text {* (* ddd *)+
−
  The following two lemmas confirm that @{text "Set"}-operation+
−
  only changes the precedence of the initiating thread (or actor)+
−
  of the operation (or event).+
−
*}+
−
+
−
+
−
lemma eq_preced:+
−
  assumes "th' \<noteq> th"+
−
  shows "preced th' (e#s) = preced th' s"+
−
proof -+
−
  from assms show ?thesis +
−
    by (unfold is_set, auto simp:preced_def)+
−
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_pre:+
−
  shows "cp (e#s) th' = cp s th'"+
−
  using cp_kept_1 cp_kept_2+
−
  by (cases "th' = th", auto)+
−
+
−
lemma eq_cp: +
−
  shows "cp (e#s) = cp s"+
−
  by (rule ext, unfold eq_cp_pre, simp)+
−
+
−
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 {*+
−
  It can be shown that the @{text tG} is not changed by +
−
  the @{text P}-action. The reason is that the edge added to @{text RAG}+
−
  by the @{text P}-action, namely @{text "(Cs cs, Th th)"},+
−
  does not bring any new thread into graph @{text tG}, because +
−
  the node of @{text cs} is isolated from the original @{text RAG}.+
−
*}+
−
+
−
thm RAG_es+
−
+
−
lemma tG_es: "tG (e # s) = tG s"+
−
proof -+
−
  have [simp]: "\<And> th1. (Th th1, Cs cs) \<notin> RAG s"+
−
    by (metis in_RAG_E no_holder node.simps(4) the_cs.simps waiting_holding)+
−
  show ?thesis+
−
    apply (unfold tG_def_tRAG tRAG_alt_def RAG_es)+
−
    by (auto)+
−
qed+
−
+
−
text {*+
−
  Since both @{text tG} and precedences are not changed, it is easy+
−
  to show that all @{text cp}-value are not changed, therefore, +
−
  no @{text cp}-recalculation is needed:+
−
*}+
−
+
−
lemma cp_kept: "cp (e#s) = cp s"+
−
  by (rule ext, simp add: cp_alt_def2 preced_kept tG_es)+
−
+
−
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] .+
−
+
−
+
−
lemma tG_ancestors_tRAG_refute:+
−
  assumes "th'' \<notin> ancestors (tG (e#s)) th"+
−
  shows "Th th'' \<notin> ancestors (tRAG (e#s)) (Th th)"+
−
  using assms using node.inject(1) tRAG_ancestorsE_tG by force +
−
+
−
text {*+
−
  The following lemma shows only the ancestors of @{text th} (the initiating +
−
  thread of the @{text P}-operation) may possibly +
−
  need a @{text cp}-recalculation. All other threads (including @{text th} itself)+
−
  do not need @{text cp}-recalculation. +
−
*}+
−
+
−
lemma cp_kept:+
−
  assumes "Th th'' \<notin> ancestors (tRAG (e#s)) (Th th)"+
−
  shows "cp (e#s) th'' = cp s th''"+
−
proof -+
−
  have h: "subtree (tRAG (e#s)) (Th th'') = subtree (tRAG s) (Th th'')"+
−
  proof -+
−
    have "Th holder \<notin> subtree (tRAG s) (Th th'')"+
−
    proof+
−
      assume "Th holder \<in> subtree (tRAG s) (Th th'')"+
−
      thus False+
−
      proof(rule subtreeE)+
−
         assume "Th holder = Th th''"+
−
         from assms[unfolded tRAG_s ancestors_def, folded this]+
−
         show ?thesis by auto+
−
      next+
−
         assume "Th th'' \<in> ancestors (tRAG s) (Th holder)"+
−
         moreover have "... \<subseteq> ancestors (tRAG (e#s)) (Th holder)"+
−
         proof(rule ancestors_mono)+
−
            show "tRAG s \<subseteq> tRAG (e#s)" by (unfold tRAG_s, auto)+
−
         qed +
−
         ultimately have "Th th'' \<in> ancestors (tRAG (e#s)) (Th holder)" by auto+
−
         moreover have "Th holder \<in> ancestors (tRAG (e#s)) (Th th)"+
−
           by (unfold tRAG_s, auto simp:ancestors_def)+
−
         ultimately have "Th th'' \<in> ancestors (tRAG (e#s)) (Th th)"+
−
                       by (auto simp:ancestors_def)+
−
         with assms show ?thesis by auto+
−
      qed+
−
    qed+
−
    from subtree_insert_next[OF this]+
−
    have "subtree (tRAG s \<union> {(Th th, Th holder)}) (Th th'') = subtree (tRAG s) (Th th'')" .+
−
    from this[folded tRAG_s] show ?thesis .+
−
  qed+
−
  show ?thesis by (unfold cp_alt_def1 h preced_kept, simp)+
−
qed+
−
+
−
lemma cp_kept_tG: (* aaa *)+
−
  assumes "th'' \<notin> ancestors (tG (e#s)) th"+
−
  shows "cp (e#s) th'' = cp s th''"+
−
  using cp_kept tG_ancestors_tRAG_refute assms+
−
  by blast+
−
  +
−
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+
−
+
−
lemma cp_up_tG: (* aaa *)+
−
  assumes "th' \<in> ancestors (tG (e#s)) th"+
−
  and "cp (e#s) th' = cp s th'"+
−
  and "th'' \<in> ancestors (tG (e#s)) th'"+
−
  shows "cp (e#s) th'' = cp s th''"+
−
  using assms cp_up ancestors_tG_tRAG by blast   +
−
+
−
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)"+
−
  unfolding  children_of_th+
−
  apply(subst vat_es.cp_rec)+
−
  apply(simp add:the_preced_def children_of_th)+
−
  done+
−
    +
−
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+
−
+
−