theory Correctness+
−
imports PIPBasics+
−
begin+
−
+
−
lemma actions_of_len_cons [iff]: +
−
    "length (actions_of ts (e#t)) \<le> length ((actions_of ts t)) + 1"+
−
      by  (unfold actions_of_def, simp)+
−
+
−
+
−
text {* +
−
  The following two auxiliary lemmas are used to reason about @{term Max}.+
−
*}+
−
+
−
lemma subset_Max:+
−
  assumes "finite A"+
−
  and "B \<subseteq> A"+
−
  and "c \<in> B"+
−
  and "Max A = c"+
−
shows "Max B = c"+
−
using Max.subset assms+
−
by (metis Max.coboundedI Max_eqI rev_finite_subset subset_eq)+
−
+
−
+
−
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)+
−
+
−
fun occs where+
−
  "occs Q [] = (if Q [] then 1 else 0::nat)" |+
−
  "occs Q (x#xs) = (if Q (x#xs) then (1 + occs Q xs) else occs Q xs)"+
−
+
−
lemma occs_le: "occs Q t + occs (\<lambda> e. \<not> Q e) t \<le> (1 + length t)"+
−
  by  (induct t, auto)+
−
+
−
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 (the_preced s ` threads s)"+
−
  using eq_cp_s_th highest max_cp_eq the_preced_def by presburger+
−
  +
−
+
−
lemma highest_preced_thread: "preced th s = Max (the_preced s ` threads s)"+
−
  by (fold eq_cp_s_th, unfold highest_cp_preced, simp)+
−
+
−
lemma highest': "cp s th = Max (cp s ` threads s)"+
−
  by (simp add: eq_cp_s_th highest)+
−
+
−
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+
−
+
−
+
−
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 liveness 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: +
−
  shows "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"+
−
proof(induct rule:ind)+
−
  case Nil+
−
  from highest_preced_thread+
−
  show ?case by 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 (force)+
−
      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[simp]: "Max (cp (t@s) ` threads (t@s)) = cp (t@s) th"+
−
  using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger+
−
+
−
lemma [simp]: "Max (cp (t@s) ` threads (t@s)) = Max (the_preced (t@s) ` threads (t@s))"+
−
  by (simp add: th_cp_max_preced)+
−
  +
−
lemma [simp]: "Max (the_preced (t@s) ` threads (t@s)) = the_preced (t@s) th"+
−
  using max_kept th_kept the_preced_def by auto+
−
+
−
lemma [simp]: "the_preced (t@s) th = preced th (t@s)"+
−
  using the_preced_def by auto+
−
+
−
lemma [simp]: "preced th (t@s) = preced th s"+
−
  by (simp add: th_kept)+
−
+
−
lemma [simp]: "cp s th = preced th s"+
−
  by (simp add: eq_cp_s_th)+
−
+
−
lemma th_cp_preced [simp]: "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)+
−
+
−
section {* The `blocking thread` *}+
−
+
−
text {* +
−
  The purpose of PIP is to ensure that the most +
−
  urgent thread @{term th} is not blocked unreasonably. +
−
  Therefore, a clear picture of the blocking thread is essential +
−
  to assure people that the purpose is fulfilled. +
−
  +
−
  In this section, we are going to derive a series of lemmas +
−
  with finally give rise to a picture of the blocking thread. +
−
+
−
  By `blocking thread`, we mean a thread in running state but +
−
  different from thread @{term th}.+
−
*}+
−
+
−
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 running_preced_inversion:+
−
  assumes running': "th' \<in> running (t @ s)"+
−
  shows "cp (t @ s) th' = preced th s"+
−
proof -+
−
  have "th' \<in> readys (t @ s)" using assms+
−
    using running_ready subsetCE by blast+
−
    +
−
  have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" using assms+
−
      unfolding running_def by simp+
−
  also have "... =  Max (cp (t @ s) ` threads (t @ s))"+
−
      using vat_t.max_cp_readys_threads .+
−
  also have "... = cp (t @ s) th"+
−
      using th_cp_max .+
−
  also have "\<dots> = preced th s"+
−
      using th_cp_preced .+
−
  finally show ?thesis .+
