diff -r 71a3300d497b -r 95e7933968f8 Correctness.thy --- a/Correctness.thy Fri Apr 15 14:44:09 2016 +0100 +++ b/Correctness.thy Thu Jun 02 13:15:03 2016 +0100 @@ -52,6 +52,13 @@ sublocale highest_gen < vat_s?: valid_trace "s" by (unfold_locales, insert vt_s, simp) +fun occs where + "occs Q [] = (if Q [] then 1 else 0::nat)" | + "occs Q (x#xs) = (if Q (x#xs) then (1 + occs Q xs) else occs Q xs)" + +lemma occs_le: "occs Q t + occs (\ e. \ Q e) t \ (1 + length t)" + by (induct t, auto) + context highest_gen begin @@ -68,6 +75,7 @@ @{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" @@ -742,6 +750,9 @@ -- {* 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)" @@ -762,9 +773,82 @@ 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 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 + +lemma (* new proof of th_blockedE *) + 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 - + -- {* 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 + 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} @@ -792,5 +876,588 @@ thus ?thesis using th_blockedE by auto qed +lemma blockedE: + assumes "th \ runing (t@s)" + obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" + "th' \ runing (t@s)" + "th' \ threads s" + "\detached s th'" + "cp (t@s) th' = preced th s" + "th' \ th" +by (metis assms runing_inversion(2) runing_preced_inversion runing_threads_inv th_blockedE) + +lemma detached_not_runing: + assumes "detached (t@s) th'" + and "th' \ th" + shows "th' \ runing (t@s)" +proof + assume otherwise: "th' \ runing (t @ s)" + have "cp (t@s) th' = cp (t@s) th" + proof - + have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" using otherwise + by (simp add:runing_def) + moreover have "cp (t@s) th = ..." by (simp add: vat_t.max_cp_readys_threads) + ultimately show ?thesis by simp + qed + moreover have "cp (t@s) th' = preced th' (t@s)" using assms(1) + by (simp add: detached_cp_preced) + moreover have "cp (t@s) th = preced th (t@s)" by simp + ultimately have "preced th' (t@s) = preced th (t@s)" by simp + from preced_unique[OF this] + have "th' \ threads (t @ s) \ th \ threads (t @ s) \ th' = th" . + moreover have "th' \ threads (t@s)" + using otherwise by (unfold runing_def readys_def, auto) + moreover have "th \ threads (t@s)" by (simp add: th_kept) + ultimately have "th' = th" by metis + with assms(2) show False by simp +qed + +section {* The correctness theorem of PIP *} + +text {* + In this section, we identify two more conditions in addition to the ones already + specified in the 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 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. +*} + +text {* + The following set @{text "blockers"} characterizes the set of threads which + might block @{term th} in @{term t}: +*} + +definition "blockers = {th'. \detached s th' \ th' \ th}" + +text {* + The following lemma shows that the definition of @{term "blockers"} is correct, + i.e. blockers do block @{term "th"}. It is a very simple corollary of @{thm blockedE}. +*} +lemma runingE: + assumes "th' \ runing (t@s)" + obtains (is_th) "th' = th" + | (is_other) "th' \ blockers" + using assms blockers_def runing_inversion(2) by auto + +text {* + The following lemma shows that the number of blockers are finite. + The reason is simple, because blockers are subset of thread set, which + has been shown finite. +*} + +lemma finite_blockers: "finite blockers" +proof - + have "finite {th'. \detached s th'}" + proof - + have "finite {th'. Th th' \ Field (RAG s)}" + proof - + have "{th'. Th th' \ Field (RAG s)} \ threads s" + proof + fix x + assume "x \ {th'. Th th' \ Field (RAG s)}" + thus "x \ threads s" using vat_s.RAG_threads by auto + qed + moreover have "finite ..." by (simp add: vat_s.finite_threads) + ultimately show ?thesis using rev_finite_subset by auto + qed + thus ?thesis by (unfold detached_test, auto) + qed + thus ?thesis unfolding blockers_def by simp +qed + +text {* + The following lemma shows that a blocker 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}. +*} + +lemma blockers_kept: + assumes "th' \ blockers" + shows "th' \ threads (t@s)" +proof(induct rule:ind) + case Nil + from assms[unfolded blockers_def detached_test] + have "Th th' \ Field (RAG s)" by simp + from vat_s.RAG_threads[OF this] + show ?case by simp +next + case h: (Cons e t) + interpret et: extend_highest_gen s th prio tm t + using h by simp + show ?case + proof - + { assume otherwise: "th' \ threads ((e # t) @ s)" + from threads_Exit[OF h(5)] this have eq_e: "e = Exit th'" by auto + from h(2)[unfolded this] + have False + proof(cases) + case h: (thread_exit) + hence "th' \ readys (t@s)" by (auto simp:runing_def) + from readys_holdents_detached[OF this h(2)] + have "detached (t @ s) th'" . + from et.detached_not_runing[OF this] assms[unfolded blockers_def] + have "th' \ runing (t @ s)" by auto + with h(1) show ?thesis by simp + qed + } thus ?thesis by auto + qed +qed + +text {* + The following lemma shows that a blocker may never execute its @{term Create}-operation + during the period of @{term t}. The reason is that for a thread to be created + (or executing its @{term Create} operation), it must be non-existing (or dead). + However, since lemma @{thm blockers_kept} shows that blockers are always living, + it can not be created. + + A thread is created only when there is some external reason, there is need for it to run. + The precondition for this is that it has already died (or get out of existence). +*} + +lemma blockers_no_create: + assumes "th' \ blockers" + and "e \ set t" + and "actor e = th'" + shows "\ isCreate e" + using assms(2,3) +proof(induct rule:ind) + case h: (Cons e' t) + interpret et: extend_highest_gen s th prio tm t + using h by simp + { assume eq_e: "e = e'" + from et.blockers_kept assms + have "th' \ threads (t @ s)" by auto + with h(2,7) + have ?case + by (unfold eq_e, cases, auto simp:blockers_def) + } with h + show ?case by auto +qed auto + +text {* + The following lemma shows that, same as blockers, + the highest thread @{term th} also can not execute its @{term Create}-operation. + And the reason is similar: since @{thm th_kept} says that thread @{term th} is kept live + during @{term t}, it can not (or need not) be created another time. +*} +lemma th_no_create: + assumes "e \ set t" + and "actor e = th" + shows "\ isCreate e" + using assms +proof(induct rule:ind) + case h:(Cons e' t) + interpret et: extend_highest_gen s th prio tm t + using h by simp + { assume eq_e: "e = e'" + from et.th_kept have "th \ threads (t @ s)" by simp + with h(2,7) + have ?case by (unfold eq_e, cases, auto) + } with h + show ?case by auto +qed auto + +text {* + The following is a preliminary lemma in order to show that the number of + actions (or operations) taken by the highest thread @{term th} is + less or equal to the number of occurrences when @{term th} is in running + state. What is proved in this lemma is essentially a strengthening, which + says the inequality holds even if the occurrence at the very beginning is + ignored. + + The reason for this lemma is that for every operation to be executed, its actor must + be in running state. Therefore, there is one occurrence of running state + behind every action. + + However, this property does not hold in general, because, for + the execution of @{term Create}-operation, the actor does not have to be in running state. + Actually, the actor must be in dead state, in order to be created. For @{term th}, this + property holds because, according to lemma @{thm th_no_create}, @{term th} can not execute + any @{term Create}-operation during the period of @{term t}. +*} +lemma actions_th_occs_pre: + assumes "t = e'#t'" + shows "length (actions_of {th} t) \ occs (\ t'. th \ runing (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 \ runing 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 \ runing (t' @ s)) t1" + (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 \ runing (t@s)" by simp + hence "?R = 1 + ?G t1" by (unfold h1 eq_t', simp) + moreover have "?L = 1 + ?F t" using True by (simp add:actions_of_def) + ultimately show ?thesis using le by simp + next + case False + with le + show ?thesis by (unfold h1 eq_t', simp add:actions_of_def) + qed + qed +qed auto + +text {* + The following lemma is a simple corollary of @{thm actions_th_occs_pre}. It is the + lemma really needed in later proofs. +*} +lemma actions_th_occs: + shows "length (actions_of {th} t) \ occs (\ t'. th \ runing (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 \ runing (t' @ s)) t'" . + moreover have "... \ occs (\t'. th \ runing (t' @ s)) t" + by (unfold Cons, auto) + ultimately show ?thesis by simp +qed (auto simp:actions_of_def) + +text {* + The following lemma splits all the operations in @{term t} into three + disjoint sets, namely the operations of @{term th}, the operations of + blockers and @{term Create}-operations. These sets are mutually disjoint + because: @{term "{th}"} and @{term blockers} are disjoint by definition, + and neither @{term th} nor any blocker can execute @{term Create}-operation + (according to lemma @{thm th_no_create} and @{thm blockers_no_create}). + + One important caveat noted by this lemma is that: + Although according to assumption @{thm create_low}, each thread created in + @{term t} has precedence lower than @{term th}, therefore, will get no + change to run after creation, therefore, can not acquire any resource + to become a blocker, the @{term Create}-operations of such + lower threads may still consume overall execution time of duration @{term t}, therefore, + may compete for execution time with the most urgent thread @{term th}. + For PIP to be correct, the number of such competing operations needs to be + bounded somehow. +*} + +lemma actions_split: + "length t = length (actions_of {th} t) + + length (actions_of blockers t) + + length (filter (isCreate) t)" +proof(induct rule:ind) + case h: (Cons e t) + interpret ve : extend_highest_gen s th prio tm t using h by simp + interpret ve': extend_highest_gen s th prio tm "e#t" using h by simp + show ?case (is "?L (e#t) = ?T (e#t) + ?O (e#t) + ?C (e#t)") + proof(cases "actor e \ runing (t@s)") + case True + thus ?thesis + proof(rule ve.runingE) + assume 1: "actor e = th" + have "?T (e#t) = 1 + ?T (t)" using 1 by (simp add:actions_of_def) + moreover have "?O (e#t) = ?O t" + proof - + have "actor e \ blockers" using 1 + by (simp add:actions_of_def blockers_def) + thus ?thesis by (simp add:actions_of_def) + qed + moreover have "?C (e#t) = ?C t" + proof - + from ve'.th_no_create[OF _ 1] + have "\ isCreate e" by auto + thus ?thesis by (simp add:actions_of_def) + qed + ultimately show ?thesis using h by simp + next + assume 2: "actor e \ ve'.blockers" + have "?T (e#t) = ?T (t)" + proof - + from 2 have "actor e \ th" by (auto simp:blockers_def) + thus ?thesis by (auto simp:actions_of_def) + qed + moreover have "?O (e#t) = 1 + ?O(t)" using 2 + by (auto simp:actions_of_def) + moreover have "?C (e#t) = ?C(t)" + proof - + from ve'.blockers_no_create[OF 2, of e] + have "\ isCreate e" by auto + thus ?thesis by (simp add:actions_of_def) + qed + ultimately show ?thesis using h by simp + qed + next + case False + from h(2) + have is_create: "isCreate e" + by (cases; insert False, auto) + have "?T (e#t) = ?T t" + proof - + have "actor e \ th" + proof + assume "actor e = th" + from ve'.th_no_create[OF _ this] + have "\ isCreate e" by auto + with is_create show False by simp + qed + thus ?thesis by (auto simp:actions_of_def) + qed + moreover have "?O (e#t) = ?O t" + proof - + have "actor e \ blockers" + proof + assume "actor e \ blockers" + from ve'.blockers_no_create[OF this, of e] + have "\ isCreate e" by simp + with is_create show False by simp + qed + thus ?thesis by (simp add:actions_of_def) + qed + moreover have "?C (e#t) = 1 + ?C t" using is_create + by (auto simp:actions_of_def) + ultimately show ?thesis using h by simp + qed +qed (auto simp:actions_of_def) + +text {* + By combining several of forging lemmas, this lemma gives a upper bound + of the occurrence number when the most urgent thread @{term th} is blocked. + + It says, the occasions when @{term th} is blocked during period @{term t} + is no more than the number of @{term Create}-operations and + the operations taken by blockers plus one. + + Since the length of @{term t} may extend indefinitely, if @{term t} is full + of the above mentioned blocking operations, @{term th} may have not chance to run. + And, since @{term t} can extend indefinitely, @{term th} my be blocked indefinitely + with the growth of @{term t}. Therefore, this lemma alone does not ensure + the correctness of PIP. + +*} + +theorem bound_priority_inversion: + "occs (\ t'. th \ runing (t'@s)) t \ + 1 + (length (actions_of blockers t) + length (filter (isCreate) t))" + (is "?L \ ?R") +proof - + let ?Q = "(\ t'. th \ runing (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 \ runing (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 + (by {\em blocking operation}, we mean the @{term Create}-operations and + operations taken by blockers) has to be bounded somehow. + + And the following lemma is for this purpose. +*} + +locale bounded_extend_highest = extend_highest_gen + + -- {* + To bound operations of blockers, the locale specifies that each blocker + releases all resources and becomes detached after a certain number + of operations. In the assumption, this number is given by the + existential variable @{text span}. Notice that this number is fixed for each + blocker regardless of any particular instance of @{term t} in which it operates. + + This assumption is reasonable, because it is a common sense that + the total number of operations take by any standalone thread (or process) + is only determined by its own input, and should not be affected by + the particular environment in which it operates. In this particular case, + we regard the @{term t} as the environment of thread @{term th}. + *} + assumes finite_span: + "th' \ blockers \ + (\ span. \ t'. extend_highest_gen s th prio tm t' \ + length (actions_of {th'} t') = span \ detached (t'@s) th')" + -- {* The following @{text BC} is bound of @{term Create}-operations *} + fixes BC + -- {* + The following assumption requires the number of @{term Create}-operations is + less or equal to @{term BC} regardless of any particular extension of @{term t}. + + Although this assumption might seem doubtful at first sight, it is necessary + to ensure the occasions when @{term th} is blocked to be finite. Just consider + the extreme case when @{term Create}-operations consume all the time in duration + @{term "t"} and leave no space for neither @{term "th"} nor blockers to operate. + An investigate of the precondition for @{term Create}-operation in the definition + of @{term PIP} may reveal that such extreme cases are well possible, because it + is only required the thread to be created be a fresh (or dead one), and there + are infinitely many such threads. + + However, if we relax the correctness criterion of PIP, allowing @{term th} to be + blocked indefinitely while still attaining a certain portion of @{term t} to complete + its task, then this bound @{term BC} can be lifted to function depending on @{term t} + where @{text "BC t"} is of a certain proportion of @{term "length t"}. + *} + assumes finite_create: + "\ t'. extend_highest_gen s th prio tm t' \ length (filter isCreate t') \ BC" +begin + +text {* + The following lemmas show that the number of @{term Create}-operations is bound by @{term BC}: +*} + +lemma create_bc: + shows "length (filter isCreate t) \ BC" + by (meson extend_highest_gen_axioms finite_create) + +text {* + The following @{term span}-function gives the upper bound of + operations take by each particular blocker. +*} +definition "span th' = (SOME span. + \t'. extend_highest_gen s th prio tm t' \ + length (actions_of {th'} t') = span \ detached (t' @ s) th')" + +text {* + The following lemmas shows the correctness of @{term span}, i.e. + the number of operations of taken by @{term th'} is given by + @{term "span th"}. + + The reason for this lemma is that since @{term th'} gives up all resources + after @{term "span th'"} operations and becomes detached, + its inherited high priority is lost, with which the right to run goes as well. +*} +lemma le_span: + assumes "th' \ blockers" + shows "length (actions_of {th'} t) \ span th'" +proof - + from finite_span[OF assms(1)] obtain span' + where span': "\t'. extend_highest_gen s th prio tm t' \ + length (actions_of {th'} t') = span' \ detached (t' @ s) th'" (is "?P span'") + by auto + have "length (actions_of {th'} t) \ (SOME span. ?P span)" + proof(rule someI2[where a = span']) + fix span + assume fs: "?P span" + show "length (actions_of {th'} t) \ span" + proof(induct rule:ind) + case h: (Cons e t) + interpret ve': extend_highest_gen s th prio tm "e#t" using h by simp + show ?case + proof(cases "length (actions_of {th'} t) < span") + case True + thus ?thesis by (simp add:actions_of_def) + next + case False + have "actor e \ th'" + proof + assume otherwise: "actor e = th'" + from ve'.blockers_no_create [OF assms _ this] + have "\ isCreate e" by auto + from PIP_actorE[OF h(2) otherwise this] + have "th' \ runing (t @ s)" . + moreover have "th' \ runing (t @ s)" + proof - + from False h(4) h(5) have "length (actions_of {th'} t) = span" by simp + from fs[rule_format, OF h(3) this] have "detached (t @ s) th'" . + from extend_highest_gen.detached_not_runing[OF h(3) this] assms + show ?thesis by (auto simp:blockers_def) + qed + ultimately show False by simp + qed + with h show ?thesis by (auto simp:actions_of_def) + qed + qed (simp add: actions_of_def) + next + from span' + show "?P span'" . + qed + thus ?thesis by (unfold span_def, auto) +qed + +text {* + The following lemma is a corollary of @{thm le_span}, which says + the total operations of blockers is bounded by the + sum of @{term span}-values of all blockers. +*} +lemma len_action_blockers: + "length (actions_of blockers t) \ (\ th' \ blockers . span th')" + (is "?L \ ?R") +proof - + from len_actions_of_sigma[OF finite_blockers] + have "?L = (\th'\blockers. length (actions_of {th'} t))" by simp + also have "... \ ?R" + by (rule Groups_Big.setsum_mono, insert le_span, auto) + finally show ?thesis . +qed + +text {* + By combining forgoing lemmas, it is proved that the number of + blocked occurrences of the most urgent thread @{term th} is finitely bounded: +*} +theorem priority_inversion_is_finite: + "occs (\ t'. th \ runing (t'@s)) t \ + 1 + ((\ th' \ blockers . span th') + BC)" (is "?L \ ?R" is "_ \ 1 + (?A + ?B)" ) +proof - + from bound_priority_inversion + 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 . + ultimately show ?thesis by simp +qed + +text {* + The following lemma says the most urgent thread @{term th} will get as many + as operations it wishes, provided @{term t} is long enough. + Similar result can also be obtained under the slightly weaker assumption where + @{term BC} is lifted to a function and @{text "BC t"} is a portion of + @{term "length t"}. +*} +theorem enough_actions_for_the_highest: + "length t - ((\ th' \ blockers . span th') + BC) \ length (actions_of {th} t)" + using actions_split create_bc len_action_blockers by linarith + end + +end