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