theory ExtGGimports PrioG CpsGbegintext {* The following two auxiliary lemmas are used to reason about @{term Max}.*}lemma image_Max_eqI: assumes "finite B" and "b \<in> B" and "\<forall> x \<in> B. f x \<le> f b" shows "Max (f ` B) = f b" using assms using Max_eqI by blast lemma image_Max_subset: assumes "finite A" and "B \<subseteq> A" and "a \<in> B" and "Max (f ` A) = f a" shows "Max (f ` B) = f a"proof(rule image_Max_eqI) show "finite B" using assms(1) assms(2) finite_subset by auto next show "a \<in> B" using assms by 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)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 autoqed(* ccc *)lemma highest_cp_preced: "cp s th = Max ((\<lambda> th'. preced th' s) ` threads s)" by (fold max_cp_eq, unfold eq_cp_s_th, insert highest, simp)lemma highest_preced_thread: "preced th s = Max ((\<lambda> th'. preced th' s) ` threads s)" by (fold eq_cp_s_th, unfold highest_cp_preced, simp)lemma highest': "cp s th = Max (cp s ` threads s)"proof - from highest_cp_preced max_cp_eq[symmetric] show ?thesis by simpqedendlocale 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 qedqedlocale red_extend_highest_gen = extend_highest_gen + fixes i::natsublocale red_extend_highest_gen < red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)" apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric]) apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp) by (unfold highest_gen_def, auto dest:step_back_vt_app)context extend_highest_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 living status and precedence kept along the way of @{text "t"}. The following lemma shows that this preserved precedence of @{text "th"} remains as the highest along the way of @{text "t"}. The proof goes by induction over @{text "t"} using the specialized induction rule @{thm ind}, followed by case analysis of each possible operations of PIP. All cases follow the same pattern rendered by the generalized introduction rule @{thm "image_Max_eqI"}. The very essence is to show that precedences, no matter whether they are newly introduced or modified, are always lower than the one held by @{term "th"}, which by @{thm th_kept} is preserved along the way.*}lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"proof(induct rule:ind) case Nil from highest_preced_thread show ?case by (unfold the_preced_def, simp)next case (Cons e t) interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto show ?case proof(cases e) case (Create thread prio') show ?thesis (is "Max (?f ` ?A) = ?t") proof - -- {* The following is the common pattern of each branch of the case analysis. *} -- {* The major part is to show that @{text "th"} holds the highest precedence: *} have "Max (?f ` ?A) = ?f th" proof(rule image_Max_eqI) show "finite ?A" using h_e.finite_threads by auto next show "th \<in> ?A" using h_e.th_kept by auto next show "\<forall>x\<in>?A. ?f x \<le> ?f th" proof fix x assume "x \<in> ?A" hence "x = thread \<or> x \<in> threads (t@s)" by (auto simp:Create) thus "?f x \<le> ?f th" proof assume "x = thread" thus ?thesis apply (simp add:Create the_preced_def preced_def, fold preced_def) using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 preced_th by force next assume h: "x \<in> threads (t @ s)" from Cons(2)[unfolded Create] have "x \<noteq> thread" using h by (cases, auto) hence "?f x = the_preced (t@s) x" by (simp add:Create the_preced_def preced_def) hence "?f x \<le> Max (the_preced (t@s) ` threads (t@s))" by (simp add: h_t.finite_threads h) also have "... = ?f th" by (metis Cons.hyps(5) h_e.th_kept the_preced_def) finally show ?thesis . qed qed qed -- {* The minor part is to show that the precedence of @{text "th"} equals to preserved one, given by the foregoing lemma @{thm th_kept} *} also have "... = ?t" using h_e.th_kept the_preced_def by auto -- {* Then it follows trivially that the precedence preserved for @{term "th"} remains the maximum of all living threads along the way. *} finally show ?thesis . qed next case (Exit thread) show ?thesis (is "Max (?f ` ?A) = ?t") proof - have "Max (?f ` ?A) = ?f th" proof(rule image_Max_eqI) show "finite ?A" using h_e.finite_threads by auto next show "th \<in> ?A" using h_e.th_kept by auto next show "\<forall>x\<in>?A. ?f x \<le> ?f th" proof fix x assume "x \<in> ?A" hence "x \<in> threads (t@s)" by (simp add: Exit) hence "?f x \<le> Max (?f ` threads (t@s))" by (simp add: h_t.finite_threads) also have "... \<le> ?f th" apply (simp add:Exit the_preced_def preced_def, fold preced_def) using Cons.hyps(5) h_t.th_kept the_preced_def by auto finally show "?f x \<le> ?f th" . qed qed also have "... = ?t" using h_e.th_kept the_preced_def by auto finally show ?thesis . qed next case (P thread cs) with Cons show ?thesis by (auto simp:preced_def the_preced_def) next case (V thread cs) with Cons show ?thesis by (auto simp:preced_def the_preced_def) next case (Set thread prio') show ?thesis (is "Max (?f ` ?A) = ?t") proof - have "Max (?f ` ?A) = ?f th" proof(rule image_Max_eqI) show "finite ?A" using h_e.finite_threads by auto next show "th \<in> ?A" using h_e.th_kept by auto next show "\<forall>x\<in>?A. ?f x \<le> ?f th" proof fix x assume h: "x \<in> ?A" show "?f x \<le> ?f th" proof(cases "x = thread") case True moreover have "the_preced (Set thread prio' # t @ s) thread \<le> the_preced (t @ s) th" proof - have "the_preced (t @ s) th = Prc prio tm" using h_t.th_kept preced_th by (simp add:the_preced_def) moreover have "prio' \<le> prio" using Set h_e.set_diff_low by auto ultimately show ?thesis by (insert lt_tm, auto simp:the_preced_def preced_def) qed ultimately show ?thesis by (unfold Set, simp add:the_preced_def preced_def) next case False then have "?f x = the_preced (t@s) x" by (simp add:the_preced_def preced_def Set) also have "... \<le> Max (the_preced (t@s) ` threads (t@s))" using Set h h_t.finite_threads by auto also have "... = ?f th" by (metis Cons.hyps(5) h_e.th_kept the_preced_def) finally show ?thesis . qed qed qed also have "... = ?t" using h_e.th_kept the_preced_def by auto finally show ?thesis . qed 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 (smt Collect_cong Setcompr_eq_image mem_Collect_eq the_thread.simps) moreover have "finite ..." by (simp add: vat_t.fsbtRAGs.finite_subtree) ultimately show ?thesis by simp qed next show "th \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}" by (auto simp:subtree_def) next show "\<forall>x\<in>{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}. the_preced (t @ s) x \<le> the_preced (t @ s) th" proof fix th' assume "th' \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}" hence "Th th' \<in> subtree (RAG (t @ s)) (Th th)" by auto moreover have "... \<subseteq> Field (RAG (t @ s)) \<union> {Th th}" by (meson subtree_Field) ultimately have "Th th' \<in> ..." by auto hence "th' \<in> threads (t@s)" proof assume "Th th' \<in> {Th th}" thus ?thesis using th_kept by auto next assume "Th th' \<in> Field (RAG (t @ s))" thus ?thesis using vat_t.not_in_thread_isolated by blast qed thus "the_preced (t @ s) th' \<le> the_preced (t @ s) th" by (metis Max_ge finite_imageI finite_threads image_eqI max_kept th_kept the_preced_def) qed qed also have "... = ?R" by (simp add: max_preced the_preced_def) finally show ?thesis .qedlemma th_cp_max: "cp (t@s) th = Max (cp (t@s) ` threads (t@s))" using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburgerlemma th_cp_preced: "cp (t@s) th = preced th s" by (fold max_kept, unfold th_cp_max_preced, simp)lemma preced_less: assumes th'_in: "th' \<in> threads s" and neq_th': "th' \<noteq> th" shows "preced th' s < preced th s" using 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)text {* Counting of the number of @{term "P"} and @{term "V"} operations is the cornerstone of a large number of the following proofs. The reason is that this counting is quite easy to calculate and convenient to use in the reasoning. The following lemma shows that the counting controls whether a thread is running or not.*}lemma pv_blocked_pre: assumes th'_in: "th' \<in> threads (t@s)" and neq_th': "th' \<noteq> th" and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" shows "th' \<notin> runing (t@s)"proof assume otherwise: "th' \<in> runing (t@s)" show False proof - have "th' = th" proof(rule preced_unique) show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R") proof - have "?L = cp (t@s) th'" by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp) also have "... = cp (t @ s) th" using otherwise by (metis (mono_tags, lifting) mem_Collect_eq runing_def th_cp_max vat_t.max_cp_readys_threads) also have "... = ?R" by (metis th_cp_preced th_kept) finally show ?thesis . qed qed (auto simp: th'_in th_kept) moreover have "th' \<noteq> th" using neq_th' . ultimately show ?thesis by simp qedqedlemmas pv_blocked = pv_blocked_pre[folded detached_eq]lemma runing_precond_pre: fixes th' assumes th'_in: "th' \<in> threads s" and eq_pv: "cntP s th' = cntV s th'" and neq_th': "th' \<noteq> th" shows "th' \<in> threads (t@s) \<and> cntP (t@s) th' = cntV (t@s) th'"proof(induct rule:ind) case (Cons e t) 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 show ?case proof(cases e) case (P thread cs) show ?thesis proof - have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" proof - have "thread \<noteq> th'" proof - have "step (t@s) (P thread cs)" using Cons P by auto thus ?thesis proof(cases) assume "thread \<in> runing (t@s)" moreover have "th' \<notin> runing (t@s)" using Cons(5) by (metis neq_th' vat_t.pv_blocked_pre) ultimately show ?thesis by auto qed qed with Cons show ?thesis by (unfold P, simp add:cntP_def cntV_def count_def) qed moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold P, simp) ultimately show ?thesis by auto qed next case (V thread cs) show ?thesis proof - have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" proof - have "thread \<noteq> th'" proof - have "step (t@s) (V thread cs)" using Cons V by auto thus ?thesis proof(cases) assume "thread \<in> runing (t@s)" moreover have "th' \<notin> runing (t@s)" using Cons(5) by (metis neq_th' vat_t.pv_blocked_pre) ultimately show ?thesis by auto qed qed with Cons show ?thesis by (unfold V, simp add:cntP_def cntV_def count_def) qed moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold V, simp) ultimately show ?thesis by auto qed next case (Create thread prio') show ?thesis proof - have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" proof - have "thread \<noteq> th'" proof - have "step (t@s) (Create thread prio')" using Cons Create by auto thus ?thesis using Cons(5) by (cases, auto) qed with Cons show ?thesis by (unfold Create, simp add:cntP_def cntV_def count_def) qed moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold Create, simp) ultimately show ?thesis by auto qed next case (Exit thread) show ?thesis proof - have neq_thread: "thread \<noteq> th'" proof - have "step (t@s) (Exit thread)" using Cons Exit by auto thus ?thesis apply (cases) using Cons(5) by (metis neq_th' vat_t.pv_blocked_pre) qed hence "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" using Cons by (unfold Exit, simp add:cntP_def cntV_def count_def) moreover have "th' \<in> threads ((e # t) @ s)" using Cons neq_thread by (unfold Exit, simp) ultimately show ?thesis by auto qed next case (Set thread prio') with Cons show ?thesis by (auto simp:cntP_def cntV_def count_def) qednext case Nil with assms show ?case by autoqedtext {* Changing counting balance to detachedness *}lemmas runing_precond_pre_dtc = runing_precond_pre [folded vat_t.detached_eq vat_s.detached_eq]lemma runing_precond: fixes th' assumes th'_in: "th' \<in> threads s" and neq_th': "th' \<noteq> th" and is_runing: "th' \<in> runing (t@s)" shows "cntP s th' > cntV s th'" using assmsproof - have "cntP s th' \<noteq> cntV s th'" by (metis is_runing neq_th' pv_blocked_pre runing_precond_pre th'_in) moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto ultimately show ?thesis by autoqedlemma moment_blocked_pre: assumes neq_th': "th' \<noteq> th" and th'_in: "th' \<in> threads ((moment i t)@s)" and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" shows "cntP ((moment (i+j) t)@s) th' = cntV ((moment (i+j) t)@s) th' \<and> th' \<in> threads ((moment (i+j) t)@s)"proof - interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales) interpret h_j: red_extend_highest_gen _ _ _ _ _ "i+j" by (unfold_locales) interpret h: extend_highest_gen "((moment i t)@s)" th prio tm "moment j (restm i t)" proof(unfold_locales) show "vt (moment i t @ s)" by (metis h_i.vt_t) next show "th \<in> threads (moment i t @ s)" by (metis h_i.th_kept) next show "preced th (moment i t @ s) = Max (cp (moment i t @ s) ` threads (moment i t @ s))" by (metis h_i.th_cp_max h_i.th_cp_preced h_i.th_kept) next show "preced th (moment i t @ s) = Prc prio tm" by (metis h_i.th_kept preced_th) next show "vt (moment j (restm i t) @ moment i t @ s)" using moment_plus_split by (metis add.commute append_assoc h_j.vt_t) next fix th' prio' assume "Create th' prio' \<in> set (moment j (restm i t))" thus "prio' \<le> prio" using assms by (metis Un_iff add.commute h_j.create_low moment_plus_split set_append) next fix th' prio' assume "Set th' prio' \<in> set (moment j (restm i t))" thus "th' \<noteq> th \<and> prio' \<le> prio" by (metis Un_iff add.commute h_j.set_diff_low moment_plus_split set_append) next fix th' assume "Exit th' \<in> set (moment j (restm i t))" thus "th' \<noteq> th" by (metis Un_iff add.commute h_j.exit_diff moment_plus_split set_append) qed show ?thesis by (metis add.commute append_assoc eq_pv h.runing_precond_pre moment_plus_split neq_th' th'_in)qedlemma moment_blocked_eqpv: assumes neq_th': "th' \<noteq> th" and th'_in: "th' \<in> threads ((moment i t)@s)" and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" and le_ij: "i \<le> j" shows "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th' \<and> th' \<in> threads ((moment j t)@s) \<and> th' \<notin> runing ((moment j t)@s)"proof - from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'" and h2: "th' \<in> threads ((moment j t)@s)" by auto moreover have "th' \<notin> runing ((moment j t)@s)" proof - interpret h: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) show ?thesis using h.pv_blocked_pre h1 h2 neq_th' by auto qed ultimately show ?thesis by autoqed(* The foregoing two lemmas are preparation for this one, but in long run can be combined. Maybe I am wrong.*)lemma moment_blocked: assumes neq_th': "th' \<noteq> th" and th'_in: "th' \<in> threads ((moment i t)@s)" and dtc: "detached (moment i t @ s) th'" and le_ij: "i \<le> j" shows "detached (moment j t @ s) th' \<and> th' \<in> threads ((moment j t)@s) \<and> th' \<notin> runing ((moment j t)@s)"proof - interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales) interpret h_j: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) have cnt_i: "cntP (moment i t @ s) th' = cntV (moment i t @ s) th'" by (metis dtc h_i.detached_elim) from moment_blocked_eqpv[OF neq_th' th'_in cnt_i le_ij] show ?thesis by (metis h_j.detached_intro) qedlemma runing_preced_inversion: assumes runing': "th' \<in> runing (t@s)" shows "cp (t@s) th' = preced th s" (is "?L = ?R")proof - have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms by (unfold runing_def, auto) also have "\<dots> = ?R" by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) finally show ?thesis .qedtext {* The situation when @{term "th"} is blocked is analyzed by the following lemmas.*}text {* The following lemmas shows the running thread @{text "th'"}, if it is different from @{term th}, must be live at the very beginning. By the term {\em the very beginning}, we mean the moment where the formal investigation starts, i.e. the moment (or state) @{term s}. *}lemma runing_inversion_0: assumes neq_th': "th' \<noteq> th" and runing': "th' \<in> runing (t@s)" shows "th' \<in> threads s"proof - -- {* The proof is by contradiction: *} { assume otherwise: "\<not> ?thesis" have "th' \<notin> runing (t @ s)" proof - -- {* Since @{term "th'"} is running at time @{term "t@s"}, so it exists that time. *} have th'_in: "th' \<in> threads (t@s)" using runing' by (simp add:runing_def readys_def) -- {* However, @{text "th'"} does not exist at very beginning. *} have th'_notin: "th' \<notin> threads (moment 0 t @ s)" using otherwise by (metis append.simps(1) moment_zero) -- {* Therefore, there must be a moment during @{text "t"}, when @{text "th'"} came into being. *} -- {* Let us suppose the moment being @{text "i"}: *} from p_split_gen[OF th'_in th'_notin] obtain i where lt_its: "i < length t" and le_i: "0 \<le> i" and pre: " th' \<notin> threads (moment i t @ s)" (is "th' \<notin> threads ?pre") and post: "(\<forall>i'>i. th' \<in> threads (moment i' t @ s))" by (auto) interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales) interpret h_i': red_extend_highest_gen _ _ _ _ _ "(Suc i)" by (unfold_locales) from lt_its have "Suc i \<le> length t" by auto -- {* Let us also suppose the event which makes this change is @{text e}: *} from moment_head[OF this] obtain e where eq_me: "moment (Suc i) t = e # moment i t" by blast hence "vt (e # (moment i t @ s))" by (metis append_Cons h_i'.vt_t) hence "PIP (moment i t @ s) e" by (cases, simp) -- {* It can be derived that this event @{text "e"}, which gives birth to @{term "th'"} must be a @{term "Create"}: *} from create_pre[OF this, of th'] obtain prio where eq_e: "e = Create th' prio" by (metis append_Cons eq_me lessI post pre) have h1: "th' \<in> threads (moment (Suc i) t @ s)" using post by auto have h2: "cntP (moment (Suc i) t @ s) th' = cntV (moment (Suc i) t@ s) th'" proof - have "cntP (moment i t@s) th' = cntV (moment i t@s) th'" by (metis h_i.cnp_cnv_eq pre) thus ?thesis by (simp add:eq_me eq_e cntP_def cntV_def count_def) qed show ?thesis using moment_blocked_eqpv [OF neq_th' h1 h2, of "length t"] lt_its moment_ge by auto qed with `th' \<in> runing (t@s)` have False by simp } thus ?thesis by autoqedtext {* The second lemma says, if the running thread @{text th'} is different from @{term th}, then this @{text th'} must in the possession of some resources at the very beginning. To ease the reasoning of resource possession of one particular thread, we used two auxiliary functions @{term cntV} and @{term cntP}, which are the counters of @{term P}-operations and @{term V}-operations respectively. If the number of @{term V}-operation is less than the number of @{term "P"}-operations, the thread must have some unreleased resource. *}lemma runing_inversion_1: (* ddd *) assumes neq_th': "th' \<noteq> th" and runing': "th' \<in> runing (t@s)" -- {* thread @{term "th'"} is a live on in state @{term "s"} and it has some unreleased resource. *} shows "th' \<in> threads s \<and> cntV s th' < cntP s th'"proof - -- {* The proof is a simple composition of @{thm runing_inversion_0} and @{thm runing_precond}: *} -- {* By applying @{thm runing_inversion_0} to assumptions, it can be shown that @{term th'} is live in state @{term s}: *} have "th' \<in> threads s" using runing_inversion_0[OF assms(1,2)] . -- {* Then the thesis is derived easily by applying @{thm runing_precond}: *} with runing_precond [OF this neq_th' runing'] show ?thesis by simpqedtext {* The following lemma is just a rephrasing of @{thm runing_inversion_1}:*}lemma runing_inversion_2: assumes runing': "th' \<in> runing (t@s)" shows "th' = th \<or> (th' \<noteq> th \<and> th' \<in> threads s \<and> cntV s th' < cntP s th')"proof - from runing_inversion_1[OF _ runing'] show ?thesis by autoqedlemma runing_inversion_3: assumes runing': "th' \<in> runing (t@s)" and neq_th: "th' \<noteq> th" shows "th' \<in> threads s \<and> (cntV s th' < cntP s th' \<and> cp (t@s) th' = preced th s)" by (metis neq_th runing' runing_inversion_2 runing_preced_inversion)lemma runing_inversion_4: assumes runing': "th' \<in> runing (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" apply (metis neq_th runing' runing_inversion_2) apply (metis neq_th pv_blocked runing' runing_inversion_2 runing_precond_pre_dtc) by (metis neq_th runing' runing_inversion_3)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 runing}-thread. However, we are going to show more: this running thread is exactly @{term "th'"}. *}lemma th_blockedE: (* ddd *) assumes "th \<notin> runing (t@s)" obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" "th' \<in> runing (t@s)"proof - -- {* According to @{thm vat_t.th_chain_to_ready}, either @{term "th"} is in @{term "readys"} or there is path leading from it to one thread in @{term "readys"}. *} have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+)" using th_kept vat_t.th_chain_to_ready by auto -- {* However, @{term th} can not be in @{term readys}, because otherwise, since @{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *} moreover have "th \<notin> readys (t@s)" using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in term @{term readys}: *} ultimately obtain th' where th'_in: "th' \<in> readys (t@s)" and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto -- {* We are going to show that this @{term th'} is running. *} have "th' \<in> runing (t@s)" proof - -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *} have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R") proof - have "?L = Max ((the_preced (t @ s) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th'))" by (unfold cp_alt_def1, simp) also have "... = (the_preced (t @ s) \<circ> the_thread) (Th th)" proof(rule image_Max_subset) show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads) next show "subtree (tRAG (t @ s)) (Th th') \<subseteq> Th ` threads (t @ s)" by (metis Range.intros dp trancl_range vat_t.range_in vat_t.subtree_tRAG_thread) next show "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp by (unfold tRAG_subtree_eq, auto simp:subtree_def) next show "Max ((the_preced (t @ s) \<circ> the_thread) ` Th ` threads (t @ s)) = (the_preced (t @ s) \<circ> the_thread) (Th th)" (is "Max ?L = _") proof - have "?L = the_preced (t @ s) ` threads (t @ s)" by (unfold image_comp, rule image_cong, auto) thus ?thesis using max_preced the_preced_def by auto qed 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 ?thesis . qed -- {* Now, since @{term th'} holds the highest @{term cp} and we have already show it is in @{term readys}, it is @{term runing} by definition. *} with `th' \<in> readys (t@s)` show ?thesis by (simp add: runing_def) qed -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *} moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) ultimately show ?thesis using that by metisqedtext {* 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: "runing (t@s) \<noteq> {}"proof(cases "th \<in> runing (t@s)") case True thus ?thesis by autonext case False thus ?thesis using th_blockedE by autoqedendend