theory Correctnessimports PIPBasicsbeginlemma 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 assmsby (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 simpnext 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) qedtext {* 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_genbegintext {* @{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 autoqedlemma 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 presburgerlemma 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)endlocale 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 qedqedcontext extend_highest_genbegin 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 qedqedlemma 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 qedqedtext {* 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 simpnext 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 qedqedlemma 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 .qedlemma 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 presburgerlemma [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 autolemma [simp]: "the_preced (t@s) th = preced th (t@s)" using the_preced_def by autolemma [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 assmsby (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 .qedtext {* 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 qedqedtext {* 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 qedqed (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 assmsproof - -- {* 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 autoqedtext {* 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 simpqedtext {* 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 simpnext from running_preced_inversion[OF running'] show "cp (t@s) th' = preced th s" .qedsection {* 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 metisqedlemma th_blockedE_pretty: shows "\<exists>th' \<in> nancestors (tG (t @ s)) th. th' \<in> running (t @ s)"using th_blockedE assms by blasttext {* 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 autolemma 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 metisqedlemma 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_defusing assms nancestors3 by autolemma 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 simpqedsection {* 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 autotext {* 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 simpqedtext {* The following lemma shows that a blocker does not die as long as thehighest 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 simpnext 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 qedqedtext {* 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 autoqed autotext {* 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 assmsproof(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 autoqed autotext {* 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 assmsproof(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 qedqed autotext {* 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 simpqed (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 qedqed (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] have "?L \<le> (1 + length t) - occs ?Q t" by simp also have "... \<le> ?R" proof - 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 - 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 .qedvalue "sublists [a,b,cThe]"theorem bound_priority_inversion: "card { s' @ s | s'. s' \<in> set t \<and> th \<notin> running (s'@s) } \<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] have "?L \<le> (1 + length t) - occs ?Q t" by simp also have "... \<le> ?R" proof - 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 - 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 .qedendtext {* 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)qedtext {* 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 .qedtext {* 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 simpqedtext {* 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 linarithendend