section {*

  This file contains lemmas used to guide the recalculation of current precedence 

  after every system call (or system operation)

*}

theory Implementation

imports PIPBasics

begin

text {* (* ddd *)

  One beauty of our modelling is that we follow the definitional extension tradition of HOL.

  The benefit of such a concise and miniature model is that  large number of intuitively 

  obvious facts are derived as lemmas, rather than asserted as axioms.

*}

text {*

  However, the lemmas in the forthcoming several locales are no longer 

  obvious. These lemmas show how the current precedences should be recalculated 

  after every execution step (in our model, every step is represented by an event, 

  which in turn, represents a system call, or operation). Each operation is 

  treated in a separate locale.

  The complication of current precedence recalculation comes 

  because the changing of RAG needs to be taken into account, 

  in addition to the changing of precedence. 

  The reason RAG changing affects current precedence is that,

  according to the definition, current precedence 

  of a thread is the maximum of the precedences of its dependants, 

  where the dependants are defined in terms of RAG.

  Therefore, each operation, lemmas concerning the change of the precedences 

  and RAG are derived first, so that the lemmas about

  current precedence recalculation can be based on.

*}

text {* (* ddd *)

  The following locale @{text "step_set_cps"} investigates the recalculation 

  after the @{text "Set"} operation.

*}

locale step_set_cps =

  fixes s' th prio s 

  -- {* @{text "s'"} is the system state before the operation *}

  -- {* @{text "s"} is the system state after the operation *}

  defines s_def : "s \<equiv> (Set th prio#s')" 

  -- {* @{text "s"} is assumed to be a legitimate state, from which

         the legitimacy of @{text "s"} can be derived. *}

  assumes vt_s: "vt s"

sublocale step_set_cps < vat_s : valid_trace "s"

proof

  from vt_s show "vt s" .

qed

sublocale step_set_cps < vat_s' : valid_trace "s'"

proof

  from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .

qed

context step_set_cps 

begin

text {* (* ddd *)

  The following two lemmas confirm that @{text "Set"}-operating only changes the precedence 

  of the initiating thread.

*}

lemma eq_preced:

  assumes "th' \<noteq> th"

  shows "preced th' s = preced th' s'"

proof -

  from assms show ?thesis 

    by (unfold s_def, auto simp:preced_def)

qed

lemma eq_the_preced: 

  fixes th'

  assumes "th' \<noteq> th"

  shows "the_preced s th' = the_preced s' th'"

  using assms

  by (unfold the_preced_def, intro eq_preced, simp)

text {*

  The following lemma assures that the resetting of priority does not change the RAG. 

*}

lemma eq_dep: "RAG s = RAG s'"

  by (unfold s_def RAG_set_unchanged, auto)

text {* (* ddd *)

  Th following lemma @{text "eq_cp_pre"} says the priority change of @{text "th"}

  only affects those threads, which as @{text "Th th"} in their sub-trees.

  The proof of this lemma is simplified by using the alternative definition of @{text "cp"}. 

*}

lemma eq_cp_pre:

  fixes th' 

  assumes nd: "Th th \<notin> subtree (RAG s') (Th th')"

  shows "cp 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 s ` {th'a. Th th'a \<in> subtree (RAG 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 eq_dep 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 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 {*

  The following lemma shows that @{term "th"} is not in the 

  sub-tree of any other thread. 

*}

lemma th_in_no_subtree:

  assumes "th' \<noteq> th"

  shows "Th th \<notin> subtree (RAG s') (Th th')"

proof -

  have "th \<in> readys s'"

  proof -

    from step_back_step [OF vt_s[unfolded s_def]]

    have "step s' (Set th prio)" .

    hence "th \<in> runing s'" by (cases, simp)

    thus ?thesis by (simp add:readys_def runing_def)

  qed

  from vat_s'.readys_in_no_subtree[OF this assms(1)]

  show ?thesis by blast

qed

text {* 

  By combining @{thm "eq_cp_pre"} and @{thm "th_in_no_subtree"}, 

  it is obvious that the change of priority only affects the @{text "cp"}-value 

  of the initiating thread @{text "th"}.

*}

lemma eq_cp:

  fixes th' 

  assumes "th' \<noteq> th"

  shows "cp s th' = cp s' th'"

  by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]])

end

text {*

  The following @{text "step_v_cps"} is the locale for @{text "V"}-operation.

*}

locale step_v_cps =

  -- {* @{text "th"} is the initiating thread *}

  -- {* @{text "cs"} is the critical resource release by the @{text "V"}-operation *}

  fixes s' th cs s    -- {* @{text "s'"} is the state before operation*}

  defines s_def : "s \<equiv> (V th cs#s')" -- {* @{text "s"} is the state after operation*}

  -- {* @{text "s"} is assumed to be valid, which implies the validity of @{text "s'"} *}

  assumes vt_s: "vt s"

