--- 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)) \<le> 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 \<subseteq> A"
- and "c \<in> 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 \<in> 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' \<in> set t \<Longrightarrow> prio' \<le> prio"
and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio"
and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> th"
@@ -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 \<in> threads (t @ s) \<and>
- 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' \<in> running (t @ s)"
- shows "cp (t @ s) th' = preced th s"
+ assumes running': "th' \<in> running (t@s)"
+ shows "cp (t@s) th' = preced th s" (is "?L = ?R")
proof -
- have "th' \<in> 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 "\<dots> = 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 "\<dots> = ?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' \<in> readys (t@s)"
- and dp: "th' \<in> 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' \<subseteq> threads (t @ s)"
- using readys_def th'_in vat_t.subtree_tG_thread by auto
- next
- show "th \<in> 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 \<notin> running (t@s)"
+ obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
+ "th' \<in> 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 \<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 "running"}. *}
+ moreover have "th \<notin> 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' \<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> 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) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th'))"
+ by (unfold cp_alt_def1, simp)
+ also have "... = (the_preced (t @ s) \<circ> the_thread) (Th th)"
+ proof(rule image_Max_subset)
+ show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads)
+ next
+ show "subtree (tRAG (t @ s)) (Th th') \<subseteq> Th ` threads (t @ s)"
+ by (metis Range.intros dp trancl_range vat_t.rg_RAG_threads vat_t.subtree_tRAG_thread)
+ next
+ show "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp
+ by (unfold tRAG_subtree_eq, auto simp:subtree_def)
+ next
+ show "Max ((the_preced (t @ s) \<circ> the_thread) ` Th ` threads (t @ s)) =
+ (the_preced (t @ s) \<circ> the_thread) (Th th)" (is "Max ?L = _")
+ proof -
+ have "?L = the_preced (t @ s) ` threads (t @ s)"
+ by (unfold image_comp, rule image_cong, auto)
+ thus ?thesis using max_preced the_preced_def by auto
+ qed
+ qed
+ 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' \<in> 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' \<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 th_blockedE: (* ddd, the other main lemma to be presented: *)
- obtains th' where "th' \<in> nancestors (tG (t @ s)) th"
+lemma (* new proof of th_blockedE *)
+ assumes "th \<notin> running (t @ s)"
+ obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
"th' \<in> running (t @ s)"
proof -
- -- {* According to @{thm vat_t.th_chain_to_ready}, there is a
- ready ancestor of @{term th}. *}
- have "\<exists>th' \<in> nancestors (tG (t @ s)) th. th' \<in> readys (t @ s)"
- using th_kept vat_t.th_chain_to_ready_tG by auto
- then obtain th' where th'_in: "th' \<in> readys (t @ s)"
- and dp: "th' \<in> 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 \<notin> readys (t @ s)"
+ using assms running_def th_cp_max vat_t.max_cp_readys_threads by auto
+ then have "\<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
+ then 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 first show that this @{term th'} is running. *}
+ have "th' \<in> 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) \<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
+ 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' \<in> readys (t @ s)`
- have "th' \<in> 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' \<in> readys (t @ s)` show "th' \<in> 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' \<in> nancestors (tG (t @ s)) th"
- using dp unfolding nancestors_def2 by simp
+ 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 th_blockedE_pretty:
- shows "\<exists>th' \<in> nancestors (tG (t @ s)) th. th' \<in> running (t @ s)"
-using th_blockedE assms
-by blast
-
+ assumes "th \<notin> running (t@s)"
+ shows "\<exists>th'. Th th' \<in> ancestors (RAG (t @ s)) (Th th) \<and> th' \<in> 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) \<noteq> {}"
-using th_blockedE by auto
+lemma live: "running (t@s) \<noteq> {}"
+proof(cases "th \<in> running (t@s)")
+ case True thus ?thesis by auto
+next
+ case False
+ thus ?thesis using th_blockedE by auto
+qed
lemma blockedE:
- assumes "th \<notin> running (t @ s)"
- obtains th' where "th' \<in> nancestors (tG (t @ s)) th"
- "th' \<in> running (t @ s)"
+ assumes "th \<notin> running (t@s)"
+ obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
+ "th' \<in> running (t@s)"
"th' \<in> threads s"
"\<not>detached s th'"
- "cp (t @ s) th' = preced th s"
+ "cp (t@s) th' = preced th s"
"th' \<noteq> th"
-proof -
- obtain th' where a: "th' \<in> nancestors (tG (t @ s)) th" "th' \<in> running (t @ s)"
- using th_blockedE by blast
- moreover
- from a(2) have b: "th' \<in> threads s"
- using running_threads_inv assms by metis
- moreover
- from a(2) have "\<not>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' \<noteq> th" using assms a(2) by blast
- ultimately show ?thesis using that by metis
-qed
-
-
-lemma nblockedE:
- assumes "th \<notin> running (t @ s)"
- obtains th' where "th' \<in> ancestors (tG (t @ s)) th"
- "th' \<in> running (t @ s)"
- "th' \<in> threads s"
- "\<not>detached s th'"
- "cp (t @ s) th' = preced th s"
- "th' \<noteq> 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' \<noteq> th"
- shows "th' \<notin> running (t @ s)"
+ shows "th' \<notin> running (t@s)"
proof
assume otherwise: "th' \<in> 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 (\<lambda> t'. th \<notin> running (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> running (t'@s))"
- from occs_le[of ?Q t]
- thm occs_le
- have "?L \<le> (1 + length t) - occs ?Q t" by simp
- also have "... \<le> ?R"
- proof -
- thm actions_th_occs actions_split
- have "length t - (length (actions_of blockers t) + length (filter (isCreate) t))
- \<le> occs (\<lambda> t'. th \<in> running (t'@s)) t" (is "?L1 \<le> ?R1")
- proof -
- from actions_split 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
+(* 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' (\<lambda>t'. th \<in> running (t' @ s)) t"
+ sorry
+*)
+
+
+lemma actions_th_occs'_pre:
+ assumes "t = e'#t'"
+ shows "length (actions_of {th} t) \<le> occs' (\<lambda> t'. th \<in> 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 \<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> 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) \<le> occs' (\<lambda>t'. th \<in> running (t' @ s)) t"
+ (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> 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' (\<lambda> t'. th \<in> running (t'@s)) t = length (filter (\<lambda> s'. th \<in> running s') (up_to s t))"
+proof -
+ have h: "((\<lambda>s'. th \<in> running s') \<circ> (\<lambda>t'. t' @ s)) = (\<lambda> t'. th \<in> 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' (\<lambda> t'. th \<notin> running (t'@s)) t = length (filter (\<lambda> s'. th \<notin> running s') (up_to s t))"
+proof -
+ have h: "((\<lambda>s'. th \<notin> running s') \<circ> (\<lambda>t'. t' @ s)) = (\<lambda> t'. th \<notin> 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) \<le> occs' (\<lambda> t'. th \<in> running (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> running (t' @ s)) t" .
+ thus ?thesis by simp
+qed (auto simp:actions_of_def)
+
+theorem bound_priority_inversion':
+ "occs' (\<lambda> t'. th \<notin> running (t'@s)) t \<le>
+ (length (actions_of blockers t) + length (filter (isCreate) t))"
+ (is "?L \<le> ?R")
+proof -
+ let ?Q = "(\<lambda> t'. th \<in> running (t'@s))"
+ from occs_len'[of ?Q t]
+ have "?L \<le> (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> running (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
+
+theorem bound_priority_inversion:
+ "occs (\<lambda> t'. th \<notin> running (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> running (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> running (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
@@ -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' \<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 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' \<in> blockers \<Longrightarrow>
(\<exists> span. \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow>
\<not> detached (t'@s) th' \<longrightarrow> 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:
- "\<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> length (filter isCreate t') \<le> BC"
+ "\<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> length (filter isCreate t') < BC"
begin
text {*
@@ -1367,7 +1545,7 @@
*}
lemma create_bc:
- shows "length (filter isCreate t) \<le> 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' (\<lambda> t'. th \<notin> running (t'@s)) t \<le>
+ ((\<Sum> th' \<in> blockers . span th') + BC)" (is "?L \<le> ?R" is "_ \<le> (?A + ?B)" )
+proof -
+ from bound_priority_inversion'
+ have "?L \<le> (length (actions_of blockers t) + length (filter isCreate t))"
+ (is "_ \<le> (?A' + ?B')") .
+ moreover have "?A' \<le> ?A" using len_action_blockers .
+ moreover have "?B' \<le> ?B" using create_bc by auto
+ ultimately show ?thesis by simp
+qed
+
+
+theorem priority_inversion_is_finite_upto:
+ "length [s'\<leftarrow>up_to s t . th \<notin> running s'] \<le>
+ ((\<Sum> th' \<in> blockers . span th') + BC)"
+ using priority_inversion_is_finite'[unfolded occs'_replacement2] by simp
+
theorem priority_inversion_is_finite:
"occs (\<lambda> t'. th \<notin> running (t'@s)) t \<le>
1 + ((\<Sum> th' \<in> blockers . span th') + BC)" (is "?L \<le> ?R" is "_ \<le> 1 + (?A + ?B)" )
@@ -1462,7 +1659,7 @@
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 .
+ moreover have "?B' \<le> ?B" using create_bc by auto
ultimately show ?thesis by simp
qed
@@ -1477,11 +1674,7 @@
"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
-thm actions_split
-
end
-
-
end