−
qed+
−
+
−
text {*+
−
+
−
  The following lemma shows how the counters for @{term "P"} and+
−
  @{term "V"} operations relate to the running threads in the states+
−
  @{term s} and @{term "t @ s"}.  The lemma shows that if a thread's+
−
  @{term "P"}-count equals its @{term "V"}-count (which means it no+
−
  longer has any resource in its possession), it cannot be a running+
−
  thread.+
−
+
−
  The proof is by contraction with the assumption @{text "th' \<noteq> th"}.+
−
  The key is the use of @{thm eq_pv_dependants} to derive the+
−
  emptiness of @{text th'}s @{term dependants}-set from the balance of+
−
  its @{term P} and @{term V} counts.  From this, it can be shown+
−
  @{text th'}s @{term cp}-value equals to its own precedence.+
−
+
−
  On the other hand, since @{text th'} is running, by @{thm+
−
  running_preced_inversion}, its @{term cp}-value equals to the+
−
  precedence of @{term th}.+
−
+
−
  Combining the above two resukts we have that @{text th'} and @{term+
−
  th} have the same precedence. By uniqueness of precedences, we have+
−
  @{text "th' = th"}, which is in contradiction with the assumption+
−
  @{text "th' \<noteq> th"}.+
−
+
−
*} +
−
                      +
−
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> running (t@s)"+
−
proof+
−
  assume otherwise: "th' \<in> running (t@s)"+
−
  show False+
−
  proof -+
−
    have th'_in: "th' \<in> threads (t@s)"+
−
        using otherwise readys_threads running_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 (simp add: detached_cp_preced eq_pv vat_t.detached_intro)+
−
        -- {* Since @{term "th'"} is running, by @{thm running_preced_inversion},+
−
              its @{term cp}-value equals @{term "preced th s"}, +
−
              which equals to @{term "?R"} by simplification: *}+
−
        also have "... = ?R" +
−
        thm running_preced_inversion+
−
            using running_preced_inversion[OF otherwise] by simp+
−
        finally show ?thesis .+
−
      qed+
−
    qed (auto simp: th'_in th_kept)+
−
    with `th' \<noteq> th` show ?thesis by simp+
−
 qed+
−
qed+
−
+
−
text {*+
−
  The following lemma is the extrapolation of @{thm eq_pv_blocked}.+
−
  It says if a thread, different from @{term th}, +
−
  does not hold any resource at the very beginning,+
−
  it will keep hand-emptied in the future @{term "t@s"}.+
−
*}+
−
lemma eq_pv_persist: (* ddd *)+
−
  assumes neq_th': "th' \<noteq> th"+
−
  and eq_pv: "cntP s th' = cntV s th'"+
−
  shows "cntP (t@s) th' = cntV (t@s) th'"+
−
proof(induction rule:ind) -- {* The proof goes by induction. *}+
−
  -- {* The nontrivial case is for the @{term Cons}: *}+
−
  case (Cons e t)+
−
  -- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *}+
−
  interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp+
−
  interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp+
−
  interpret vat_es: valid_trace_e "t@s" e using Cons(1,2) by (unfold_locales, auto)+
−
  show ?case+
−
  proof -+
−
    -- {* It can be proved that @{term cntP}-value of @{term th'} does not change+
−
          by the happening of event @{term e}: *}+
−
    have "cntP ((e#t)@s) th' = cntP (t@s) th'"+
−
    proof(rule ccontr) -- {* Proof by contradiction. *}+
−
      -- {* Suppose @{term cntP}-value of @{term th'} is changed by @{term e}: *}+
−
      assume otherwise: "cntP ((e # t) @ s) th' \<noteq> cntP (t @ s) th'"+
−
      from cntP_diff_inv[OF this[simplified]]+
−
      obtain cs' where "e = P th' cs'" by auto+
−
      from vat_es.pip_e[unfolded this]+
−
      have "th' \<in> running (t@s)" +
−
        by (cases, simp)+
−
      -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis+
−
            shows @{term th'} can not be running at moment  @{term "t@s"}: *}+
−
      moreover have "th' \<notin> running (t@s)" +
−
               using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] .+
−
      -- {* Contradiction is finally derived: *}+
−
      ultimately show False by simp+
−
    qed+
−
    -- {* It can also be proved that @{term cntV}-value of @{term th'} does not change+
−
          by the happening of event @{term e}: *}+
−
    -- {* The proof follows exactly the same pattern as the case for @{term cntP}-value: *}+
−
    moreover have "cntV ((e#t)@s) th' = cntV (t@s) th'"+
−
    proof(rule ccontr) -- {* Proof by contradiction. *}+
−
      assume otherwise: "cntV ((e # t) @ s) th' \<noteq> cntV (t @ s) th'"+
−
      from cntV_diff_inv[OF this[simplified]]+
−
      obtain cs' where "e = V th' cs'" by auto+
−
      from vat_es.pip_e[unfolded this]+
−
      have "th' \<in> running (t@s)" by (cases, auto)+
−
      moreover have "th' \<notin> running (t@s)"+
−
          using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] .+
−
      ultimately show False by simp+
−
    qed+
−
    -- {* Finally, it can be shown that the @{term cntP} and @{term cntV} +
−
          value for @{term th'} are still in balance, so @{term th'} +
−
          is still hand-emptied after the execution of event @{term e}: *}+
−
    ultimately show ?thesis using Cons(5) by metis+
−
  qed+
−
qed (auto simp:eq_pv)+
−
+
−
text {*+
−
  By combining @{thm  eq_pv_blocked} and @{thm eq_pv_persist},+
−
  it can be derived easily that @{term th'} can not be running in the future:+
−
*}+
−
lemma eq_pv_blocked_persist:+
−
  assumes neq_th': "th' \<noteq> th"+
−
  and eq_pv: "cntP s th' = cntV s th'"+
−
  shows "th' \<notin> running (t@s)"+
−
  using assms+
−
  by (simp add: eq_pv_blocked eq_pv_persist) +
−
+
−
text {*+
−
  The following lemma shows the blocking thread @{term th'}+
−
  must hold some resource in the very beginning. +
−
*}+
−
lemma running_cntP_cntV_inv: (* ddd *)+
−
  assumes is_running: "th' \<in> running (t@s)"+
−
  and neq_th': "th' \<noteq> th"+
−
  shows "cntP s th' > cntV s th'"+
−
  using assms+
−
proof -+
−
  -- {* First, it can be shown that the number of @{term P} and+
−
        @{term V} operations can not be equal for thred @{term th'} *}+
−
  have "cntP s th' \<noteq> cntV s th'"+
−
  proof+
−
     -- {* The proof goes by contradiction, suppose otherwise: *}+
−
    assume otherwise: "cntP s th' = cntV s th'"+
−
    -- {* By applying @{thm  eq_pv_blocked_persist} to this: *}+
−
    from eq_pv_blocked_persist[OF neq_th' otherwise] +
−
    -- {* we have that @{term th'} can not be running at moment @{term "t@s"}: *}+
−
    have "th' \<notin> running (t@s)" .+
−
    -- {* This is obvious in contradiction with assumption @{thm is_running}  *}+
−
    thus False using is_running by simp+
−
  qed+
−
  -- {* However, the number of @{term V} is always less or equal to @{term P}: *}+
−
  moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto+
−
  -- {* Thesis is finally derived by combining the these two results: *}+
−
  ultimately show ?thesis by auto+
−
qed+
−
+
−
+
−
text {*+
−
  The following lemmas shows the blocking thread @{text th'} must be live +
−
  at the very beginning, i.e. the moment (or state) @{term s}. +
−
+
−
  The proof is a  simple combination of the results above:+
−
*}+
−
lemma running_threads_inv: +
−
  assumes running': "th' \<in> running (t@s)"+
−
  and neq_th': "th' \<noteq> th"+
−
  shows "th' \<in> threads s"+
−
proof(rule ccontr) -- {* Proof by contradiction: *}+
−
  assume otherwise: "th' \<notin> threads s" +
−
  have "th' \<notin> running (t @ s)"+
−
  proof -+
−
    from vat_s.cnp_cnv_eq[OF otherwise]+
−
    have "cntP s th' = cntV s th'" .+
−
    from eq_pv_blocked_persist[OF neq_th' this]+
−
    show ?thesis .+
−
  qed+
−
  with running' show False by simp+
−
qed+
−
+
−
text {*+
−
  The following lemma summarizes several foregoing +
−
  lemmas to give an overall picture of the blocking thread @{text "th'"}:+
−
*}+
−
lemma running_inversion: (* ddd, one of the main lemmas to present *)+
−
  assumes running': "th' \<in> running (t@s)"+
−
  and neq_th: "th' \<noteq> th"+
−
  shows "th' \<in> threads s"+
−
  and    "\<not>detached s th'"+
−
  and    "cp (t@s) th' = preced th s"+
−
proof -+
−
  from running_threads_inv[OF assms]+
−
  show "th' \<in> threads s" .+
−
next+
−
  from running_cntP_cntV_inv[OF running' neq_th]+
−
  show "\<not>detached s th'" using vat_s.detached_eq by simp+
−
next+
−
  from running_preced_inversion[OF running']+
−
  show "cp (t@s) th' = preced th s" .+
−
qed+
−
+
−
section {* The existence of `blocking thread` *}+
−
+
−
lemma th_ancestor_has_max_ready:+
−
  assumes th'_in: "th' \<in> readys (t@s)" +
−
  and dp: "th' \<in> nancestors (tG (t @ s)) th"+
−
  shows "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" (is "?L = ?R")+
−
proof -+
−
      -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),+
−
            the  @{term cp}-value of @{term th'} is the maximum of +
−
            all precedences of all thread nodes in its @{term tRAG}-subtree: *}+
−
      have "?L =  Max (the_preced (t @ s) ` (subtree (tG (t @ s)) th'))"+
−
            by (unfold cp_alt_def2, simp)+
−
      also have "... = (the_preced (t @ s) th)"+
−
      proof(rule image_Max_subset)+
−
        show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads)+
−
      next+
−
        show "subtree (tG (t @ s)) th' \<subseteq> threads (t @ s)"+
−
          using readys_def th'_in vat_t.subtree_tG_thread by auto +
−
      next+
−
        show "th \<in> subtree (tG (t @ s)) th'" +
−
        using dp unfolding subtree_def nancestors_def2 by simp  +
−
      next+
−
        show " Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"+
−
          by simp+
−
      qed+
−
      also have "... = ?R"+
−
        using th_cp_max th_cp_preced th_kept +
−
              the_preced_def vat_t.max_cp_readys_threads by auto+
−
      finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" .+
−
 qed +
−
+
−
+
−
text {* +
−
  Suppose @{term th} is not running, it is first shown that+
−
  there is a path in RAG leading from node @{term th} to another thread @{text "th'"} +
−
  in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).+
−
+
−
  Now, since @{term readys}-set is non-empty, there must be+
−
  one in it which holds the highest @{term cp}-value, which, by definition, +
−
  is the @{term running}-thread. However, we are going to show more: this +
−
  running thread is exactly @{term "th'"}. *}+
−
+
−
+
−
lemma th_blockedE: (* ddd, the other main lemma to be presented: *)+
−
  obtains th' where "th' \<in> nancestors (tG (t @ s)) th"+
−
                    "th' \<in> running (t @ s)"+
−
proof -+
−
    -- {* According to @{thm vat_t.th_chain_to_ready}, there is a+
−
       ready ancestor of @{term th}. *}+
−
  have "\<exists>th' \<in> nancestors (tG (t @ s)) th. th' \<in> readys (t @ s)" +
−
    using th_kept vat_t.th_chain_to_ready_tG by auto+
−
  then obtain th' where th'_in: "th' \<in> readys (t @ s)"+
−
                    and dp: "th' \<in> nancestors (tG (t @ s)) th"+
−
    by blast+
−
+
−
  -- {* We are going to first show that this @{term th'} is running. *}+
−
+
−
  from th'_in dp+
−
  have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" +
−
    by (rule th_ancestor_has_max_ready)+
−
  with `th' \<in> readys (t @ s)` +
−
  have "th' \<in> running (t @ s)" by (simp add: running_def) +
−
 +
−
  -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}+
−
  moreover have "th' \<in> nancestors (tG (t @ s)) th"+
−
    using dp unfolding nancestors_def2 by simp+
−
  ultimately show ?thesis using that by metis+
−
qed+
−
+
−
lemma th_blockedE_pretty:+
−
  shows "\<exists>th' \<in> nancestors (tG (t @ s)) th. th' \<in> running (t @ s)"+
−
using th_blockedE assms +
−
by blast+
−
+
−
+
−
text {*+
−
  Now it is easy to see there is always a thread to run by case analysis+
−
  on whether thread @{term th} is running: if the answer is yes, the +
−
  the running thread is obviously @{term th} itself; otherwise, the running+
−
  thread is the @{text th'} given by lemma @{thm th_blockedE}.+
−
*}+
−
lemma live: "running (t @ s) \<noteq> {}"+
−
using th_blockedE by auto+
−
+
−
lemma blockedE:+
−
  assumes "th \<notin> running (t @ s)"+
−
  obtains th' where "th' \<in> nancestors (tG (t @ s)) th"+
−
                    "th' \<in> running (t @ s)"+
−
                    "th' \<in> threads s"+
−
                    "\<not>detached s th'"+
−
                    "cp (t @ s) th' = preced th s"+
−
                    "th' \<noteq> th"+
−
proof -+
−
  obtain th' where a: "th' \<in> nancestors (tG (t @ s)) th" "th' \<in> running (t @ s)"+
−
    using th_blockedE by blast+
−
  moreover+
−
    from a(2) have b: "th' \<in> threads s" +
−
    using running_threads_inv assms by metis+
−
  moreover+
−
    from a(2) have "\<not>detached s th'" +
−
    using running_inversion(2) assms by metis+
−
  moreover+
−
    from a(2) have "cp (t @ s) th' = preced th s" +
−
    using running_preced_inversion by blast +
−
  moreover+
−
    from a(2) have "th' \<noteq> th" using assms a(2) by blast +
−
  ultimately show ?thesis using that by metis+
−
qed+
−
+
−
+
−
lemma nblockedE:+
−
  assumes "th \<notin> running (t @ s)"+
−
  obtains th' where "th' \<in> ancestors (tG (t @ s)) th"+
−
                    "th' \<in> running (t @ s)"+
−
                    "th' \<in> threads s"+
−
                    "\<not>detached s th'"+
−
                    "cp (t @ s) th' = preced th s"+
−
                    "th' \<noteq> th"+
−
using blockedE unfolding nancestors_def+
−
using assms nancestors3 by auto+
−
+
−
+
−
lemma detached_not_running:+
−
  assumes "detached (t @ s) th'"+
−
  and "th' \<noteq> th"+
−
  shows "th' \<notin> running (t @ s)"+
−
proof+
−
    assume otherwise: "th' \<in> running (t @ s)"+
−
    have "cp (t@s) th' = cp (t@s) th"+
−
    proof -+
−
      have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" using otherwise+
−
          by (simp add:running_def)+
−
      moreover have "cp (t@s) th = ..." by (simp add: vat_t.max_cp_readys_threads)+
−
      ultimately show ?thesis by simp+
−
    qed+
−
    moreover have "cp (t@s) th' = preced th' (t@s)" using assms(1)+
−
      by (simp add: detached_cp_preced)+
−
    moreover have "cp (t@s) th = preced th (t@s)" by simp+
−
    ultimately have "preced th' (t@s) = preced th (t@s)" by simp+
−
    from preced_unique[OF this] +
−
    have "th' \<in> threads (t @ s) \<Longrightarrow> th \<in> threads (t @ s) \<Longrightarrow> th' = th" .+
−
    moreover have "th' \<in> threads (t@s)" +
−
      using otherwise by (unfold running_def readys_def, auto)+
−
    moreover have "th \<in> threads (t@s)" by (simp add: th_kept) +
−
    ultimately have "th' = th" by metis+
−
    with assms(2) show False by simp+
−
qed+
−
+
−
section {* The correctness theorem of PIP *}+
−
+
−
text {*+
−
+
−
  In this section, we identify two more conditions in addition to the ones+
−
  already specified in the current locale, based on which the correctness+
−
  of PIP is formally proved.+
−
+
−
  Note that Priority Inversion refers to the phenomenon where the thread+
−
  with highest priority is blocked by one with lower priority because the+
−
  resource it is requesting is currently held by the later. The objective of+
−
  PIP is to avoid {\em Indefinite Priority Inversion}, i.e. the number of+
−
  occurrences of {\em Priority Inversion} becomes indefinitely large.+
−
+
−
  For PIP to be correct, a finite upper bound needs to be found for the+
−
  occurrence number, and the existence. This section makes explicit two more+
−
  conditions so that the existence of such a upper bound can be proved to+
−
  exist. *}+
−
+
−
text {*+
−
  The following set @{text "blockers"} characterizes the set of threads which +
−
  might block @{term th} in @{term t}:+
−
*}+
−
+
−
definition "blockers = {th'. \<not>detached s th' \<and> th' \<noteq> th}"+
−
+
−
text {*+
−
  The following lemma shows that the definition of @{term "blockers"} is correct, +
−
  i.e. blockers do block @{term "th"}. It is a very simple corollary of @{thm blockedE}.+
−
*}+
−
lemma runningE:+
−
  assumes "th' \<in> running (t@s)"+
−
  obtains (is_th) "th' = th"+
−
        | (is_other) "th' \<in> blockers"+
−
  using assms blockers_def running_inversion(2) by auto+
−
+
−
text {*+
−
  The following lemma shows that the number of blockers are finite.+
−
  The reason is simple, because blockers are subset of thread set, which+
−
  has been shown finite.+
−
*}+
−
+
−
lemma finite_blockers: "finite blockers"+
−
proof -+
−
  have "finite {th'. \<not>detached s th'}"+
−
  proof -+
−
    have "finite {th'. Th th' \<in> Field (RAG s)}"+
−
    proof -+
−
      have "{th'. Th th' \<in> Field (RAG s)} \<subseteq> threads s"+
−
      proof+
−
        fix x+
−
        assume "x \<in> {th'. Th th' \<in> Field (RAG s)}"+
−
        thus "x \<in> threads s" using vat_s.RAG_threads by auto+
−
      qed+
−
      moreover have "finite ..." by (simp add: vat_s.finite_threads) +
−
      ultimately show ?thesis using rev_finite_subset by auto +
−
    qed+
−
    thus ?thesis by (unfold detached_test, auto)+
−
  qed+
−
  thus ?thesis unfolding blockers_def by simp+
−
qed+
−
+
−
text {* The following lemma shows that a blocker does not die as long as the+
−
highest thread @{term th} is live.+
−
+
−
  The reason for this is that, before a thread can execute an @{term Exit}+
−
  operation, it must give up all its resource. However, the high priority+
−
  inherited by a blocker thread also goes with the resources it once held,+
−
  and the consequence is the lost of right to run, the other precondition+
−
  for it to execute its own @{term Exit} operation. For this reason, a+
−
  blocker may never exit before the exit of the highest thread @{term th}.+
−
*}+
−
+
−
lemma blockers_kept:+
−
  assumes "th' \<in> blockers"+
−
  shows "th' \<in> threads (t@s)"+
−
proof(induct rule:ind)+
−
  case Nil+
−
  from assms[unfolded blockers_def detached_test]+
−
  have "Th th' \<in> Field (RAG s)" by simp+
−
  from vat_s.RAG_threads[OF this]+
−
  show ?case by simp+
−
next+
−
  case h: (Cons e t)+
−
  interpret et: extend_highest_gen s th prio tm t+
−
    using h by simp+
−
  show ?case+
−
  proof -+
−
    { assume otherwise: "th' \<notin> threads ((e # t) @ s)"+
−
      from threads_Exit[OF h(5)] this have eq_e: "e = Exit th'" by auto+
−
      from h(2)[unfolded this]+
−
      have False+
−
      proof(cases)+
−
        case h: (thread_exit)+
−
        hence "th' \<in> readys (t@s)" by (auto simp:running_def)+
−
        from readys_holdents_detached[OF this h(2)]+
−
        have "detached (t @ s) th'" .+
−
        from et.detached_not_running[OF this] assms[unfolded blockers_def]+
−
        have "th' \<notin> running (t @ s)" by auto+
−
        with h(1) show ?thesis by simp+
−
      qed+
−
    } thus ?thesis by auto+
−
  qed+
−
qed+
−
+
−
text {*+
−
  The following lemma shows that a blocker may never execute its @{term Create}-operation+
−
  during the period of @{term t}. The reason is that for a thread to be created +
−
  (or executing its @{term Create} operation), it must be non-existing (or dead). +
−
  However, since lemma @{thm blockers_kept} shows that blockers are always living, +
−
  it can not be created. +
−
+
−
  A thread is created only when there is some external reason, there is need for it to run. +
−
  The precondition for this is that it has already died (or get out of existence).+
−
*}+
−
+
−
lemma blockers_no_create:+
−
  assumes "th' \<in> blockers"+
−
  and "e \<in> set t"+
−
  and "actor e = th'"+
−
  shows "\<not> isCreate e"+
−
  using assms(2,3)+
−
proof(induct rule:ind)+
−
  case h: (Cons e' t)+
−
  interpret et: extend_highest_gen s th prio tm t+
−
    using h by simp+
−
  { assume eq_e: "e = e'"+
−
    from et.blockers_kept assms+
−
    have "th' \<in> threads (t @ s)" by auto+
−
    with h(2,7)+
−
    have ?case +
−
      by (unfold eq_e, cases, auto simp:blockers_def)+
−
  } with h+
−
  show ?case by auto+
−
qed auto+
−
+
−
text {*+
−
  The following lemma shows that, same as blockers, +
−
  the highest thread @{term th} also can not execute its @{term Create}-operation.+
−
  And the reason is similar: since @{thm th_kept} says that thread @{term th} is kept live+
−
  during @{term t}, it can not (or need not) be created another time.+
−
*}+
−
lemma th_no_create:+
−
  assumes "e \<in> set t"+
−
  and "actor e = th"+
−
  shows "\<not> isCreate e"+
−
  using assms+
−
proof(induct rule:ind)+
−
  case h:(Cons e' t)+
−
  interpret et: extend_highest_gen s th prio tm t+
−
    using h by simp+
−
  { assume eq_e: "e = e'"+
−
    from et.th_kept have "th \<in> threads (t @ s)" by simp+
−
    with h(2,7)+
−
    have ?case by (unfold eq_e, cases, auto)+
−
  } with h+
−
  show ?case by auto+
−
qed auto+
−
+
−
text {*+
−
  The following is a preliminary lemma in order to show that the number of +
−
  actions (or operations) taken by the highest thread @{term th} is +
−
  less or equal to the number of occurrences when @{term th} is in running+
−
  state. What is proved in this lemma is essentially a strengthening, which +
−
  says the inequality holds even if the occurrence at the very beginning is+
−
  ignored.+
−
+
−
  The reason for this lemma is that for every operation to be executed, its actor must+
−
  be in running state. Therefore, there is one occurrence of running state+
−
  behind every action. +
−
+
−
  However, this property does not hold in general, because, for +
−
  the execution of @{term Create}-operation, the actor does not have to be in running state. +
−
  Actually, the actor must be in dead state, in order to be created. For @{term th}, this +
−
  property holds because, according to lemma @{thm th_no_create}, @{term th} can not execute+
−
  any @{term Create}-operation during the period of @{term t}.+
−
*}+
−
lemma actions_th_occs_pre:+
−
  assumes "t = e'#t'"+
−
  shows "length (actions_of {th} t) \<le> occs (\<lambda> t'. th \<in> running (t'@s)) t'"+
−
  using assms+
−
proof(induct arbitrary: e' t' rule:ind)+
−
  case h: (Cons e t e' t')+
−
  interpret vt: valid_trace "(t@s)" using h(1)+
−
    by (unfold_locales, simp)+
−
  interpret ve:  extend_highest_gen s th prio tm t using h by simp+
−
  interpret ve':  extend_highest_gen s th prio tm "e#t" using h by simp+
−
  show ?case (is "?L \<le> ?R")+
−
  proof(cases t)+
−
    case Nil+
−
    show ?thesis+
−
    proof(cases "actor e = th")+
−
      case True+
−
      from ve'.th_no_create[OF _ this]+
−
      have "\<not> isCreate e" by auto+
−
      from PIP_actorE[OF h(2) True this] Nil+
−
      have "th \<in> running s" by simp+
−
      hence "?R = 1" using Nil h by simp+
−
      moreover have "?L = 1" using True Nil by (simp add:actions_of_def)+
−
      ultimately show ?thesis by simp+
−
    next+
−
      case False+
−
      with Nil+
−
      show ?thesis by (auto simp:actions_of_def)+
−
    qed+
−
  next+
−
    case h1: (Cons e1 t1)+
−
    hence eq_t': "t' = e1#t1" using h by simp+
−
    from h(5)[OF h1]+
−
    have le: "length (actions_of {th} t) \<le> occs (\<lambda>t'. th \<in> running (t' @ s)) t1" +
−
      (is "?F t \<le> ?G t1") .+
−
    show ?thesis +
−
    proof(cases "actor e = th")+
−
      case True+
−
      from ve'.th_no_create[OF _ this]+
−
      have "\<not> isCreate e" by auto+
−
      from PIP_actorE[OF h(2) True this]+
−
      have "th \<in> running (t@s)" by simp+
−
      hence "?R = 1 + ?G t1" by (unfold h1 eq_t', simp)+
−
      moreover have "?L = 1 + ?F t" using True by (simp add:actions_of_def)+
−
      ultimately show ?thesis using le by simp+
−
    next+
−
      case False+
−
      with le+
−
      show ?thesis by (unfold h1 eq_t', simp add:actions_of_def)+
−
    qed+
−
  qed+
−
qed auto+
−
+
−
text {*+
−
  The following lemma is a simple corollary of @{thm actions_th_occs_pre}. It is the+
−
  lemma really needed in later proofs.+
−
*}+
−
lemma actions_th_occs:+
−
  shows "length (actions_of {th} t) \<le> occs (\<lambda> t'. th \<in> running (t'@s)) t"+
−
proof(cases t)+
−
  case (Cons e' t')+
−
  from actions_th_occs_pre[OF this]+
−
  have "length (actions_of {th} t) \<le> occs (\<lambda>t'. th \<in> running (t' @ s)) t'" .+
−
  moreover have "... \<le> occs (\<lambda>t'. th \<in> running (t' @ s)) t" +
−
    by (unfold Cons, auto)+
−
  ultimately show ?thesis by simp+
−
qed (auto simp:actions_of_def)+
−
+
−
text {*+
−
  The following lemma splits all the operations in @{term t} into three+
−
  disjoint sets, namely the operations of @{term th}, the operations of +
−
  blockers and @{term Create}-operations. These sets are mutually disjoint+
−
  because: @{term "{th}"} and @{term blockers} are disjoint by definition, +
−
  and neither @{term th} nor any blocker can execute @{term Create}-operation+
−
  (according to lemma @{thm th_no_create} and @{thm blockers_no_create}).+
−
+
−
  One important caveat noted by this lemma is that: +
−
  Although according to assumption @{thm create_low}, each thread created in +
−
  @{term t} has precedence lower than @{term th}, therefore, will get no+
−
  change to run after creation, therefore, can not acquire any resource +
−
  to become a blocker, the @{term Create}-operations of such +
−
  lower threads may still consume overall execution time of duration @{term t}, therefore,+
−
  may compete for execution time with the most urgent thread @{term th}.+
−
  For PIP to be correct, the number of such competing operations needs to be +
−
  bounded somehow.+
−
*}+
−
+
−
lemma actions_split:+
−
  "length t = length (actions_of {th} t) + +
−
              length (actions_of blockers t) + +
−
              length (filter (isCreate) t)"+
−
proof(induct rule:ind)+
−
  case h: (Cons e t)+
−
  interpret ve :  extend_highest_gen s th prio tm t using h by simp+
−
  interpret ve':  extend_highest_gen s th prio tm "e#t" using h by simp+
−
  show ?case (is "?L (e#t) = ?T (e#t) + ?O (e#t) + ?C (e#t)")+
−
  proof(cases "actor e \<in> running (t@s)")+
−
    case True+
−
    thus ?thesis+
−
    proof(rule ve.runningE)+
−
      assume 1: "actor e = th"+
−
      have "?T (e#t) = 1 + ?T (t)" using 1 by (simp add:actions_of_def)+
−
      moreover have "?O (e#t) = ?O t" +
−
      proof -+
−
        have "actor e \<notin> blockers" using 1+
−
          by (simp add:actions_of_def blockers_def)+
−
        thus ?thesis by (simp add:actions_of_def)+
−
      qed+
−
      moreover have "?C (e#t) = ?C t"+
−
      proof -+
−
        from ve'.th_no_create[OF _ 1]+
−
        have "\<not> isCreate e" by auto+
−
        thus ?thesis by (simp add:actions_of_def)+
−
      qed+
−
      ultimately show ?thesis using h by simp+
−
    next+
−
      assume 2: "actor e \<in> ve'.blockers"+
−
      have "?T (e#t) = ?T (t)"+
−
      proof -+
−
        from 2 have "actor e \<noteq> th" by (auto simp:blockers_def)+
−
        thus ?thesis by (auto simp:actions_of_def)+
−
      qed+
−
      moreover have "?O (e#t) = 1 + ?O(t)" using 2+
−
        by (auto simp:actions_of_def)+
−
      moreover have "?C (e#t) = ?C(t)"+
−
      proof -+
−
        from ve'.blockers_no_create[OF 2, of e]+
−
        have "\<not> isCreate e" by auto+
−
        thus ?thesis by (simp add:actions_of_def)+
−
      qed+
−
      ultimately show ?thesis using h by simp+
−
    qed+
−
  next+
−
    case False+
−
    from h(2)+
−
    have is_create: "isCreate e"+
−
      by (cases; insert False, auto)+
−
    have "?T (e#t) = ?T t"+
−
    proof -+
−
      have "actor e \<noteq> th"+
−
      proof+
−
        assume "actor e = th"+
−
        from ve'.th_no_create[OF _ this]+
−
        have "\<not> isCreate e" by auto+
−
        with is_create show False by simp+
−
      qed+
−
      thus ?thesis by (auto simp:actions_of_def)+
−
    qed+
−
    moreover have "?O (e#t) = ?O t"+
−
    proof -+
−
      have "actor e \<notin> blockers"+
−
      proof+
−
        assume "actor e \<in> blockers"+
−
        from ve'.blockers_no_create[OF this, of e]+
−
        have "\<not> isCreate e" by simp+
−
        with is_create show False by simp+
−
      qed+
−
      thus ?thesis by (simp add:actions_of_def)+
−
    qed+
−
    moreover have "?C (e#t) = 1 + ?C t" using is_create+
−
        by (auto simp:actions_of_def)+
−
    ultimately show ?thesis using h by simp+
−
  qed+
−
qed (auto simp:actions_of_def)+
−
+
−
text {*+
−
  By combining several of forging lemmas, this lemma gives a upper bound+
−
  of the occurrence number when the most urgent thread @{term th} is blocked.+
−
+
−
  It says, the occasions when @{term th} is blocked during period @{term t} +
−
  is no more than the number of @{term Create}-operations and +
−
  the operations taken by blockers plus one. +
−
+
−
  Since the length of @{term t} may extend indefinitely, if @{term t} is full+
−
  of the above mentioned blocking operations, @{term th} may have not chance to run. +
−
  And, since @{term t} can extend indefinitely, @{term th} my be blocked indefinitely +
−
  with the growth of @{term t}. Therefore, this lemma alone does not ensure +
−
  the correctness of PIP. +
−
+
−
*}+
−
+
−
theorem bound_priority_inversion:+
−
  "occs (\<lambda> t'. th \<notin> running (t'@s)) t \<le> +
−
          1 + (length (actions_of blockers t) + length (filter (isCreate) t))"+
−
   (is "?L \<le> ?R")+
−
proof - +
−
  let ?Q = "(\<lambda> t'. th \<in> running (t'@s))"+
−
  from occs_le[of ?Q t] +
−
  thm occs_le+
−
  have "?L \<le> (1 + length t) - occs ?Q t" by simp+
−
  also have "... \<le> ?R"+
−
  proof -+
−
  thm actions_th_occs actions_split+
−
    have "length t - (length (actions_of blockers t) + length (filter (isCreate) t))+
−
              \<le> occs (\<lambda> t'. th \<in> running (t'@s)) t" (is "?L1 \<le> ?R1")+
−
    proof -+
−
      from actions_split have "?L1 = length (actions_of {th} t)" using actions_split by arith+
−
      also have "... \<le> ?R1" using actions_th_occs by simp+
−
      finally show ?thesis .+
−
    qed            +
−
    thus ?thesis by simp+
−
  qed+
−
  finally show ?thesis .+
−
qed+
−
+
−
end+
−
+
−
text {*+
−
  As explained before, lemma @{text bound_priority_inversion} alone does not+
−
  ensure the correctness of PIP. For PIP to be correct, the number of blocking operations +
−
  (by {\em blocking operation}, we mean the @{term Create}-operations and +
−
           operations taken by blockers) has to be bounded somehow.+
−
+
−
  And the following lemma is for this purpose.+
−
*}+
−
+
−
locale bounded_extend_highest = extend_highest_gen + +
−
  -- {*+
−
    To bound operations of blockers, the locale specifies that each blocker +
−
    releases all resources and becomes detached after a certain number +
−
    of operations. In the assumption, this number is given by the +
−
    existential variable @{text span}. Notice that this number is fixed for each +
−
    blocker regardless of any particular instance of @{term t} in which it operates.+
−
    +
−
    This assumption is reasonable, because it is a common sense that +
−
    the total number of operations take by any standalone thread (or process) +
−
    is only determined by its own input, and should not be affected by +
−
    the particular environment in which it operates. In this particular case,+
−
    we regard the @{term t} as the environment of thread @{term th}.+
−
  *}+
−
  assumes finite_span:+
−
          "th' \<in> blockers \<Longrightarrow>+
−
                 (\<exists> span. \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> +
−
                                  \<not> detached (t'@s) th' \<longrightarrow> length (actions_of {th'} t') < span)"+
−
+
−
  -- {*+
−
    The difference between this @{text finite_span} and the former one is to allow the number+
−
    of action steps to change with execution paths (i.e. different value of @{term "t'@s"}}).+
−
    The @{term span} is a upper bound on these step numbers. +
−
  *}+
−
+
−
  fixes BC+
−
  -- {* +
−
  The following assumption requires the number of @{term Create}-operations is +
−
  less or equal to @{term BC} regardless of any particular extension of @{term t}.+
−
+
−
   Although this assumption might seem doubtful at first sight, it is necessary +
−
   to ensure the occasions when @{term th} is blocked to be finite. Just consider+
−
   the extreme case when @{term Create}-operations consume all the time in duration +
−
   @{term "t"} and leave no space for neither @{term "th"} nor blockers to operate.+
−
   An investigate of the precondition for @{term Create}-operation in the definition +
−
   of @{term PIP} may reveal that such extreme cases are well possible, because it +
−
   is only required the thread to be created be a fresh (or dead one), and there +
−
   are infinitely many such threads. +
−
+
−
   However, if we relax the correctness criterion of PIP, allowing @{term th} to be +
−
   blocked indefinitely while still attaining a certain portion of @{term t} to complete +
−
   its task, then this bound @{term BC} can be lifted to function depending on @{term t}+
−
   where @{text "BC t"} is of a certain proportion of @{term "length t"}.+
−
  *}+
−
  assumes finite_create: +
−
          "\<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> length (filter isCreate t') \<le> BC"+
−
begin +
−
+
−
text {*+
−
  The following lemmas show that the number of @{term Create}-operations is bound by @{term BC}:+
−
*}+
−
+
−
lemma create_bc: +
−
  shows "length (filter isCreate t) \<le> BC"+
−
    by (meson extend_highest_gen_axioms finite_create)+
−
+
−
text {*+
−
  The following @{term span}-function gives the upper bound of +
−
  operations take by each particular blocker.+
−
*}+
−
definition "span th' = (SOME span.+
−
         \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> +
−
                  \<not> detached (t'@s) th' \<longrightarrow> length (actions_of {th'} t') < span)"+
−
+
−
text {*+
−
  The following lemmas shows the correctness of @{term span}, i.e. +
−
  the number of operations of taken by @{term th'} is given by +
−
  @{term "span th"}.+
−
+
−
  The reason for this lemma is that since @{term th'} gives up all resources +
−
  after @{term "span th'"} operations and becomes detached,+
−
  its inherited high priority is lost, with which the right to run goes as well.+
−
*}+
−
lemma le_span:+
−
  assumes "th' \<in> blockers"+
−
  shows "length (actions_of {th'} t) \<le> span th'"+
−
proof -+
−
  from finite_span[OF assms(1)] obtain span' +
−
  where span': "\<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> +
−
                       \<not> detached (t'@s) th' \<longrightarrow> length (actions_of {th'} t') < span'" (is "?P span'")+
−
                     by auto+
−
  have "length (actions_of {th'} t) \<le> (SOME span. ?P span)"+
−
  proof(rule someI2[where a = span'])+
−
    fix span+
−
    assume fs: "?P span" +
−
    show "length (actions_of {th'} t) \<le> span"+
−
    proof(induct rule:ind)+
−
      case h: (Cons e t)+
−
        interpret ve':  extend_highest_gen s th prio tm "e#t" using h by simp+
−
      show ?case+
−
      proof(cases "detached (t@s) th'")+
−
        case True+
−
        have "actor e \<noteq> th'"+
−
        proof+
−
          assume otherwise: "actor e = th'"+
−
          from ve'.blockers_no_create [OF assms _ this]+
−
          have "\<not> isCreate e" by auto+
−
          from PIP_actorE[OF h(2) otherwise this]+
−
          have "th' \<in> running (t @ s)" .+
−
          moreover have "th' \<notin> running (t @ s)"+
−
          proof -+
−
            from extend_highest_gen.detached_not_running[OF h(3) True] assms+
−
            show ?thesis by (auto simp:blockers_def)+
−
          qed+
−
          ultimately show False by simp+
−
        qed+
−
        with h show ?thesis by (auto simp:actions_of_def)+
−
      next+
−
        case False+
−
        from fs[rule_format, OF h(3) this] and actions_of_len_cons+
−
        show ?thesis by (meson discrete order.trans) +
−
      qed+
−
    qed (simp add: actions_of_def)+
−
  next+
−
    from span'+
−
    show "?P span'" .+
−
  qed+
−
  thus ?thesis by (unfold span_def, auto)+
−
qed+
−
+
−
text {*+
−
  The following lemma is a corollary of @{thm le_span}, which says +
−
  the total operations of blockers is bounded by the +
−
  sum of @{term span}-values of all blockers.+
−
*}+
−
lemma len_action_blockers: +
−
  "length (actions_of blockers t) \<le> (\<Sum> th' \<in> blockers . span th')"+
−
    (is "?L \<le> ?R")+
−
proof -+
−
  from len_actions_of_sigma[OF finite_blockers]+
−
  have "?L  = (\<Sum>th'\<in>blockers. length (actions_of {th'} t))" by simp+
−
  also have "... \<le> ?R"+
−
    by (rule Groups_Big.setsum_mono, insert le_span, auto)+
−
  finally show ?thesis .+
−
qed+
−
+
−
text {*+
−
  By combining forgoing lemmas, it is proved that the number of +
−
  blocked occurrences of the most urgent thread @{term th} is finitely bounded:+
−
*}+
−
theorem priority_inversion_is_finite:+
−
  "occs (\<lambda> t'. th \<notin> running (t'@s)) t \<le> +
−
          1 + ((\<Sum> th' \<in> blockers . span th') + BC)" (is "?L \<le> ?R" is "_ \<le> 1 + (?A + ?B)" )+
−
proof -+
−
  from bound_priority_inversion+
−
  have "?L \<le> 1 + (length (actions_of blockers t) + length (filter isCreate t))" +
−
      (is "_ \<le> 1 + (?A' + ?B')") .+
−
  moreover have "?A' \<le> ?A" using len_action_blockers .+
−
  moreover have "?B' \<le> ?B" using create_bc .+
−
  ultimately show ?thesis by simp+
−
qed+
−
+
−
text {*+
−
  The following lemma says the most urgent thread @{term th} will get as many +
−
  as operations it wishes, provided @{term t} is long enough. +
−
  Similar result can also be obtained under the slightly weaker assumption where+
−
  @{term BC} is lifted to a function and @{text "BC t"} is a portion of +
−
  @{term "length t"}.+
−
*}+
−
theorem enough_actions_for_the_highest:+
−
  "length t - ((\<Sum> th' \<in> blockers . span th') + BC) \<le> length (actions_of {th} t)"+
−
  using actions_split create_bc len_action_blockers by linarith+
−
+
−
thm actions_split+
−
+
−
end+
−
+
−
+
−
+
−
+
−
end+
−