theory Implementation

imports PIPBasics

begin

section {*

  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.

*}

text {*

  The following two lemmas are general about any valid system state, 

  but are used in the derivation in more specific system operations. 

*}

context valid_trace

begin

lemma readys_root:

  assumes "th \<in> readys s"

  shows "root (RAG s) (Th th)"

proof -

  { fix x

    assume "x \<in> ancestors (RAG s) (Th th)"

    hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def)

    from tranclD[OF this]

    obtain z where "(Th th, z) \<in> RAG s" by auto

    with assms(1) have False

         apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_raw)

         by (fold wq_def, blast)

  } thus ?thesis by (unfold root_def, auto)

qed

lemma readys_in_no_subtree:

  assumes "th \<in> readys s"

  and "th' \<noteq> th"

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

proof

   assume "Th th \<in> subtree (RAG s) (Th th')"

   thus False

   proof(cases rule:subtreeE)

      case 1

      with assms show ?thesis by auto

   next

      case 2

      with readys_root[OF assms(1)]

      show ?thesis by (auto simp:root_def)

   qed

qed

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 *)

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

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

  The proof of this lemma is simplified by using the alternative definition 

  of @{text "cp"}. 

*}

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 {*

  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 -

  from readys_in_no_subtree[OF th_ready_s 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:

  assumes "th' \<noteq> th"

  shows "cp (e#s) th' = cp s th'"

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

end

section {* The @{term V} operation *}

text {*

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

*}

context valid_trace_v

begin

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

proof -

  from readys_root[OF th_ready_s]

  show ?thesis

  by (unfold root_def, simp)

qed

lemma edge_of_th:

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

proof -

 from holding_th_cs_s

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

   by (rule rtree_RAG.ancestors_accum[OF edge_of_th])

  from this[unfolded ancestors_th] show ?thesis by simp

qed

end

text {*

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

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

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

*}

lemma (in valid_trace_v)

  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

context valid_trace_v_n

begin

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 waiting_eq holding_eq, auto)

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  rtree_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

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)

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

  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

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

  proof(rule subtree_insert_next)

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

    proof(rule subtree_refute)

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

            (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

  qed

  ultimately show ?thesis by (unfold RAG_s, simp)

qed

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)

end

context valid_trace_v_e

begin

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

  by (unfold RAG_es waiting_set_eq holding_set_eq, simp)

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

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)

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 waiting_eq)

      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

lemma subtree_th: 

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

proof(unfold RAG_s, fold subtree_cs, rule 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 (e#s) th = cp s th" 

 by (unfold cp_alt_def subtree_th the_preced_es, auto)

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

context valid_trace_p

begin

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

  by (simp add: ready_th_s readys_root)

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 (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

context valid_trace_p_h

begin

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

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

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 holding_eq, auto)

lemma tRAG_s: 

  "tRAG (e#s) = tRAG s \<union> {(Th th, Th holder)}"

  using RAG_tRAG_transfer[OF RAG_es cs_held] .

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_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

            proof(cases rule:vat_es.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