theory Correctness

imports PIPBasics

begin

text {* 

  The following two auxiliary lemmas are used to reason about @{term Max}.

*}

lemma image_Max_eqI: 

  assumes "finite B"

  and "b \<in> B"

  and "\<forall> x \<in> B. f x \<le> f b"

  shows "Max (f ` B) = f b"

  using assms

  using Max_eqI by blast 

lemma image_Max_subset:

  assumes "finite A"

  and "B \<subseteq> A"

  and "a \<in> B"

  and "Max (f ` A) = f a"

  shows "Max (f ` B) = f a"

proof(rule image_Max_eqI)

  show "finite B"

    using assms(1) assms(2) finite_subset by auto 

next

  show "a \<in> B" using assms by simp

next

  show "\<forall>x\<in>B. f x \<le> f a"

    by (metis Max_ge assms(1) assms(2) assms(4) 

            finite_imageI image_eqI subsetCE) 

qed

text {*

  The following locale @{text "highest_gen"} sets the basic context for our

  investigation: supposing thread @{text th} holds the highest @{term cp}-value

  in state @{text s}, which means the task for @{text th} is the 

  most urgent. We want to show that  

  @{text th} is treated correctly by PIP, which means

  @{text th} will not be blocked unreasonably by other less urgent

  threads. 

*}

locale highest_gen =

  fixes s th prio tm

  assumes vt_s: "vt s"

  and threads_s: "th \<in> threads s"

  and highest: "preced th s = Max ((cp s)`threads s)"

  -- {* The internal structure of @{term th}'s precedence is exposed:*}

  and preced_th: "preced th s = Prc prio tm" 

-- {* @{term s} is a valid trace, so it will inherit all results derived for

      a valid trace: *}

sublocale highest_gen < vat_s: valid_trace "s"

  by (unfold_locales, insert vt_s, simp)

context highest_gen

begin

text {*

  @{term tm} is the time when the precedence of @{term th} is set, so 

  @{term tm} must be a valid moment index into @{term s}.

*}

lemma lt_tm: "tm < length s"

  by (insert preced_tm_lt[OF threads_s preced_th], simp)

text {*

  Since @{term th} holds the highest precedence and @{text "cp"}

  is the highest precedence of all threads in the sub-tree of 

  @{text "th"} and @{text th} is among these threads, 

  its @{term cp} must equal to its precedence:

*}

lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R")

proof -

  have "?L \<le> ?R"

  by (unfold highest, rule Max_ge, 

        auto simp:threads_s finite_threads)

  moreover have "?R \<le> ?L"

    by (unfold vat_s.cp_rec, rule Max_ge, 

        auto simp:the_preced_def vat_s.fsbttRAGs.finite_children)

  ultimately show ?thesis by auto

qed

lemma highest_cp_preced: "cp s th = Max ((\<lambda> th'. preced th' s) ` threads s)"

  by (fold max_cp_eq, unfold eq_cp_s_th, insert highest, simp)

lemma highest_preced_thread: "preced th s = Max ((\<lambda> th'. preced th' s) ` threads s)"

  by (fold eq_cp_s_th, unfold highest_cp_preced, simp)

lemma highest': "cp s th = Max (cp s ` threads s)"

proof -

  from highest_cp_preced max_cp_eq[symmetric]

  show ?thesis by simp

qed

end

locale extend_highest_gen = highest_gen + 

  fixes t 

  assumes vt_t: "vt (t@s)"

  and create_low: "Create th' prio' \<in> set t \<Longrightarrow> prio' \<le> prio"

  and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio"

  and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> th"

sublocale extend_highest_gen < vat_t: valid_trace "t@s"

  by (unfold_locales, insert vt_t, simp)

lemma step_back_vt_app: 

  assumes vt_ts: "vt (t@s)" 

  shows "vt s"

proof -

  from vt_ts show ?thesis

  proof(induct t)

    case Nil

    from Nil show ?case by auto

  next

    case (Cons e t)

    assume ih: " vt (t @ s) \<Longrightarrow> vt s"

      and vt_et: "vt ((e # t) @ s)"

    show ?case

    proof(rule ih)

      show "vt (t @ s)"

      proof(rule step_back_vt)

        from vt_et show "vt (e # t @ s)" by simp

      qed

    qed

  qed

qed

locale red_extend_highest_gen = extend_highest_gen +

   fixes i::nat

sublocale red_extend_highest_gen <   red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)"

  apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])

  apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp)

  by (unfold highest_gen_def, auto dest:step_back_vt_app)

context extend_highest_gen

