# HG changeset patch # User zhangx # Date 1492777033 -28800 # Node ID 83da37e8b1d226e044a67b4f4db1e38bb399b367 # Parent 023bdcc221ea35353ff50d115e586a15dfa61922 "up_to" added and main theorems improved. diff -r 023bdcc221ea -r 83da37e8b1d2 Correctness.thy --- a/Correctness.thy Thu Apr 20 14:22:01 2017 +0100 +++ b/Correctness.thy Fri Apr 21 20:17:13 2017 +0800 @@ -6,21 +6,9 @@ "length (actions_of ts (e#t)) \ 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 \ A" - and "c \ B" - and "Max A = c" -shows "Max B = c" -using Max.subset assms -by (metis Max.coboundedI Max_eqI rev_finite_subset subset_eq) - - lemma image_Max_eqI: assumes "finite B" and "b \ B" @@ -117,7 +105,7 @@ locale extend_highest_gen = highest_gen + fixes t - assumes vt_t: "vt (t @ s)" + 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" @@ -147,6 +135,16 @@ 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 @@ -189,7 +187,7 @@ lemma th_kept: "th \ threads (t @ s) \ - preced th (t @ s) = preced th s" (is "?Q t") + preced th (t@s) = preced th s" (is "?Q t") proof - show ?thesis proof(induct rule:ind) @@ -252,7 +250,7 @@ qed text {* - According to @{thm th_kept}, thread @{text "th"} has its liveness status + 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"}. @@ -266,8 +264,7 @@ 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" +lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s" proof(induct rule:ind) case Nil from highest_preced_thread @@ -506,20 +503,13 @@ precedence in the whole system. *} lemma running_preced_inversion: - assumes running': "th' \ running (t @ s)" - shows "cp (t @ s) th' = preced th s" + assumes running': "th' \ running (t@s)" + shows "cp (t@s) th' = preced th s" (is "?L = ?R") proof - - have "th' \ 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 "\ = preced th s" - using th_cp_preced . + have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms + by (unfold running_def, auto) + also have "\ = ?R" + by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) finally show ?thesis . qed @@ -730,36 +720,6 @@ section {* The existence of `blocking thread` *} -lemma th_ancestor_has_max_ready: - assumes th'_in: "th' \ readys (t@s)" - and dp: "th' \ 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' \ threads (t @ s)" - using readys_def th'_in vat_t.subtree_tG_thread by auto - next - show "th \ 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'"} @@ -767,93 +727,178 @@ 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'"}. *} + 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: *) + assumes "th \ running (t@s)" + obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" + "th' \ running (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 "running"}. *} + moreover have "th \ readys (t@s)" + using assms running_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' \ running (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 - + -- {* 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) \ 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.rg_RAG_threads 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 + thm the_preced_def + also have "... = ?R" + using th_cp_max th_cp_preced th_kept + the_preced_def vat_t.max_cp_readys_threads by auto + thm th_cp_max th_cp_preced th_kept + the_preced_def vat_t.max_cp_readys_threads + 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 running} by definition. *} + with `th' \ readys (t@s)` show ?thesis by (simp add: running_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 - -lemma th_blockedE: (* ddd, the other main lemma to be presented: *) - obtains th' where "th' \ nancestors (tG (t @ s)) th" +lemma (* new proof of th_blockedE *) + assumes "th \ running (t @ s)" + obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" "th' \ running (t @ s)" proof - - -- {* According to @{thm vat_t.th_chain_to_ready}, there is a - ready ancestor of @{term th}. *} - have "\th' \ nancestors (tG (t @ s)) th. th' \ readys (t @ s)" - using th_kept vat_t.th_chain_to_ready_tG by auto - then obtain th' where th'_in: "th' \ readys (t @ s)" - and dp: "th' \ nancestors (tG (t @ s)) th" - by blast - + + -- {* According to @{thm vat_t.th_chain_to_ready}, either @{term "th"} is + in @{term "readys"} or there is path in the @{term RAG} leading from + it to a thread that is in @{term "readys"}. However, @{term th} cannot + be in @{term readys}, because otherwise, since @{term th} holds the + highest @{term cp}-value, it must be @{term "running"}. This would + violate our assumption. *} + have "th \ readys (t @ s)" + using assms running_def th_cp_max vat_t.max_cp_readys_threads by auto + then have "\th'. th' \ readys (t @ s) \ (Th th, Th th') \ (RAG (t @ s))\<^sup>+" + using th_kept vat_t.th_chain_to_ready by auto + then 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 first show that this @{term th'} is running. *} + have "th' \ running (t @ s)" + proof - + -- {* For this we need to show that @{term th'} holds the highest @{term cp}-value: *} + have "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) ` (the_thread ` subtree (tRAG (t @ s)) (Th th')))" + proof - + have "(the_preced (t @ s) \ the_thread) ` subtree (tRAG (t @ s)) (Th th') = + the_preced (t @ s) ` the_thread ` subtree (tRAG (t @ s)) (Th th')" + by fastforce + thus ?thesis by (unfold cp_alt_def1, simp) + qed + 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 "the_thread ` subtree (tRAG (t @ s)) (Th th') \ threads (t @ s)" + by (smt imageE mem_Collect_eq readys_def subsetCE subsetI th'_in + the_thread.simps vat_t.subtree_tRAG_thread) + next + show "th \ the_thread ` subtree (tRAG (t @ s)) (Th th')" + proof - + have "Th th \ subtree (tRAG (t @ s)) (Th th')" using dp + by (unfold tRAG_subtree_eq, auto simp:subtree_def) + thus ?thesis by force + qed + 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 - 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' \ readys (t @ s)` - have "th' \ running (t @ s)" by (simp add: running_def) - + -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, + it is @{term running} by definition. *} + with `th' \ readys (t @ s)` show "th' \ running (t @ s)" by (simp add: running_def) + qed + -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *} - moreover have "th' \ nancestors (tG (t @ s)) th" - using dp unfolding nancestors_def2 by simp + 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 lemma th_blockedE_pretty: - shows "\th' \ nancestors (tG (t @ s)) th. th' \ running (t @ s)" -using th_blockedE assms -by blast - + assumes "th \ running (t@s)" + shows "\th'. Th th' \ ancestors (RAG (t @ s)) (Th th) \ th' \ running (t@s)" +using th_blockedE assms by blast text {* Now it is easy to see there is always a thread to run by case analysis - on whether thread @{term th} is running: if the answer is yes, the + 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) \ {}" -using th_blockedE by auto +lemma live: "running (t@s) \ {}" +proof(cases "th \ running (t@s)") + case True thus ?thesis by auto +next + case False + thus ?thesis using th_blockedE by auto +qed lemma blockedE: - assumes "th \ running (t @ s)" - obtains th' where "th' \ nancestors (tG (t @ s)) th" - "th' \ running (t @ s)" + assumes "th \ running (t@s)" + obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" + "th' \ running (t@s)" "th' \ threads s" "\detached s th'" - "cp (t @ s) th' = preced th s" + "cp (t@s) th' = preced th s" "th' \ th" -proof - - obtain th' where a: "th' \ nancestors (tG (t @ s)) th" "th' \ running (t @ s)" - using th_blockedE by blast - moreover - from a(2) have b: "th' \ threads s" - using running_threads_inv assms by metis - moreover - from a(2) have "\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' \ th" using assms a(2) by blast - ultimately show ?thesis using that by metis -qed - - -lemma nblockedE: - assumes "th \ running (t @ s)" - obtains th' where "th' \ ancestors (tG (t @ s)) th" - "th' \ running (t @ s)" - "th' \ threads s" - "\detached s th'" - "cp (t @ s) th' = preced th s" - "th' \ th" -using blockedE unfolding nancestors_def -using assms nancestors3 by auto - +by (metis assms running_inversion(2) running_preced_inversion running_threads_inv th_blockedE) lemma detached_not_running: - assumes "detached (t @ s) th'" + assumes "detached (t@s) th'" and "th' \ th" - shows "th' \ running (t @ s)" + shows "th' \ running (t@s)" proof assume otherwise: "th' \ running (t @ s)" have "cp (t@s) th' = cp (t@s) th" @@ -879,21 +924,19 @@ section {* The correctness theorem of PIP *} text {* - - In this section, we identify two more conditions in addition to the ones - already specified in the current locale, based on which the correctness - of PIP is formally proved. + In this section, we identify two more conditions in addition to the ones already + specified in the forgoing locales, 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. + 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 Prioirty 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. *} + 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 @@ -938,15 +981,15 @@ thus ?thesis unfolding blockers_def by simp qed -text {* The following lemma shows that a blocker does not die as long as the -highest thread @{term th} is live. +text {* + The following lemma shows that a blocker may never die + as long as the highest thread @{term th} is living. - 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}. + 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: @@ -1233,32 +1276,11 @@ *} -theorem bound_priority_inversion: - "occs (\ t'. th \ running (t'@s)) t \ - 1 + (length (actions_of blockers t) + length (filter (isCreate) t))" - (is "?L \ ?R") -proof - - let ?Q = "(\ t'. th \ running (t'@s))" - from occs_le[of ?Q t] - thm occs_le - have "?L \ (1 + length t) - occs ?Q t" by simp - also have "... \ ?R" - proof - - thm actions_th_occs actions_split - have "length t - (length (actions_of blockers t) + length (filter (isCreate) t)) - \ occs (\ t'. th \ running (t'@s)) t" (is "?L1 \ ?R1") - proof - - from actions_split have "?L1 = length (actions_of {th} t)" using actions_split by arith - also have "... \ ?R1" using actions_th_occs by simp - finally show ?thesis . - qed - thus ?thesis by simp - qed - finally show ?thesis . -qed end +(* ccc *) + fun postfixes where "postfixes [] = []" | "postfixes (x#xs) = (xs)#postfixes xs" @@ -1303,8 +1325,143 @@ qed simp qed auto +context extend_highest_gen +begin +(* (* this lemma does not hold *) +lemma actions_th_occs': "length (actions_of {th} t) = occs' (\t'. th \ running (t' @ s)) t" + sorry +*) + + +lemma actions_th_occs'_pre: + assumes "t = e'#t'" + shows "length (actions_of {th} t) \ occs' (\ t'. th \ running (t'@s)) t" + using assms +proof(induct arbitrary: e' t' rule:ind) + case h: (Cons e t e' t') + interpret vt: valid_trace "(t@s)" using h(1) + by (unfold_locales, simp) + interpret ve: extend_highest_gen s th prio tm t using h by simp + interpret ve': extend_highest_gen s th prio tm "e#t" using h by simp + show ?case (is "?L \ ?R") + proof(cases t) + case Nil + show ?thesis + proof(cases "actor e = th") + case True + from ve'.th_no_create[OF _ this] + have "\ isCreate e" by auto + from PIP_actorE[OF h(2) True this] Nil + have "th \ 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) \ occs' (\t'. th \ running (t' @ s)) t" + (is "?F t \ ?G t1") . + show ?thesis + proof(cases "actor e = th") + case True + from ve'.th_no_create[OF _ this] + have "\ isCreate e" by auto + from PIP_actorE[OF h(2) True this] + have "th \ running (t@s)" by simp + hence "?R = 1 + ?G t1" by (unfold h1 eq_t', simp) + moreover have "?L = 1 + ?F t" using True by (simp add:actions_of_def) + ultimately show ?thesis using le by simp + next + case False + with le + show ?thesis by (unfold h1 eq_t', simp add:actions_of_def) + qed + qed +qed auto + +text {* + The following lemma is a simple corollary of @{thm actions_th_occs_pre}. It is the + lemma really needed in later proofs. +*} + + +lemma occs'_replacement1: "occs' (\ t'. th \ running (t'@s)) t = length (filter (\ s'. th \ running s') (up_to s t))" +proof - + have h: "((\s'. th \ running s') \ (\t'. t' @ s)) = (\ t'. th \ running (t' @ s))" by (rule ext, simp) + thus ?thesis + by (unfold occs'_def up_to_def length_filter_map h, simp) +qed + +lemma occs'_replacement2: "occs' (\ t'. th \ running (t'@s)) t = length (filter (\ s'. th \ running s') (up_to s t))" +proof - + have h: "((\s'. th \ running s') \ (\t'. t' @ s)) = (\ t'. th \ running (t' @ s))" by (rule ext, simp) + thus ?thesis + by (unfold occs'_def up_to_def length_filter_map h, simp) +qed + +lemma actions_th_occs': + shows "length (actions_of {th} t) \ occs' (\ t'. th \ running (t'@s)) t" +proof(cases t) + case (Cons e' t') + from actions_th_occs'_pre[OF this] + have "length (actions_of {th} t) \ occs' (\t'. th \ running (t' @ s)) t" . + thus ?thesis by simp +qed (auto simp:actions_of_def) + +theorem bound_priority_inversion': + "occs' (\ t'. th \ running (t'@s)) t \ + (length (actions_of blockers t) + length (filter (isCreate) t))" + (is "?L \ ?R") +proof - + let ?Q = "(\ t'. th \ running (t'@s))" + from occs_len'[of ?Q t] + have "?L \ (length t) - occs' ?Q t" by simp + also have "... \ ?R" + proof - + have "length t - (length (actions_of blockers t) + length (filter (isCreate) t)) + \ occs' (\ t'. th \ running (t'@s)) t" (is "?L1 \ ?R1") + proof - + have "?L1 = length (actions_of {th} t)" using actions_split by arith + also have "... \ ?R1" using actions_th_occs' by simp + finally show ?thesis . + qed + thus ?thesis by simp + qed + finally show ?thesis . +qed + +theorem bound_priority_inversion: + "occs (\ t'. th \ running (t'@s)) t \ + 1 + (length (actions_of blockers t) + length (filter (isCreate) t))" + (is "?L \ ?R") +proof - + let ?Q = "(\ t'. th \ running (t'@s))" + from occs_le[of ?Q t] + have "?L \ 1 + (length t) - occs ?Q t" by simp + also have "... \ ?R" + proof - + have "length t - (length (actions_of blockers t) + length (filter (isCreate) t)) + \ occs (\ t'. th \ running (t'@s)) t" (is "?L1 \ ?R1") + proof - + have "?L1 = length (actions_of {th} t)" using actions_split by arith + also have "... \ ?R1" using actions_th_occs by simp + finally show ?thesis . + qed + thus ?thesis by simp + qed + finally show ?thesis . +qed + +end + text {* As explained before, lemma @{text bound_priority_inversion} alone does not ensure the correctness of PIP. For PIP to be correct, the number of blocking operations @@ -1320,7 +1477,7 @@ 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. + 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) @@ -1328,7 +1485,27 @@ 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: + (* + assumes finite_span: + "th' \ blockers \ + (\ span. \ t'. extend_highest_gen s th prio tm t' \ + length (actions_of {th'} t') = span \ detached (t'@s) th')" + *) + + -- {* + The above definition and explain is problematic because the number of actions taken + by @{term th'} may be affected by is environment not modeled by the events of our + PIP model. + *} + + -- {* + However, we still need to express the idea that every blocker becomes detached in bounded + number of steps. Supposing @{term span} is such a bound, the following @{term finite_span} + assumption says if @{term th'} is not @{term detached} in state (t'@s), then its number + of actions must be less than this bound @{term span}: + *} + + assumes finite_span: "th' \ blockers \ (\ span. \ t'. extend_highest_gen s th prio tm t' \ \ detached (t'@s) th' \ length (actions_of {th'} t') < span)" @@ -1339,6 +1516,7 @@ The @{term span} is a upper bound on these step numbers. *} + -- {* The following @{text BC} is bound of @{term Create}-operations *} fixes BC -- {* The following assumption requires the number of @{term Create}-operations is @@ -1359,7 +1537,7 @@ where @{text "BC t"} is of a certain proportion of @{term "length t"}. *} assumes finite_create: - "\ t'. extend_highest_gen s th prio tm t' \ length (filter isCreate t') \ BC" + "\ t'. extend_highest_gen s th prio tm t' \ length (filter isCreate t') < BC" begin text {* @@ -1367,7 +1545,7 @@ *} lemma create_bc: - shows "length (filter isCreate t) \ BC" + shows "length (filter isCreate t) < BC" by (meson extend_highest_gen_axioms finite_create) text {* @@ -1454,6 +1632,25 @@ 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' (\ t'. th \ running (t'@s)) t \ + ((\ th' \ blockers . span th') + BC)" (is "?L \ ?R" is "_ \ (?A + ?B)" ) +proof - + from bound_priority_inversion' + have "?L \ (length (actions_of blockers t) + length (filter isCreate t))" + (is "_ \ (?A' + ?B')") . + moreover have "?A' \ ?A" using len_action_blockers . + moreover have "?B' \ ?B" using create_bc by auto + ultimately show ?thesis by simp +qed + + +theorem priority_inversion_is_finite_upto: + "length [s'\up_to s t . th \ running s'] \ + ((\ th' \ blockers . span th') + BC)" + using priority_inversion_is_finite'[unfolded occs'_replacement2] by simp + theorem priority_inversion_is_finite: "occs (\ t'. th \ running (t'@s)) t \ 1 + ((\ th' \ blockers . span th') + BC)" (is "?L \ ?R" is "_ \ 1 + (?A + ?B)" ) @@ -1462,7 +1659,7 @@ have "?L \ 1 + (length (actions_of blockers t) + length (filter isCreate t))" (is "_ \ 1 + (?A' + ?B')") . moreover have "?A' \ ?A" using len_action_blockers . - moreover have "?B' \ ?B" using create_bc . + moreover have "?B' \ ?B" using create_bc by auto ultimately show ?thesis by simp qed @@ -1477,11 +1674,7 @@ "length t - ((\ th' \ blockers . span th') + BC) \ length (actions_of {th} t)" using actions_split create_bc len_action_blockers by linarith -thm actions_split - end - - end