sublocale step_v_cps < vat_s : valid_trace "s"

proof

  from vt_s show "vt s" .

qed

sublocale step_v_cps < vat_s' : valid_trace "s'"

proof

  from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .

qed

context step_v_cps

begin

lemma ready_th_s': "th \<in> readys s'"

  using step_back_step[OF vt_s[unfolded s_def]]

  by (cases, simp add:runing_def)

lemma ancestors_th: "ancestors (RAG s') (Th th) = {}"

proof -

  from vat_s'.readys_root[OF ready_th_s']

  show ?thesis

  by (unfold root_def, simp)

qed

lemma holding_th: "holding s' th cs"

proof -

  from vt_s[unfolded s_def]

  have " PIP s' (V th cs)" by (cases, simp)

  thus ?thesis by (cases, auto)

qed

lemma edge_of_th:

    "(Cs cs, Th th) \<in> RAG s'" 

proof -

 from holding_th

 show ?thesis 

    by (unfold s_RAG_def holding_eq, auto)

qed

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}"

  proof(rule vat_s'.rtree_RAG.ancestors_accum)

    from vt_s[unfolded s_def]

    have " PIP s' (V th cs)" by (cases, simp)

    thus "(Cs cs, Th th) \<in> RAG s'" 

    proof(cases)

      assume "holding s' th cs"

      from this[unfolded holding_eq]

      show ?thesis by (unfold s_RAG_def, auto)

    qed

  qed

  from this[unfolded ancestors_th] show ?thesis by simp

qed

lemma preced_kept: "the_preced s = the_preced s'"

  by (auto simp: s_def the_preced_def preced_def)

end

text {*

  The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, 

  which represents the case when there is another thread @{text "th'"}

  to take over the critical resource released by the initiating thread @{text "th"}.

*}

locale step_v_cps_nt = step_v_cps +

  fixes th'

  -- {* @{text "th'"} is assumed to take over @{text "cs"} *}

  assumes nt: "next_th s' th cs th'" 

context step_v_cps_nt

begin

text {*

  Lemma @{text "RAG_s"} confirms the change of RAG:

  two edges removed and one added, as shown by the following diagram.

*}

(*

  RAG before the V-operation

    th1 ----|

            |

    th' ----|

            |----> cs -----|

    th2 ----|              |

            |              |

    th3 ----|              |

                           |------> th

    th4 ----|              |

            |              |

    th5 ----|              |

            |----> cs'-----|

    th6 ----|

            |

    th7 ----|

 RAG after the V-operation

    th1 ----|

            |

            |----> cs ----> th'

    th2 ----|              

            |              

    th3 ----|              

    th4 ----|              

            |              

    th5 ----|              

            |----> cs'----> th

    th6 ----|

            |

    th7 ----|

*)

lemma sub_RAGs': "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s'"

                using next_th_RAG[OF nt]  .

lemma ancestors_th': 

  "ancestors (RAG s') (Th th') = {Th th, Cs cs}" 

proof -

  have "ancestors (RAG s') (Th th') = ancestors (RAG s') (Cs cs) \<union> {Cs cs}"

  proof(rule  vat_s'.rtree_RAG.ancestors_accum)

    from sub_RAGs' show "(Th th', Cs cs) \<in> RAG s'" by auto

  qed

  thus ?thesis using ancestors_th ancestors_cs by auto

qed

lemma RAG_s:

  "RAG s = (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union>

                                         {(Cs cs, Th th')}"

proof -

  from step_RAG_v[OF vt_s[unfolded s_def], folded s_def]

    and nt show ?thesis  by (auto intro:next_th_unique)

qed

lemma subtree_kept:

  assumes "th1 \<notin> {th, th'}"

  shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)" (is "_ = ?R")

proof -

  let ?RAG' = "(RAG s' - {(Cs cs, Th th), (Th th', Cs cs)})"

  let ?RAG'' = "?RAG' \<union> {(Cs cs, Th th')}"

  have "subtree ?RAG' (Th th1) = ?R" 

  proof(rule subset_del_subtree_outside)

    show "Range {(Cs cs, Th th), (Th th', 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

  moreover have "subtree ?RAG'' (Th th1) =  subtree ?RAG' (Th th1)"

  proof(rule subtree_insert_next)

    show "Th th' \<notin> subtree (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) (Th th1)"

    proof(rule subtree_refute)

      show "Th th1 \<notin> ancestors (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) (Th th')"

            (is "_ \<notin> ?R")

      proof -

          have "?R \<subseteq> ancestors (RAG s') (Th th')" 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 th'" by simp

    qed

  qed

  ultimately show ?thesis by (unfold RAG_s, simp)

qed

lemma cp_kept:

  assumes "th1 \<notin> {th, th'}"

  shows "cp s th1 = cp s' th1"

    by (unfold cp_alt_def preced_kept subtree_kept[OF assms], simp)

end

locale step_v_cps_nnt = step_v_cps +

  assumes nnt: "\<And> th'. (\<not> next_th s' th cs th')"

context step_v_cps_nnt

begin

lemma RAG_s: "RAG s = RAG s' - {(Cs cs, Th th)}"

proof -

  from nnt and  step_RAG_v[OF vt_s[unfolded s_def], folded s_def]

  show ?thesis by auto

qed

lemma subtree_kept:

  assumes "th1 \<noteq> th"

  shows "subtree (RAG 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

lemma cp_kept_1:

  assumes "th1 \<noteq> th"

  shows "cp s th1 = cp s' th1"

    by (unfold cp_alt_def preced_kept subtree_kept[OF assms], simp)

lemma subtree_cs: "subtree (RAG s') (Cs cs) = {Cs cs}"

proof -

  { fix n

    have "(Cs cs) \<notin> ancestors (RAG s') n"

    proof

      assume "Cs cs \<in> ancestors (RAG s') n"

      hence "(n, Cs cs) \<in> (RAG s')^+" by (auto simp:ancestors_def)

      from tranclE[OF this] obtain nn where h: "(nn, Cs cs) \<in> RAG s'" by auto

      then obtain th' where "nn = Th th'"

        by (unfold s_RAG_def, auto)

      from h[unfolded this] have "(Th th', Cs cs) \<in> RAG s'" .

      from this[unfolded s_RAG_def]

      have "waiting (wq s') th' cs" by auto

      from this[unfolded cs_waiting_def]

      have "1 < length (wq s' cs)"

          by (cases "wq s' cs", auto)

      from holding_next_thI[OF holding_th this]

      obtain th' where "next_th s' th cs th'" by auto

      with nnt show False by auto

    qed

  } note h = this

  {  fix n

     assume "n \<in> subtree (RAG s') (Cs cs)"

     hence "n = (Cs cs)"

     by (elim subtreeE, insert h, auto)

  } moreover have "(Cs cs) \<in> subtree (RAG s') (Cs cs)"

      by (auto simp:subtree_def)

  ultimately show ?thesis by auto 

qed

lemma subtree_th: 

  "subtree (RAG s) (Th th) = subtree (RAG s') (Th th) - {Cs cs}"

proof(unfold RAG_s, fold subtree_cs, rule vat_s'.rtree_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 s th = cp s' th" 

 by (unfold cp_alt_def subtree_th preced_kept, auto)

lemma eq_cp:

  fixes th' 

  shows "cp s th' = cp s' th'"

  using cp_kept_1 cp_kept_2

  by (cases "th' = th", auto)

end

locale step_P_cps =

  fixes s' th cs s 

  defines s_def : "s \<equiv> (P th cs#s')"

  assumes vt_s: "vt s"

sublocale step_P_cps < vat_s : valid_trace "s"

proof

  from vt_s show "vt s" .

qed

sublocale step_P_cps < vat_s' : valid_trace "s'"

proof

  from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .

qed

context step_P_cps

begin

lemma readys_th: "th \<in> readys s'"

proof -

    from step_back_step [OF vt_s[unfolded s_def]]

    have "PIP s' (P th cs)" .

    hence "th \<in> runing s'" by (cases, simp)

    thus ?thesis by (simp add:readys_def runing_def)

qed

lemma root_th: "root (RAG s') (Th th)"

  using readys_root[OF readys_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

lemma preced_kept: "the_preced s = the_preced s'"

  by (auto simp: s_def the_preced_def preced_def)

end

locale step_P_cps_ne =step_P_cps +

  fixes th'

  assumes ne: "wq s' cs \<noteq> []"

  defines th'_def: "th' \<equiv> hd (wq s' cs)"

locale step_P_cps_e =step_P_cps +

  assumes ee: "wq s' cs = []"

context step_P_cps_e

begin

lemma RAG_s: "RAG s = RAG s' \<union> {(Cs cs, Th th)}"

proof -

  from ee and  step_RAG_p[OF vt_s[unfolded s_def], folded s_def]

  show ?thesis by auto

qed

lemma subtree_kept:

  assumes "th' \<noteq> th"

  shows "subtree (RAG s) (Th th') = subtree (RAG s') (Th th')"

proof(unfold RAG_s, rule subtree_insert_next)

  from in_no_others_subtree[OF assms] 

  show "Th th \<notin> subtree (RAG s') (Th th')" .

qed

lemma cp_kept: 

  assumes "th' \<noteq> th"

  shows "cp s th' = cp s' th'"

proof -

  have "(the_preced s ` {th'a. Th th'a \<in> subtree (RAG 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

context step_P_cps_ne 

begin

lemma RAG_s: "RAG s = RAG s' \<union> {(Th th, Cs cs)}"