begin

 lemma ind [consumes 0, case_names Nil Cons, induct type]:

  assumes 

    h0: "R []"

  and h2: "\<And> e t. \<lbrakk>vt (t@s); step (t@s) e; 

                    extend_highest_gen s th prio tm t; 

                    extend_highest_gen s th prio tm (e#t); R t\<rbrakk> \<Longrightarrow> R (e#t)"

  shows "R t"

proof -

  from vt_t extend_highest_gen_axioms show ?thesis

  proof(induct t)

    from h0 show "R []" .

  next

    case (Cons e t')

    assume ih: "\<lbrakk>vt (t' @ s); extend_highest_gen s th prio tm t'\<rbrakk> \<Longrightarrow> R t'"

      and vt_e: "vt ((e # t') @ s)"

      and et: "extend_highest_gen s th prio tm (e # t')"

    from vt_e and step_back_step have stp: "step (t'@s) e" by auto

    from vt_e and step_back_vt have vt_ts: "vt (t'@s)" by auto

    show ?case

    proof(rule h2 [OF vt_ts stp _ _ _ ])

      show "R t'"

      proof(rule ih)

        from et show ext': "extend_highest_gen s th prio tm t'"

          by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt)

      next

        from vt_ts show "vt (t' @ s)" .

      qed

    next

      from et show "extend_highest_gen s th prio tm (e # t')" .

    next

      from et show ext': "extend_highest_gen s th prio tm t'"

          by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt)

    qed

  qed

qed

lemma th_kept: "th \<in> threads (t @ s) \<and> 

                 preced th (t@s) = preced th s" (is "?Q t") 

