# HG changeset patch # User Christian Urban # Date 1452823529 0 # Node ID b6ea51cd2e883301c4f78143891353219bf1ebd6 # Parent 2aa37de77f31c555aba2b2f0d3ebd4ccff969b1a some small changes to the paper diff -r 2aa37de77f31 -r b6ea51cd2e88 Correctness.thy --- a/Correctness.thy Thu Jan 14 03:29:22 2016 +0000 +++ b/Correctness.thy Fri Jan 15 02:05:29 2016 +0000 @@ -503,29 +503,29 @@ qed text {* - The following lemma shows how the counting of - @{term "P"} and @{term "V"} operations affects - the running state of threads in @{term t}. - 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 can not be in running thread. + 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' \ th"}. - The key is the use of @{thm count_eq_dependants} - to derive the emptiness of @{text th'}s @{term dependants}-set - from the balance of its @{term P} @{term V} counts. - From this, it can be shown @{text th'}s @{term cp}-value - equals to its own precedence. + The proof is by contraction with the assumption @{text "th' \ th"}. + The key is the use of @{thm count_eq_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 runing_preced_inversion}, its @{term cp}-value - equals to the precedence of @{term th}. + On the other hand, since @{text th'} is running, by @{thm + runing_preced_inversion}, its @{term cp}-value equals to the + precedence of @{term th}. - Combining the above two we have that @{text th'} and - @{term th} have the same precedence. By uniqueness of precedence, we - have @{text "th' = th"}, which is in contradiction with the - assumption @{text "th' \ 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' \ th"}. + *} lemma eq_pv_blocked: (* ddd *) diff -r 2aa37de77f31 -r b6ea51cd2e88 Correctness.thy~ --- a/Correctness.thy~ Thu Jan 14 03:29:22 2016 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,795 +0,0 @@ -theory Correctness -imports PIPBasics -begin - - -text {* - The following two auxiliary lemmas are used to reason about @{term Max}. -*} -lemma image_Max_eqI: - assumes "finite B" - and "b \ B" - and "\ x \ B. f x \ f b" - shows "Max (f ` B) = f b" - using assms - using Max_eqI by blast - -lemma image_Max_subset: - assumes "finite A" - and "B \ A" - and "a \ 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 \ B" using assms by simp -next - show "\x\B. f x \ 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 \ threads s" - and highest: "preced th s = Max ((cp s)`threads s)" - -- {* The internal structure of @{term th}'s precedence is exposed:*} - and preced_th: "preced th s = Prc prio tm" - --- {* @{term s} is a valid trace, so it will inherit all results derived for - a valid trace: *} -sublocale highest_gen < vat_s: valid_trace "s" - by (unfold_locales, insert vt_s, simp) - -context highest_gen -begin - -text {* - @{term tm} is the time when the precedence of @{term th} is set, so - @{term tm} must be a valid moment index into @{term s}. -*} -lemma lt_tm: "tm < length s" - by (insert preced_tm_lt[OF threads_s preced_th], simp) - -text {* - Since @{term th} holds the highest precedence and @{text "cp"} - is the highest precedence of all threads in the sub-tree of - @{text "th"} and @{text th} is among these threads, - its @{term cp} must equal to its precedence: -*} -lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R") -proof - - have "?L \ ?R" - by (unfold highest, rule Max_ge, - auto simp:threads_s finite_threads) - moreover have "?R \ ?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' \ set t \ prio' \ prio" - and set_diff_low: "Set th' prio' \ set t \ th' \ th \ prio' \ prio" - and exit_diff: "Exit th' \ set t \ th' \ 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) \ vt s" - and vt_et: "vt ((e # t) @ s)" - show ?case - proof(rule ih) - show "vt (t @ s)" - proof(rule step_back_vt) - from vt_et show "vt (e # t @ s)" by simp - qed - qed - qed -qed - -locale red_extend_highest_gen = extend_highest_gen + - fixes i::nat - -sublocale red_extend_highest_gen < red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)" - apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric]) - apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp) - by (unfold highest_gen_def, auto dest:step_back_vt_app) - -context extend_highest_gen -begin - - lemma ind [consumes 0, case_names Nil Cons, induct type]: - assumes - h0: "R []" - and h2: "\ e t. \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\ \ 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: "\vt (t' @ s); extend_highest_gen s th prio tm t'\ \ 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 \ threads (t @ s) \ - 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 \ 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 \ 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 \ thread" by auto - hence "preced th ((e # t) @ s) = preced th (t @ s)" - by (unfold Set, auto simp:preced_def) - moreover note Cons - ultimately show ?thesis - by (auto simp:Set) - qed - qed - qed -qed - -text {* - According to @{thm th_kept}, thread @{text "th"} has its living status - and precedence kept along the way of @{text "t"}. The following lemma - shows that this preserved precedence of @{text "th"} remains as the highest - along the way of @{text "t"}. - - The proof goes by induction over @{text "t"} using the specialized - induction rule @{thm ind}, followed by case analysis of each possible - operations of PIP. All cases follow the same pattern rendered by the - generalized introduction rule @{thm "image_Max_eqI"}. - - The very essence is to show that precedences, no matter whether they - are newly introduced or modified, are always lower than the one held - by @{term "th"}, which by @{thm th_kept} is preserved along the way. -*} -lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s" -proof(induct rule:ind) - case Nil - from highest_preced_thread - show ?case by 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 \ ?A" using h_e.th_kept by auto - next - show "\x\?A. ?f x \ ?f th" - proof - fix x - assume "x \ ?A" - hence "x = thread \ x \ threads (t@s)" by (auto simp:Create) - thus "?f x \ ?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 \ threads (t @ s)" - from Cons(2)[unfolded Create] - have "x \ 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 \ 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 \ ?A" using h_e.th_kept by auto - next - show "\x\?A. ?f x \ ?f th" - proof - fix x - assume "x \ ?A" - hence "x \ threads (t@s)" by (simp add: Exit) - hence "?f x \ Max (?f ` threads (t@s))" - by (simp add: h_t.finite_threads) - also have "... \ ?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 \ ?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 \ ?A" using h_e.th_kept by auto - next - show "\x\?A. ?f x \ ?f th" - proof - fix x - assume h: "x \ ?A" - show "?f x \ ?f th" - proof(cases "x = thread") - case True - moreover have "the_preced (Set thread prio' # t @ s) thread \ 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' \ 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 "... \ 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' \ subtree (RAG (t @ s)) (Th th)}" - proof - - have "{th'. Th th' \ subtree (RAG (t @ s)) (Th th)} = - the_thread ` {n . n \ subtree (RAG (t @ s)) (Th th) \ - (\ 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 \ {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" - by (auto simp:subtree_def) - next - show "\x\{th'. Th th' \ subtree (RAG (t @ s)) (Th th)}. - the_preced (t @ s) x \ the_preced (t @ s) th" - proof - fix th' - assume "th' \ {th'. Th th' \ subtree (RAG (t @ s)) (Th th)}" - hence "Th th' \ subtree (RAG (t @ s)) (Th th)" by auto - moreover have "... \ Field (RAG (t @ s)) \ {Th th}" - by (meson subtree_Field) - ultimately have "Th th' \ ..." by auto - hence "th' \ threads (t@s)" - proof - assume "Th th' \ {Th th}" - thus ?thesis using th_kept by auto - next - assume "Th th' \ Field (RAG (t @ s))" - thus ?thesis using vat_t.not_in_thread_isolated by blast - qed - thus "the_preced (t @ s) th' \ 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' \ threads s" - and neq_th': "th' \ 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 runing_preced_inversion: - assumes runing': "th' \ 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 "\ = ?R" - by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) - finally show ?thesis . -qed - -text {* - The following lemma shows how the counting of - @{term "P"} and @{term "V"} operations affects - the running state of threads in @{term t}. - - 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 can not be in running thread. - - The proof is by contraction with the assumption @{text "th' \ th"}. - The key is the use of @{thm count_eq_dependants} - to derive the emptiness of @{text th'}s @{term dependants}-set - from the balance of its @{term P} @{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 runing_preced_inversion}, its @{term cp}-value - equals to the precedence of @{term th}. - - Combining the above two we have that @{text th'} and - @{term th} have the same precedence. By uniqueness of precedence, we - have @{text "th' = th"}, which is in contradiction with the - assumption @{text "th' \ th"}. -*} - -lemma eq_pv_blocked: (* ddd *) - assumes neq_th': "th' \ th" - and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" - shows "th' \ runing (t@s)" -proof - assume otherwise: "th' \ runing (t@s)" - show False - proof - - have th'_in: "th' \ threads (t@s)" - using otherwise readys_threads runing_def by auto - have "th' = th" - proof(rule preced_unique) - -- {* The proof goes like this: - it is first shown that the @{term preced}-value of @{term th'} - equals to that of @{term th}, then by uniqueness - of @{term preced}-values (given by lemma @{thm preced_unique}), - @{term th'} equals to @{term th}: *} - show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R") - proof - - -- {* Since the counts of @{term th'} are balanced, the subtree - of it contains only itself, so, its @{term cp}-value - equals its @{term preced}-value: *} - have "?L = cp (t@s) th'" - by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp) - -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion}, - its @{term cp}-value equals @{term "preced th s"}, - which equals to @{term "?R"} by simplification: *} - also have "... = ?R" - thm runing_preced_inversion - using runing_preced_inversion[OF otherwise] by simp - finally show ?thesis . - qed - qed (auto simp: th'_in th_kept) - with `th' \ 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' \ 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 - 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' \ cntP (t @ s) th'" - -- {* Then the actor of @{term e} must be @{term th'} and @{term e} - must be a @{term P}-event: *} - hence "isP e" "actor e = th'" by (auto simp:cntP_diff_inv) - with vat_t.actor_inv[OF Cons(2)] - -- {* According to @{thm actor_inv}, @{term th'} must be running at - the moment @{term "t@s"}: *} - have "th' \ runing (t@s)" by (cases e, auto) - -- {* 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' \ runing (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' \ cntV (t @ s) th'" - hence "isV e" "actor e = th'" by (auto simp:cntV_diff_inv) - with vat_t.actor_inv[OF Cons(2)] - have "th' \ runing (t@s)" by (cases e, auto) - moreover have "th' \ runing (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' \ th" - and eq_pv: "cntP s th' = cntV s th'" - shows "th' \ runing (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 runing_cntP_cntV_inv: (* ddd *) - assumes is_runing: "th' \ runing (t@s)" - and neq_th': "th' \ 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' \ 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' \ runing (t@s)" . - -- {* This is obvious in contradiction with assumption @{thm is_runing} *} - thus False using is_runing by simp - qed - -- {* However, the number of @{term V} is always less or equal to @{term P}: *} - moreover have "cntV s th' \ 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 runing_threads_inv: - assumes runing': "th' \ runing (t@s)" - and neq_th': "th' \ th" - shows "th' \ threads s" -proof(rule ccontr) -- {* Proof by contradiction: *} - assume otherwise: "th' \ threads s" - have "th' \ runing (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 runing' 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 runing_inversion: (* ddd, one of the main lemmas to present *) - assumes runing': "th' \ runing (t@s)" - and neq_th: "th' \ th" - shows "th' \ threads s" - and "\detached s th'" - and "cp (t@s) th' = preced th s" -proof - - from runing_threads_inv[OF assms] - show "th' \ threads s" . -next - from runing_cntP_cntV_inv[OF runing' neq_th] - show "\detached s th'" using vat_s.detached_eq by simp -next - from runing_preced_inversion[OF runing'] - show "cp (t@s) th' = preced th s" . -qed - -section {* The existence of `blocking thread` *} - -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, the other main lemma to be presented: *) - assumes "th \ runing (t@s)" - obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" - "th' \ 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 \ readys (t @ s) \ (\th'. th' \ readys (t @ s) \ (Th th, Th th') \ (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 \ 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' \ readys (t@s)" - and dp: "(Th th, Th th') \ (RAG (t @ s))\<^sup>+" by auto - -- {* We are going to show that this @{term th'} is running. *} - have "th' \ 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) \ the_thread) ` subtree (tRAG (t @ s)) (Th th'))" - by (unfold cp_alt_def1, simp) - also have "... = (the_preced (t @ s) \ 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') \ Th ` threads (t @ s)" - by (metis Range.intros dp trancl_range vat_t.range_in vat_t.subtree_tRAG_thread) - next - show "Th th \ subtree (tRAG (t @ s)) (Th th')" using dp - by (unfold tRAG_subtree_eq, auto simp:subtree_def) - next - show "Max ((the_preced (t @ s) \ the_thread) ` Th ` threads (t @ s)) = - (the_preced (t @ s) \ 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' \ 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' \ ancestors (RAG (t @ s)) (Th th)" - using `(Th th, Th th') \ (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def) - ultimately show ?thesis using that by metis -qed - -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: "runing (t@s) \ {}" -proof(cases "th \ runing (t@s)") - case True thus ?thesis by auto -next - case False - thus ?thesis using th_blockedE by auto -qed - - -end -end diff -r 2aa37de77f31 -r b6ea51cd2e88 Journal/Paper.thy --- a/Journal/Paper.thy Thu Jan 14 03:29:22 2016 +0000 +++ b/Journal/Paper.thy Fri Jan 15 02:05:29 2016 +0000 @@ -23,7 +23,9 @@ cpreced ("cprec") and cp ("cprec") and holdents ("resources") and - DUMMY ("\<^raw:\mbox{$\_\!\_$}>") + DUMMY ("\<^raw:\mbox{$\_\!\_$}>") and + cntP ("c\<^bsub>P\<^esub>") and + cntV ("c\<^bsub>V\<^esub>") (*>*) @@ -178,17 +180,18 @@ priority.}'' The same error is also repeated later in this textbook. - While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only formal publications we have - found that specify the incorrect behaviour, it seems also many - informal descriptions of PIP overlook the possibility that another - high-priority might wait for a low-priority process to finish. - A notable exception is the texbook \cite{buttazzo}, which gives the correct - behaviour of resetting the priority of a thread to the highest remaining priority of the - threads it blocks. This textbook also gives an informal proof for - the correctness of PIP in the style of Sha et al. Unfortunately, this informal - proof is too vague to be useful for formalising the correctness of PIP - and the specification leaves out nearly all details in order - to implement PIP efficiently.\medskip\smallskip + While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only + formal publications we have found that specify the incorrect + behaviour, it seems also many informal descriptions of PIP overlook + the possibility that another high-priority might wait for a + low-priority process to finish. A notable exception is the texbook + \cite{buttazzo}, which gives the correct behaviour of resetting the + priority of a thread to the highest remaining priority of the + threads it blocks. This textbook also gives an informal proof for + the correctness of PIP in the style of Sha et al. Unfortunately, + this informal proof is too vague to be useful for formalising the + correctness of PIP and the specification leaves out nearly all + details in order to implement PIP efficiently.\medskip\smallskip % %The advantage of formalising the %correctness of a high-level specification of PIP in a theorem prover @@ -196,27 +199,29 @@ %informal reasoning (since we have to analyse all possible behaviours %of threads, i.e.~\emph{traces}, that could possibly happen). - \noindent - {\bf Contributions:} There have been earlier formal investigations - into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model - checking techniques. This paper presents a formalised and - mechanically checked proof for the correctness of PIP. For this we - needed to design a new correctness criterion for PIP. In contrast to model checking, our - formalisation provides insight into why PIP is correct and allows us - to prove stronger properties that, as we will show, can help with an - efficient implementation of PIP in the educational PINTOS operating - system \cite{PINTOS}. For example, we found by ``playing'' with the - formalisation that the choice of the next thread to take over a lock - when a resource is released is irrelevant for PIP being correct---a - fact that has not been mentioned in the literature and not been used - in the reference implementation of PIP in PINTOS. This fact, however, is important - for an efficient implementation of PIP, because we can give the lock - to the thread with the highest priority so that it terminates more - quickly. We were also being able to generalise the scheduler of Sha - et al.~\cite{Sha90} to the practically relevant case where critical - sections can overlap; see Figure~\ref{overlap} \emph{a)} below for an example of - this restriction. %In the existing literature there is no - %proof and also no proving method that cover this generalised case. + \noindent {\bf Contributions:} There have been earlier formal + investigations into PIP \cite{Faria08,Jahier09,Wellings07}, but they + employ model checking techniques. This paper presents a formalised + and mechanically checked proof for the correctness of PIP. For this + we needed to design a new correctness criterion for PIP. In contrast + to model checking, our formalisation provides insight into why PIP + is correct and allows us to prove stronger properties that, as we + will show, can help with an efficient implementation of PIP. We + illustrate this with an implementation of PIP in the educational + PINTOS operating system \cite{PINTOS}. For example, we found by + ``playing'' with the formalisation that the choice of the next + thread to take over a lock when a resource is released is irrelevant + for PIP being correct---a fact that has not been mentioned in the + literature and not been used in the reference implementation of PIP + in PINTOS. This fact, however, is important for an efficient + implementation of PIP, because we can give the lock to the thread + with the highest priority so that it terminates more quickly. We + were also being able to generalise the scheduler of Sha et + al.~\cite{Sha90} to the practically relevant case where critical + sections can overlap; see Figure~\ref{overlap} \emph{a)} below for + an example of this restriction. In the existing literature there is + no proof and also no proving method that cover this generalised + case. \begin{figure} \begin{center} @@ -382,6 +387,18 @@ tasks involved in the inheritance process and thus minimises the number of potentially expensive thread-switches. + We will also need counters for @{term P} and @{term V} events of a thread @{term th} + in a state @{term s}. This can be straightforwardly defined in Isabelle as + + \begin{isabelle}\ \ \ \ \ %%% + \mbox{\begin{tabular}{@ {}l} + @{thm cntP_def}\\ + @{thm cntV_def} + \end{tabular}} + \end{isabelle} + + \noindent using the predefined function @{const count} for lists. + Next, we introduce the concept of \emph{waiting queues}. They are lists of threads associated with every resource. The first thread in this list (i.e.~the head, or short @{term hd}) is chosen to be the one @@ -943,8 +960,39 @@ From these two lemmas we can see the correctness of PIP, which is that: the blockage of th is reasonable and under control. + Lemmas we want to describe: + + \begin{lemma} + @{thm eq_pv_persist} + \end{lemma} + + \begin{lemma} + @{thm eq_pv_blocked} + \end{lemma} + + \begin{lemma} + @{thm runing_cntP_cntV_inv} + \end{lemma} + + \noindent + Remember we do not have the well-nestedness restriction in our + proof, which means the difference between the counters @{const cntV} + and @{const cntP} can be larger than @{term 1}. + + \begin{lemma} + @{thm runing_inversion} + \end{lemma} + + + \begin{lemma} + @{thm th_blockedE} + \end{lemma} + \subsection*{END OUTLINE} + + + In what follows we will describe properties of PIP that allow us to prove Theorem~\ref{mainthm} and, when instructive, briefly describe our argument. It is relatively easy to see that: @@ -957,7 +1005,7 @@ \end{isabelle} \noindent - The second property is by induction of @{term vt}. The next three + The second property is by induction on @{term vt}. The next three properties are: \begin{isabelle}\ \ \ \ \ %%% diff -r 2aa37de77f31 -r b6ea51cd2e88 journal.pdf Binary file journal.pdf has changed