--- 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 (\<lambda> e. \<not> Q e) t \<le> (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 \<le> ?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) \<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)"
@@ -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' \<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 metis
+qed
+
+lemma (* new proof of th_blockedE *)
+ 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 -
+ -- {* 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) \<circ> 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') \<subseteq> 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 \<in> the_thread ` subtree (tRAG (t @ s)) (Th th')"
+ proof -
+ have "Th th \<in> 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 \<notin> runing (t@s)"
+ obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
+ "th' \<in> runing (t@s)"
+ "th' \<in> threads s"
+ "\<not>detached s th'"
+ "cp (t@s) th' = preced th s"
+ "th' \<noteq> 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' \<noteq> th"
+ shows "th' \<notin> runing (t@s)"
+proof
+ assume otherwise: "th' \<in> 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' \<in> threads (t @ s) \<Longrightarrow> th \<in> threads (t @ s) \<Longrightarrow> th' = th" .
+ moreover have "th' \<in> threads (t@s)"
+ using otherwise by (unfold runing_def readys_def, auto)
+ moreover have "th \<in> threads (t@s)" by (simp add: th_kept)
+ ultimately have "th' = th" by metis
+ with assms(2) show False by 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'. \<not>detached s th' \<and> th' \<noteq> th}"
+
+text {*
+ The following lemma shows that the definition of @{term "blockers"} is correct,
+ i.e. blockers do block @{term "th"}. It is a very simple corollary of @{thm blockedE}.
+*}
+lemma runingE:
+ assumes "th' \<in> runing (t@s)"
+ obtains (is_th) "th' = th"
+ | (is_other) "th' \<in> 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'. \<not>detached s th'}"
+ proof -
+ have "finite {th'. Th th' \<in> Field (RAG s)}"
+ proof -
+ have "{th'. Th th' \<in> Field (RAG s)} \<subseteq> threads s"
+ proof
+ fix x
+ assume "x \<in> {th'. Th th' \<in> Field (RAG s)}"
+ thus "x \<in> threads s" using vat_s.RAG_threads by auto
+ qed
+ moreover have "finite ..." by (simp add: vat_s.finite_threads)
+ ultimately show ?thesis using rev_finite_subset by auto
+ qed
+ thus ?thesis by (unfold detached_test, auto)
+ qed
+ thus ?thesis unfolding blockers_def by 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' \<in> blockers"
+ shows "th' \<in> threads (t@s)"
+proof(induct rule:ind)
+ case Nil
+ from assms[unfolded blockers_def detached_test]
+ have "Th th' \<in> Field (RAG s)" by simp
+ from vat_s.RAG_threads[OF this]
+ show ?case by 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' \<notin> threads ((e # t) @ s)"
+ from threads_Exit[OF h(5)] this have eq_e: "e = Exit th'" by auto
+ from h(2)[unfolded this]
+ have False
+ proof(cases)
+ case h: (thread_exit)
+ hence "th' \<in> readys (t@s)" by (auto simp: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' \<notin> 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' \<in> blockers"
+ and "e \<in> set t"
+ and "actor e = th'"
+ shows "\<not> isCreate e"
+ using assms(2,3)
+proof(induct rule:ind)
+ case h: (Cons e' t)
+ interpret et: extend_highest_gen s th prio tm t
+ using h by simp
+ { assume eq_e: "e = e'"
+ from et.blockers_kept assms
+ have "th' \<in> threads (t @ s)" by auto
+ with h(2,7)
+ have ?case
+ by (unfold eq_e, cases, auto simp:blockers_def)
+ } with h
+ show ?case by 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 \<in> set t"
+ and "actor e = th"
+ shows "\<not> 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 \<in> 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) \<le> occs (\<lambda> t'. th \<in> 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 \<le> ?R")
+ proof(cases t)
+ case Nil
+ show ?thesis
+ proof(cases "actor e = th")
+ case True
+ from ve'.th_no_create[OF _ this]
+ have "\<not> isCreate e" by auto
+ from PIP_actorE[OF h(2) True this] Nil
+ have "th \<in> 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) \<le> occs (\<lambda>t'. th \<in> runing (t' @ s)) t1"
+ (is "?F t \<le> ?G t1") .
+ show ?thesis
+ proof(cases "actor e = th")
+ case True
+ from ve'.th_no_create[OF _ this]
+ have "\<not> isCreate e" by auto
+ from PIP_actorE[OF h(2) True this]
+ have "th \<in> 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) \<le> occs (\<lambda> t'. th \<in> runing (t'@s)) t"
+proof(cases t)
+ case (Cons e' t')
+ from actions_th_occs_pre[OF this]
+ have "length (actions_of {th} t) \<le> occs (\<lambda>t'. th \<in> runing (t' @ s)) t'" .
+ moreover have "... \<le> occs (\<lambda>t'. th \<in> 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 \<in> 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 \<notin> blockers" using 1
+ by (simp add:actions_of_def blockers_def)
+ thus ?thesis by (simp add:actions_of_def)
+ qed
+ moreover have "?C (e#t) = ?C t"
+ proof -
+ from ve'.th_no_create[OF _ 1]
+ have "\<not> isCreate e" by auto
+ thus ?thesis by (simp add:actions_of_def)
+ qed
+ ultimately show ?thesis using h by simp
+ next
+ assume 2: "actor e \<in> ve'.blockers"
+ have "?T (e#t) = ?T (t)"
+ proof -
+ from 2 have "actor e \<noteq> th" by (auto simp:blockers_def)
+ thus ?thesis by (auto simp:actions_of_def)
+ qed
+ moreover have "?O (e#t) = 1 + ?O(t)" using 2
+ by (auto simp:actions_of_def)
+ moreover have "?C (e#t) = ?C(t)"
+ proof -
+ from ve'.blockers_no_create[OF 2, of e]
+ have "\<not> isCreate e" by auto
+ thus ?thesis by (simp add:actions_of_def)
+ qed
+ ultimately show ?thesis using h by simp
+ qed
+ next
+ case False
+ from h(2)
+ have is_create: "isCreate e"
+ by (cases; insert False, auto)
+ have "?T (e#t) = ?T t"
+ proof -
+ have "actor e \<noteq> th"
+ proof
+ assume "actor e = th"
+ from ve'.th_no_create[OF _ this]
+ have "\<not> isCreate e" by auto
+ with is_create show False by simp
+ qed
+ thus ?thesis by (auto simp:actions_of_def)
+ qed
+ moreover have "?O (e#t) = ?O t"
+ proof -
+ have "actor e \<notin> blockers"
+ proof
+ assume "actor e \<in> blockers"
+ from ve'.blockers_no_create[OF this, of e]
+ have "\<not> isCreate e" by simp
+ with is_create show False by simp
+ qed
+ thus ?thesis by (simp add:actions_of_def)
+ qed
+ moreover have "?C (e#t) = 1 + ?C t" using is_create
+ by (auto simp:actions_of_def)
+ ultimately show ?thesis using h by simp
+ 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 (\<lambda> t'. th \<notin> runing (t'@s)) t \<le>
+ 1 + (length (actions_of blockers t) + length (filter (isCreate) t))"
+ (is "?L \<le> ?R")
+proof -
+ let ?Q = "(\<lambda> t'. th \<in> runing (t'@s))"
+ from occs_le[of ?Q t]
+ have "?L \<le> (1 + length t) - occs ?Q t" by simp
+ also have "... \<le> ?R"
+ proof -
+ have "length t - (length (actions_of blockers t) + length (filter (isCreate) t))
+ \<le> occs (\<lambda> t'. th \<in> runing (t'@s)) t" (is "?L1 \<le> ?R1")
+ proof -
+ have "?L1 = length (actions_of {th} t)" using actions_split by arith
+ also have "... \<le> ?R1" using actions_th_occs by simp
+ finally show ?thesis .
+ qed
+ thus ?thesis by simp
+ qed
+ finally show ?thesis .
+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' \<in> blockers \<Longrightarrow>
+ (\<exists> span. \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow>
+ length (actions_of {th'} t') = span \<longrightarrow> 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:
+ "\<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> length (filter isCreate t') \<le> BC"
+begin
+
+text {*
+ The following lemmas show that the number of @{term Create}-operations is bound by @{term BC}:
+*}
+
+lemma create_bc:
+ shows "length (filter isCreate t) \<le> BC"
+ by (meson extend_highest_gen_axioms finite_create)
+
+text {*
+ The following @{term span}-function gives the upper bound of
+ operations take by each particular blocker.
+*}
+definition "span th' = (SOME span.
+ \<forall>t'. extend_highest_gen s th prio tm t' \<longrightarrow>
+ length (actions_of {th'} t') = span \<longrightarrow> 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' \<in> blockers"
+ shows "length (actions_of {th'} t) \<le> span th'"
+proof -
+ from finite_span[OF assms(1)] obtain span'
+ where span': "\<forall>t'. extend_highest_gen s th prio tm t' \<longrightarrow>
+ length (actions_of {th'} t') = span' \<longrightarrow> detached (t' @ s) th'" (is "?P span'")
+ by auto
+ have "length (actions_of {th'} t) \<le> (SOME span. ?P span)"
+ proof(rule someI2[where a = span'])
+ fix span
+ assume fs: "?P span"
+ show "length (actions_of {th'} t) \<le> span"
+ proof(induct rule:ind)
+ case h: (Cons e t)
+ interpret ve': extend_highest_gen s th prio tm "e#t" using h by simp
+ show ?case
+ proof(cases "length (actions_of {th'} t) < span")
+ case True
+ thus ?thesis by (simp add:actions_of_def)
+ next
+ case False
+ have "actor e \<noteq> th'"
+ proof
+ assume otherwise: "actor e = th'"
+ from ve'.blockers_no_create [OF assms _ this]
+ have "\<not> isCreate e" by auto
+ from PIP_actorE[OF h(2) otherwise this]
+ have "th' \<in> runing (t @ s)" .
+ moreover have "th' \<notin> 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) \<le> (\<Sum> th' \<in> blockers . span th')"
+ (is "?L \<le> ?R")
+proof -
+ from len_actions_of_sigma[OF finite_blockers]
+ have "?L = (\<Sum>th'\<in>blockers. length (actions_of {th'} t))" by simp
+ also have "... \<le> ?R"
+ by (rule Groups_Big.setsum_mono, insert le_span, auto)
+ finally show ?thesis .
+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 (\<lambda> t'. th \<notin> runing (t'@s)) t \<le>
+ 1 + ((\<Sum> th' \<in> blockers . span th') + BC)" (is "?L \<le> ?R" is "_ \<le> 1 + (?A + ?B)" )
+proof -
+ from bound_priority_inversion
+ have "?L \<le> 1 + (length (actions_of blockers t) + length (filter isCreate t))"
+ (is "_ \<le> 1 + (?A' + ?B')") .
+ moreover have "?A' \<le> ?A" using len_action_blockers .
+ moreover have "?B' \<le> ?B" using create_bc .
+ ultimately show ?thesis by 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 - ((\<Sum> th' \<in> blockers . span th') + BC) \<le> length (actions_of {th} t)"
+ using actions_split create_bc len_action_blockers by linarith
+
end
+
+end