proof -

  show ?thesis

  proof(induct rule:ind)

    case Nil

    from threads_s

    show ?case

      by auto

  next

    case (Cons e t)

    interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto

    interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto

    show ?case

    proof(cases e)

      case (Create thread prio)

      show ?thesis

      proof -

        from Cons and Create have "step (t@s) (Create thread prio)" by auto

        hence "th \<noteq> thread"

        proof(cases)

          case thread_create

          with Cons show ?thesis by auto

        qed

        hence "preced th ((e # t) @ s)  = preced th (t @ s)"

          by (unfold Create, auto simp:preced_def)

        moreover note Cons

        ultimately show ?thesis

          by (auto simp:Create)

      qed

    next

      case (Exit thread)

      from h_e.exit_diff and Exit

      have neq_th: "thread \<noteq> th" by auto

      with Cons

      show ?thesis

        by (unfold Exit, auto simp:preced_def)

    next

      case (P thread cs)

      with Cons

      show ?thesis 

        by (auto simp:P preced_def)

    next

      case (V thread cs)

      with Cons

      show ?thesis 

        by (auto simp:V preced_def)

    next

      case (Set thread prio')

      show ?thesis

      proof -

        from h_e.set_diff_low and Set

        have "th \<noteq> thread" by auto

        hence "preced th ((e # t) @ s)  = preced th (t @ s)"

          by (unfold Set, auto simp:preced_def)

        moreover note Cons

        ultimately show ?thesis

          by (auto simp:Set)

      qed

    qed

  qed

qed

text {*

  According to @{thm th_kept}, thread @{text "th"} has its living status

  and precedence kept along the way of @{text "t"}. The following lemma

  shows that this preserved precedence of @{text "th"} remains as the highest

  along the way of @{text "t"}.

  The proof goes by induction over @{text "t"} using the specialized

  induction rule @{thm ind}, followed by case analysis of each possible 

  operations of PIP. All cases follow the same pattern rendered by the 

  generalized introduction rule @{thm "image_Max_eqI"}. 

  The very essence is to show that precedences, no matter whether they are newly introduced 

  or modified, are always lower than the one held by @{term "th"},

  which by @{thm th_kept} is preserved along the way.

*}

lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"

proof(induct rule:ind)

  case Nil

  from highest_preced_thread

  show ?case

    by (unfold the_preced_def, simp)

next

  case (Cons e t)

    interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto

    interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto

  show ?case

  proof(cases e)

    case (Create thread prio')

    show ?thesis (is "Max (?f ` ?A) = ?t")

    proof -

      -- {* The following is the common pattern of each branch of the case analysis. *}

      -- {* The major part is to show that @{text "th"} holds the highest precedence: *}

      have "Max (?f ` ?A) = ?f th"

      proof(rule image_Max_eqI)

        show "finite ?A" using h_e.finite_threads by auto 

      next

        show "th \<in> ?A" using h_e.th_kept by auto 

      next

        show "\<forall>x\<in>?A. ?f x \<le> ?f th"

        proof 

          fix x

          assume "x \<in> ?A"

          hence "x = thread \<or> x \<in> threads (t@s)" by (auto simp:Create)

          thus "?f x \<le> ?f th"

          proof

            assume "x = thread"

            thus ?thesis 

              apply (simp add:Create the_preced_def preced_def, fold preced_def)

              using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 preced_th by force

          next

            assume h: "x \<in> threads (t @ s)"

            from Cons(2)[unfolded Create] 

            have "x \<noteq> thread" using h by (cases, auto)

            hence "?f x = the_preced (t@s) x" 

              by (simp add:Create the_preced_def preced_def)

            hence "?f x \<le> Max (the_preced (t@s) ` threads (t@s))"

              by (simp add: h_t.finite_threads h)

            also have "... = ?f th"

              by (metis Cons.hyps(5) h_e.th_kept the_preced_def) 

            finally show ?thesis .

          qed

        qed

      qed

     -- {* The minor part is to show that the precedence of @{text "th"} 

           equals to preserved one, given by the foregoing lemma @{thm th_kept} *}

      also have "... = ?t" using h_e.th_kept the_preced_def by auto

      -- {* Then it follows trivially that the precedence preserved

            for @{term "th"} remains the maximum of all living threads along the way. *}

      finally show ?thesis .

    qed 

  next 

    case (Exit thread)

    show ?thesis (is "Max (?f ` ?A) = ?t")

    proof -

      have "Max (?f ` ?A) = ?f th"

      proof(rule image_Max_eqI)

        show "finite ?A" using h_e.finite_threads by auto 

      next

        show "th \<in> ?A" using h_e.th_kept by auto 

      next

        show "\<forall>x\<in>?A. ?f x \<le> ?f th"

        proof 

          fix x

          assume "x \<in> ?A"

          hence "x \<in> threads (t@s)" by (simp add: Exit) 

          hence "?f x \<le> Max (?f ` threads (t@s))" 

            by (simp add: h_t.finite_threads) 

          also have "... \<le> ?f th" 

            apply (simp add:Exit the_preced_def preced_def, fold preced_def)

            using Cons.hyps(5) h_t.th_kept the_preced_def by auto

          finally show "?f x \<le> ?f th" .

        qed

      qed

      also have "... = ?t" using h_e.th_kept the_preced_def by auto

      finally show ?thesis .

    qed 

  next

    case (P thread cs)

    with Cons

    show ?thesis by (auto simp:preced_def the_preced_def)

  next

    case (V thread cs)

    with Cons

    show ?thesis by (auto simp:preced_def the_preced_def)

  next 

    case (Set thread prio')

    show ?thesis (is "Max (?f ` ?A) = ?t")

    proof -

      have "Max (?f ` ?A) = ?f th"

      proof(rule image_Max_eqI)

        show "finite ?A" using h_e.finite_threads by auto 

      next

        show "th \<in> ?A" using h_e.th_kept by auto 

      next

        show "\<forall>x\<in>?A. ?f x \<le> ?f th"

        proof 

          fix x

          assume h: "x \<in> ?A"

          show "?f x \<le> ?f th"

          proof(cases "x = thread")

            case True

            moreover have "the_preced (Set thread prio' # t @ s) thread \<le> the_preced (t @ s) th"

            proof -

              have "the_preced (t @ s) th = Prc prio tm"  

                using h_t.th_kept preced_th by (simp add:the_preced_def)

              moreover have "prio' \<le> prio" using Set h_e.set_diff_low by auto

              ultimately show ?thesis by (insert lt_tm, auto simp:the_preced_def preced_def)

            qed

            ultimately show ?thesis

              by (unfold Set, simp add:the_preced_def preced_def)

          next

            case False

            then have "?f x  = the_preced (t@s) x"

              by (simp add:the_preced_def preced_def Set)

            also have "... \<le> Max (the_preced (t@s) ` threads (t@s))"

              using Set h h_t.finite_threads by auto 

            also have "... = ?f th" by (metis Cons.hyps(5) h_e.th_kept the_preced_def) 

            finally show ?thesis .

          qed

        qed

      qed

      also have "... = ?t" using h_e.th_kept the_preced_def by auto

      finally show ?thesis .

    qed 

  qed

qed

lemma max_preced: "preced th (t@s) = Max (the_preced (t@s) ` (threads (t@s)))"

  by (insert th_kept max_kept, auto)

text {*

  The reason behind the following lemma is that:

  Since @{term "cp"} is defined as the maximum precedence 

  of those threads contained in the sub-tree of node @{term "Th th"} 

  in @{term "RAG (t@s)"}, and all these threads are living threads, and 

  @{term "th"} is also among them, the maximum precedence of 

  them all must be the one for @{text "th"}.

*}

lemma th_cp_max_preced: 

  "cp (t@s) th = Max (the_preced (t@s) ` (threads (t@s)))" (is "?L = ?R") 

proof -

  let ?f = "the_preced (t@s)"

  have "?L = ?f th"

  proof(unfold cp_alt_def, rule image_Max_eqI)

    show "finite {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"

    proof -

      have "{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)} = 

            the_thread ` {n . n \<in> subtree (RAG (t @ s)) (Th th) \<and>

                            (\<exists> th'. n = Th th')}"

      by (smt Collect_cong Setcompr_eq_image mem_Collect_eq the_thread.simps)

      moreover have "finite ..." by (simp add: vat_t.fsbtRAGs.finite_subtree) 

      ultimately show ?thesis by simp

    qed

  next

    show "th \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"

      by (auto simp:subtree_def)

  next

    show "\<forall>x\<in>{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}.

               the_preced (t @ s) x \<le> the_preced (t @ s) th"

    proof

      fix th'

      assume "th' \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"

      hence "Th th' \<in> subtree (RAG (t @ s)) (Th th)" by auto

      moreover have "... \<subseteq> Field (RAG (t @ s)) \<union> {Th th}"

        by (meson subtree_Field)

      ultimately have "Th th' \<in> ..." by auto

      hence "th' \<in> threads (t@s)" 

      proof

        assume "Th th' \<in> {Th th}"

        thus ?thesis using th_kept by auto 

      next

        assume "Th th' \<in> Field (RAG (t @ s))"

        thus ?thesis using vat_t.not_in_thread_isolated by blast 

      qed

      thus "the_preced (t @ s) th' \<le> the_preced (t @ s) th"

        by (metis Max_ge finite_imageI finite_threads image_eqI 

               max_kept th_kept the_preced_def)

    qed

  qed

  also have "... = ?R" by (simp add: max_preced the_preced_def) 

  finally show ?thesis .

qed

lemma th_cp_max: "cp (t@s) th = Max (cp (t@s) ` threads (t@s))"

  using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger

lemma th_cp_preced: "cp (t@s) th = preced th s"

  by (fold max_kept, unfold th_cp_max_preced, simp)

lemma preced_less:

  assumes th'_in: "th' \<in> threads s"

  and neq_th': "th' \<noteq> th"

  shows "preced th' s < preced th s"

  using assms

by (metis Max.coboundedI finite_imageI highest not_le order.trans 

    preced_linorder rev_image_eqI threads_s vat_s.finite_threads 

    vat_s.le_cp)

text {*

  The following lemmas shows that the @{term cp}-value 

  of the blocking thread @{text th'} equals to the highest

  precedence in the whole system.

*}

lemma runing_preced_inversion:

  assumes runing': "th' \<in> runing (t@s)"

  shows "cp (t@s) th' = preced th s" (is "?L = ?R")

proof -

  have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms

      by (unfold runing_def, auto)

  also have "\<dots> = ?R"

      by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) 

  finally show ?thesis .

qed

text {*

  Counting of the number of @{term "P"} and @{term "V"} operations 

  is the cornerstone of a large number of the following proofs. 

  The reason is that this counting is quite easy to calculate and 

  convenient to use in the reasoning. 

  The following lemma shows that the counting controls whether 

  a thread is running or not.

*} (* ccc *)

lemma eq_pv_blocked: (* ddd *)

  assumes neq_th': "th' \<noteq> th"

  and eq_pv: "cntP (t@s) th' = cntV (t@s) th'"

  shows "th' \<notin> runing (t@s)"

proof

  assume otherwise: "th' \<in> runing (t@s)"

  show False

  proof -

    have th'_in: "th' \<in> threads (t@s)"

        using otherwise readys_threads runing_def by auto 

    have "th' = th"

    proof(rule preced_unique)

      -- {* The proof goes like this: 

            it is first shown that the @{term preced}-value of @{term th'} 

            equals to that of @{term th}, then by uniqueness 

            of @{term preced}-values (given by lemma @{thm preced_unique}), 

            @{term th'} equals to @{term th}: *}

      show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R")

      proof -

        -- {* Since the counts of @{term th'} are balanced, the subtree

              of it contains only itself, so, its @{term cp}-value

              equals its @{term preced}-value: *}

        have "?L = cp (t@s) th'"

          by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp)

        -- {* Since @{term "th'"} is running by @{thm otherwise},

              it has the highest @{term cp}-value, by definition, 

              which in turn equals to the @{term cp}-value of @{term th}. *}

        also have "... = ?R" 

            using runing_preced_inversion[OF otherwise] th_kept by simp

        finally show ?thesis .

      qed

    qed (auto simp: th'_in th_kept)

    moreover have "th' \<noteq> th" using neq_th' .

    ultimately show ?thesis by simp

 qed

qed