theory Correctness+ −
imports PIPBasics+ −
begin+ −
+ −
lemma actions_of_len_cons [iff]: + −
"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"+ −
and "\<forall> x \<in> B. f x \<le> f b"+ −
shows "Max (f ` B) = f b"+ −
using assms+ −
using Max_eqI by blast + −
+ −
lemma image_Max_subset:+ −
assumes "finite A"+ −
and "B \<subseteq> A"+ −
and "a \<in> B"+ −
and "Max (f ` A) = f a"+ −
shows "Max (f ` B) = f a"+ −
proof(rule image_Max_eqI)+ −
show "finite B"+ −
using assms(1) assms(2) finite_subset by auto + −
next+ −
show "a \<in> B" using assms by simp+ −
next+ −
show "\<forall>x\<in>B. f x \<le> f a"+ −
by (metis Max_ge assms(1) assms(2) assms(4) + −
finite_imageI image_eqI subsetCE) + −
qed+ −
+ −
text {*+ −
The following locale @{text "highest_gen"} sets the basic context for our+ −
investigation: supposing thread @{text th} holds the highest @{term cp}-value+ −
in state @{text s}, which means the task for @{text th} is the + −
most urgent. We want to show that + −
@{text th} is treated correctly by PIP, which means+ −
@{text th} will not be blocked unreasonably by other less urgent+ −
threads. + −
*}+ −
locale highest_gen =+ −
fixes s th prio tm+ −
assumes vt_s: "vt s"+ −
and threads_s: "th \<in> threads s"+ −
and highest: "preced th s = Max ((cp s)`threads s)"+ −
-- {* The internal structure of @{term th}'s precedence is exposed:*}+ −
and preced_th: "preced th s = Prc prio tm" + −
+ −
-- {* @{term s} is a valid trace, so it will inherit all results derived for+ −
a valid trace: *}+ −
sublocale highest_gen < vat_s?: valid_trace "s"+ −
by (unfold_locales, insert vt_s, simp)+ −
+ −
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+ −
+ −
text {*+ −
@{term tm} is the time when the precedence of @{term th} is set, so + −
@{term tm} must be a valid moment index into @{term s}.+ −
*}+ −
lemma lt_tm: "tm < length s"+ −
by (insert preced_tm_lt[OF threads_s preced_th], simp)+ −
+ −
text {*+ −
Since @{term th} holds the highest precedence and @{text "cp"}+ −
is the highest precedence of all threads in the sub-tree of + −
@{text "th"} and @{text th} is among these threads, + −
its @{term cp} must equal to its precedence:+ −
*}+ −
+ −
lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R")+ −
proof -+ −
have "?L \<le> ?R"+ −
by (unfold highest, rule Max_ge, + −
auto simp:threads_s finite_threads)+ −
moreover have "?R \<le> ?L"+ −
by (unfold vat_s.cp_rec, rule Max_ge, + −
auto simp:the_preced_def vat_s.fsbttRAGs.finite_children)+ −
ultimately show ?thesis by auto+ −
qed+ −
+ −
lemma highest_cp_preced: "cp s th = Max (the_preced s ` threads s)"+ −
using eq_cp_s_th highest max_cp_eq the_preced_def by presburger+ −
+ −
+ −
lemma highest_preced_thread: "preced th s = Max (the_preced s ` threads s)"+ −
by (fold eq_cp_s_th, unfold highest_cp_preced, simp)+ −
+ −
lemma highest': "cp s th = Max (cp s ` threads s)"+ −
by (simp add: eq_cp_s_th highest)+ −
+ −
end+ −
+ −
locale extend_highest_gen = highest_gen + + −
fixes t + −
assumes vt_t: "vt (t @ s)"+ −
and create_low: "Create th' prio' \<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"+ −
+ −
sublocale extend_highest_gen < vat_t?: valid_trace "t@s"+ −
by (unfold_locales, insert vt_t, simp)+ −
+ −
lemma step_back_vt_app: + −
assumes vt_ts: "vt (t@s)" + −
shows "vt s"+ −
proof -+ −
from vt_ts show ?thesis+ −
proof(induct t)+ −
case Nil+ −
from Nil show ?case by auto+ −
next+ −
case (Cons e t)+ −
assume ih: " vt (t @ s) \<Longrightarrow> vt s"+ −
and vt_et: "vt ((e # t) @ s)"+ −
show ?case+ −
proof(rule ih)+ −
show "vt (t @ s)"+ −
proof(rule step_back_vt)+ −
from vt_et show "vt (e # t @ s)" by simp+ −
qed+ −
qed+ −
qed+ −
qed+ −
+ −
+ −
context extend_highest_gen+ −
begin+ −
+ −
lemma ind [consumes 0, case_names Nil Cons, induct type]:+ −
assumes + −
h0: "R []"+ −
and h2: "\<And> e t. \<lbrakk>vt (t@s); step (t@s) e; + −
extend_highest_gen s th prio tm t; + −
extend_highest_gen s th prio tm (e#t); R t\<rbrakk> \<Longrightarrow> R (e#t)"+ −
shows "R t"+ −
proof -+ −
from vt_t extend_highest_gen_axioms show ?thesis+ −
proof(induct t)+ −
from h0 show "R []" .+ −
next+ −
case (Cons e t')+ −
assume ih: "\<lbrakk>vt (t' @ s); extend_highest_gen s th prio tm t'\<rbrakk> \<Longrightarrow> R t'"+ −
and vt_e: "vt ((e # t') @ s)"+ −
and et: "extend_highest_gen s th prio tm (e # t')"+ −
from vt_e and step_back_step have stp: "step (t'@s) e" by auto+ −
from vt_e and step_back_vt have vt_ts: "vt (t'@s)" by auto+ −
show ?case+ −
proof(rule h2 [OF vt_ts stp _ _ _ ])+ −
show "R t'"+ −
proof(rule ih)+ −
from et show ext': "extend_highest_gen s th prio tm t'"+ −
by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt)+ −
next+ −
from vt_ts show "vt (t' @ s)" .+ −
qed+ −
next+ −
from et show "extend_highest_gen s th prio tm (e # t')" .+ −
next+ −
from et show ext': "extend_highest_gen s th prio tm t'"+ −
by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt)+ −
qed+ −
qed+ −
qed+ −
+ −
+ −
lemma th_kept: "th \<in> threads (t @ s) \<and> + −
preced th (t @ s) = preced th s" (is "?Q t") + −
proof -+ −
show ?thesis+ −
proof(induct rule:ind)+ −
case Nil+ −
from threads_s+ −
show ?case+ −
by auto+ −
next+ −
case (Cons e t)+ −
interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto+ −
interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto+ −
show ?case+ −
proof(cases e)+ −
case (Create thread prio)+ −
show ?thesis+ −
proof -+ −
from Cons and Create have "step (t@s) (Create thread prio)" by auto+ −
hence "th \<noteq> thread"+ −
proof(cases)+ −
case thread_create+ −
with Cons show ?thesis by auto+ −
qed+ −
hence "preced th ((e # t) @ s) = preced th (t @ s)"+ −
by (unfold Create, auto simp:preced_def)+ −
moreover note Cons+ −
ultimately show ?thesis+ −
by (auto simp:Create)+ −
qed+ −
next+ −
case (Exit thread)+ −
from h_e.exit_diff and Exit+ −
have neq_th: "thread \<noteq> th" by auto+ −
with Cons+ −
show ?thesis+ −
by (unfold Exit, auto simp:preced_def)+ −
next+ −
case (P thread cs)+ −
with Cons+ −
show ?thesis + −
by (auto simp:P preced_def)+ −
next+ −
case (V thread cs)+ −
with Cons+ −
show ?thesis + −
by (auto simp:V preced_def)+ −
next+ −
case (Set thread prio')+ −
show ?thesis+ −
proof -+ −
from h_e.set_diff_low and Set+ −
have "th \<noteq> thread" by auto+ −
hence "preced th ((e # t) @ s) = preced th (t @ s)"+ −
by (unfold Set, auto simp:preced_def)+ −
moreover note Cons+ −
ultimately show ?thesis+ −
by (auto simp:Set)+ −
qed+ −
qed+ −
qed+ −
qed+ −
+ −
text {*+ −
According to @{thm th_kept}, thread @{text "th"} has its liveness status+ −
and precedence kept along the way of @{text "t"}. The following lemma+ −
shows that this preserved precedence of @{text "th"} remains as the highest+ −
along the way of @{text "t"}.+ −
+ −
The proof goes by induction over @{text "t"} using the specialized+ −
induction rule @{thm ind}, followed by case analysis of each possible + −
operations of PIP. All cases follow the same pattern rendered by the + −
generalized introduction rule @{thm "image_Max_eqI"}. + −
+ −
The very essence is to show that precedences, no matter whether they + −
are newly introduced or modified, are always lower than the one held + −
by @{term "th"}, which by @{thm th_kept} is preserved along the way.+ −
*}+ −
lemma max_kept: + −
shows "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"+ −
proof(induct rule:ind)+ −
case Nil+ −
from highest_preced_thread+ −
show ?case by simp+ −
next+ −
case (Cons e t)+ −
interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto+ −
interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto+ −
show ?case+ −
proof(cases e)+ −
case (Create thread prio')+ −
show ?thesis (is "Max (?f ` ?A) = ?t")+ −
proof -+ −
-- {* The following is the common pattern of each branch of the case analysis. *}+ −
-- {* The major part is to show that @{text "th"} holds the highest precedence: *}+ −
have "Max (?f ` ?A) = ?f th"+ −
proof(rule image_Max_eqI)+ −
show "finite ?A" using h_e.finite_threads by auto + −
next+ −
show "th \<in> ?A" using h_e.th_kept by auto + −
next+ −
show "\<forall>x\<in>?A. ?f x \<le> ?f th"+ −
proof + −
fix x+ −
assume "x \<in> ?A"+ −
hence "x = thread \<or> x \<in> threads (t@s)" by (auto simp:Create)+ −
thus "?f x \<le> ?f th"+ −
proof+ −
assume "x = thread"+ −
thus ?thesis + −
apply (simp add:Create the_preced_def preced_def, fold preced_def)+ −
using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 + −
preced_th by force+ −
next+ −
assume h: "x \<in> threads (t @ s)"+ −
from Cons(2)[unfolded Create] + −
have "x \<noteq> thread" using h by (cases, auto)+ −
hence "?f x = the_preced (t@s) x" + −
by (simp add:Create the_preced_def preced_def)+ −
hence "?f x \<le> Max (the_preced (t@s) ` threads (t@s))"+ −
by (simp add: h_t.finite_threads h)+ −
also have "... = ?f th"+ −
by (metis Cons.hyps(5) h_e.th_kept the_preced_def) + −
finally show ?thesis .+ −
qed+ −
qed+ −
qed+ −
-- {* The minor part is to show that the precedence of @{text "th"} + −
equals to preserved one, given by the foregoing lemma @{thm th_kept} *}+ −
also have "... = ?t" using h_e.th_kept the_preced_def by auto+ −
-- {* Then it follows trivially that the precedence preserved+ −
for @{term "th"} remains the maximum of all living threads along the way. *}+ −
finally show ?thesis .+ −
qed + −
next + −
case (Exit thread)+ −
show ?thesis (is "Max (?f ` ?A) = ?t")+ −
proof -+ −
have "Max (?f ` ?A) = ?f th"+ −
proof(rule image_Max_eqI)+ −
show "finite ?A" using h_e.finite_threads by auto + −
next+ −
show "th \<in> ?A" using h_e.th_kept by auto + −
next+ −
show "\<forall>x\<in>?A. ?f x \<le> ?f th"+ −
proof + −
fix x+ −
assume "x \<in> ?A"+ −
hence "x \<in> threads (t@s)" by (simp add: Exit) + −
hence "?f x \<le> Max (?f ` threads (t@s))" + −
by (simp add: h_t.finite_threads) + −
also have "... \<le> ?f th" + −
apply (simp add:Exit the_preced_def preced_def, fold preced_def)+ −
using Cons.hyps(5) h_t.th_kept the_preced_def by auto+ −
finally show "?f x \<le> ?f th" .+ −
qed+ −
qed+ −
also have "... = ?t" using h_e.th_kept the_preced_def by auto+ −
finally show ?thesis .+ −
qed + −
next+ −
case (P thread cs)+ −
with Cons+ −
show ?thesis by (auto simp:preced_def the_preced_def)+ −
next+ −
case (V thread cs)+ −
with Cons+ −
show ?thesis by (auto simp:preced_def the_preced_def)+ −
next + −
case (Set thread prio')+ −
show ?thesis (is "Max (?f ` ?A) = ?t")+ −
proof -+ −
have "Max (?f ` ?A) = ?f th"+ −
proof(rule image_Max_eqI)+ −
show "finite ?A" using h_e.finite_threads by auto + −
next+ −
show "th \<in> ?A" using h_e.th_kept by auto + −
next+ −
show "\<forall>x\<in>?A. ?f x \<le> ?f th"+ −
proof + −
fix x+ −
assume h: "x \<in> ?A"+ −
show "?f x \<le> ?f th"+ −
proof(cases "x = thread")+ −
case True+ −
moreover have "the_preced (Set thread prio' # t @ s) thread \<le> the_preced (t @ s) th"+ −
proof -+ −
have "the_preced (t @ s) th = Prc prio tm" + −
using h_t.th_kept preced_th by (simp add:the_preced_def)+ −
moreover have "prio' \<le> prio" using Set h_e.set_diff_low by auto+ −
ultimately show ?thesis by (insert lt_tm, auto simp:the_preced_def preced_def)+ −
qed+ −
ultimately show ?thesis+ −
by (unfold Set, simp add:the_preced_def preced_def)+ −
next+ −
case False+ −
then have "?f x = the_preced (t@s) x"+ −
by (simp add:the_preced_def preced_def Set)+ −
also have "... \<le> Max (the_preced (t@s) ` threads (t@s))"+ −
using Set h h_t.finite_threads by auto + −
also have "... = ?f th" by (metis Cons.hyps(5) h_e.th_kept the_preced_def) + −
finally show ?thesis .+ −
qed+ −
qed+ −
qed+ −
also have "... = ?t" using h_e.th_kept the_preced_def by auto+ −
finally show ?thesis .+ −
qed + −
qed+ −
qed+ −
+ −
lemma max_preced: "preced th (t@s) = Max (the_preced (t@s) ` (threads (t@s)))"+ −
by (insert th_kept max_kept, auto)+ −
+ −
text {*+ −
The reason behind the following lemma is that:+ −
Since @{term "cp"} is defined as the maximum precedence + −
of those threads contained in the sub-tree of node @{term "Th th"} + −
in @{term "RAG (t@s)"}, and all these threads are living threads, and + −
@{term "th"} is also among them, the maximum precedence of + −
them all must be the one for @{text "th"}.+ −
*}+ −
lemma th_cp_max_preced: + −
"cp (t@s) th = Max (the_preced (t@s) ` (threads (t@s)))" (is "?L = ?R") + −
proof -+ −
let ?f = "the_preced (t@s)"+ −
have "?L = ?f th"+ −
proof(unfold cp_alt_def, rule image_Max_eqI)+ −
show "finite {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"+ −
proof -+ −
have "{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)} = + −
the_thread ` {n . n \<in> subtree (RAG (t @ s)) (Th th) \<and>+ −
(\<exists> th'. n = Th th')}"+ −
by (force)+ −
moreover have "finite ..." by (simp add: vat_t.fsbtRAGs.finite_subtree) + −
ultimately show ?thesis by simp+ −
qed+ −
next+ −
show "th \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"+ −
by (auto simp:subtree_def)+ −
next+ −
show "\<forall>x\<in>{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}.+ −
the_preced (t @ s) x \<le> the_preced (t @ s) th"+ −
proof+ −
fix th'+ −
assume "th' \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"+ −
hence "Th th' \<in> subtree (RAG (t @ s)) (Th th)" by auto+ −
moreover have "... \<subseteq> Field (RAG (t @ s)) \<union> {Th th}"+ −
by (meson subtree_Field)+ −
ultimately have "Th th' \<in> ..." by auto+ −
hence "th' \<in> threads (t@s)" + −
proof+ −
assume "Th th' \<in> {Th th}"+ −
thus ?thesis using th_kept by auto + −
next+ −
assume "Th th' \<in> Field (RAG (t @ s))"+ −
thus ?thesis using vat_t.not_in_thread_isolated by blast + −
qed+ −
thus "the_preced (t @ s) th' \<le> the_preced (t @ s) th"+ −
by (metis Max_ge finite_imageI finite_threads image_eqI + −
max_kept th_kept the_preced_def)+ −
qed+ −
qed+ −
also have "... = ?R" by (simp add: max_preced the_preced_def) + −
finally show ?thesis .+ −
qed+ −
+ −
lemma th_cp_max[simp]: "Max (cp (t@s) ` threads (t@s)) = cp (t@s) th"+ −
using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger+ −
+ −
lemma [simp]: "Max (cp (t@s) ` threads (t@s)) = Max (the_preced (t@s) ` threads (t@s))"+ −
by (simp add: th_cp_max_preced)+ −
+ −
lemma [simp]: "Max (the_preced (t@s) ` threads (t@s)) = the_preced (t@s) th"+ −
using max_kept th_kept the_preced_def by auto+ −
+ −
lemma [simp]: "the_preced (t@s) th = preced th (t@s)"+ −
using the_preced_def by auto+ −
+ −
lemma [simp]: "preced th (t@s) = preced th s"+ −
by (simp add: th_kept)+ −
+ −
lemma [simp]: "cp s th = preced th s"+ −
by (simp add: eq_cp_s_th)+ −
+ −
lemma th_cp_preced [simp]: "cp (t@s) th = preced th s"+ −
by (fold max_kept, unfold th_cp_max_preced, simp)+ −
+ −
lemma preced_less:+ −
assumes th'_in: "th' \<in> threads s"+ −
and neq_th': "th' \<noteq> th"+ −
shows "preced th' s < preced th s"+ −
using assms+ −
by (metis Max.coboundedI finite_imageI highest not_le order.trans + −
preced_linorder rev_image_eqI threads_s vat_s.finite_threads + −
vat_s.le_cp)+ −
+ −
section {* The `blocking thread` *}+ −
+ −
text {* + −
The purpose of PIP is to ensure that the most + −
urgent thread @{term th} is not blocked unreasonably. + −
Therefore, a clear picture of the blocking thread is essential + −
to assure people that the purpose is fulfilled. + −
+ −
In this section, we are going to derive a series of lemmas + −
with finally give rise to a picture of the blocking thread. + −
+ −
By `blocking thread`, we mean a thread in running state but + −
different from thread @{term th}.+ −
*}+ −
+ −
text {*+ −
The following lemmas shows that the @{term cp}-value + −
of the blocking thread @{text th'} equals to the highest+ −
precedence in the whole system.+ −
*}+ −
lemma running_preced_inversion:+ −
assumes running': "th' \<in> running (t @ s)"+ −
shows "cp (t @ s) th' = preced th s"+ −
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 .+ −
finally show ?thesis .+ −
qed+ −
+ −
text {*+ −
+ −
The following lemma shows how the counters for @{term "P"} and+ −
@{term "V"} operations relate to the running threads in the states+ −
@{term s} and @{term "t @ s"}. The lemma shows that if a thread's+ −
@{term "P"}-count equals its @{term "V"}-count (which means it no+ −
longer has any resource in its possession), it cannot be a running+ −
thread.+ −
+ −
The proof is by contraction with the assumption @{text "th' \<noteq> th"}.+ −
The key is the use of @{thm eq_pv_dependants} to derive the+ −
emptiness of @{text th'}s @{term dependants}-set from the balance of+ −
its @{term P} and @{term V} counts. From this, it can be shown+ −
@{text th'}s @{term cp}-value equals to its own precedence.+ −
+ −
On the other hand, since @{text th'} is running, by @{thm+ −
running_preced_inversion}, its @{term cp}-value equals to the+ −
precedence of @{term th}.+ −
+ −
Combining the above two resukts we have that @{text th'} and @{term+ −
th} have the same precedence. By uniqueness of precedences, we have+ −
@{text "th' = th"}, which is in contradiction with the assumption+ −
@{text "th' \<noteq> th"}.+ −
+ −
*} + −
+ −
lemma eq_pv_blocked: (* ddd *)+ −
assumes neq_th': "th' \<noteq> th"+ −
and eq_pv: "cntP (t@s) th' = cntV (t@s) th'"+ −
shows "th' \<notin> running (t@s)"+ −
proof+ −
assume otherwise: "th' \<in> running (t@s)"+ −
show False+ −
proof -+ −
have th'_in: "th' \<in> threads (t@s)"+ −
using otherwise readys_threads running_def by auto + −
have "th' = th"+ −
proof(rule preced_unique)+ −
-- {* The proof goes like this: + −
it is first shown that the @{term preced}-value of @{term th'} + −
equals to that of @{term th}, then by uniqueness + −
of @{term preced}-values (given by lemma @{thm preced_unique}), + −
@{term th'} equals to @{term th}: *}+ −
show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R")+ −
proof -+ −
-- {* Since the counts of @{term th'} are balanced, the subtree+ −
of it contains only itself, so, its @{term cp}-value+ −
equals its @{term preced}-value: *}+ −
have "?L = cp (t@s) th'"+ −
by (simp add: detached_cp_preced eq_pv vat_t.detached_intro)+ −
-- {* Since @{term "th'"} is running, by @{thm running_preced_inversion},+ −
its @{term cp}-value equals @{term "preced th s"}, + −
which equals to @{term "?R"} by simplification: *}+ −
also have "... = ?R" + −
thm running_preced_inversion+ −
using running_preced_inversion[OF otherwise] by simp+ −
finally show ?thesis .+ −
qed+ −
qed (auto simp: th'_in th_kept)+ −
with `th' \<noteq> th` show ?thesis by simp+ −
qed+ −
qed+ −
+ −
text {*+ −
The following lemma is the extrapolation of @{thm eq_pv_blocked}.+ −
It says if a thread, different from @{term th}, + −
does not hold any resource at the very beginning,+ −
it will keep hand-emptied in the future @{term "t@s"}.+ −
*}+ −
lemma eq_pv_persist: (* ddd *)+ −
assumes neq_th': "th' \<noteq> th"+ −
and eq_pv: "cntP s th' = cntV s th'"+ −
shows "cntP (t@s) th' = cntV (t@s) th'"+ −
proof(induction rule:ind) -- {* The proof goes by induction. *}+ −
-- {* The nontrivial case is for the @{term Cons}: *}+ −
case (Cons e t)+ −
-- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *}+ −
interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp+ −
interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp+ −
interpret vat_es: valid_trace_e "t@s" e using Cons(1,2) by (unfold_locales, auto)+ −
show ?case+ −
proof -+ −
-- {* It can be proved that @{term cntP}-value of @{term th'} does not change+ −
by the happening of event @{term e}: *}+ −
have "cntP ((e#t)@s) th' = cntP (t@s) th'"+ −
proof(rule ccontr) -- {* Proof by contradiction. *}+ −
-- {* Suppose @{term cntP}-value of @{term th'} is changed by @{term e}: *}+ −
assume otherwise: "cntP ((e # t) @ s) th' \<noteq> cntP (t @ s) th'"+ −
from cntP_diff_inv[OF this[simplified]]+ −
obtain cs' where "e = P th' cs'" by auto+ −
from vat_es.pip_e[unfolded this]+ −
have "th' \<in> running (t@s)" + −
by (cases, simp)+ −
-- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis+ −
shows @{term th'} can not be running at moment @{term "t@s"}: *}+ −
moreover have "th' \<notin> running (t@s)" + −
using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] .+ −
-- {* Contradiction is finally derived: *}+ −
ultimately show False by simp+ −
qed+ −
-- {* It can also be proved that @{term cntV}-value of @{term th'} does not change+ −
by the happening of event @{term e}: *}+ −
-- {* The proof follows exactly the same pattern as the case for @{term cntP}-value: *}+ −
moreover have "cntV ((e#t)@s) th' = cntV (t@s) th'"+ −
proof(rule ccontr) -- {* Proof by contradiction. *}+ −
assume otherwise: "cntV ((e # t) @ s) th' \<noteq> cntV (t @ s) th'"+ −
from cntV_diff_inv[OF this[simplified]]+ −
obtain cs' where "e = V th' cs'" by auto+ −
from vat_es.pip_e[unfolded this]+ −
have "th' \<in> running (t@s)" by (cases, auto)+ −
moreover have "th' \<notin> running (t@s)"+ −
using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] .+ −
ultimately show False by simp+ −
qed+ −
-- {* Finally, it can be shown that the @{term cntP} and @{term cntV} + −
value for @{term th'} are still in balance, so @{term th'} + −
is still hand-emptied after the execution of event @{term e}: *}+ −
ultimately show ?thesis using Cons(5) by metis+ −
qed+ −
qed (auto simp:eq_pv)+ −
+ −
text {*+ −
By combining @{thm eq_pv_blocked} and @{thm eq_pv_persist},+ −
it can be derived easily that @{term th'} can not be running in the future:+ −
*}+ −
lemma eq_pv_blocked_persist:+ −
assumes neq_th': "th' \<noteq> th"+ −
and eq_pv: "cntP s th' = cntV s th'"+ −
shows "th' \<notin> running (t@s)"+ −
using assms+ −
by (simp add: eq_pv_blocked eq_pv_persist) + −
+ −
text {*+ −
The following lemma shows the blocking thread @{term th'}+ −
must hold some resource in the very beginning. + −
*}+ −
lemma running_cntP_cntV_inv: (* ddd *)+ −
assumes is_running: "th' \<in> running (t@s)"+ −
and neq_th': "th' \<noteq> th"+ −
shows "cntP s th' > cntV s th'"+ −
using assms+ −
proof -+ −
-- {* First, it can be shown that the number of @{term P} and+ −
@{term V} operations can not be equal for thred @{term th'} *}+ −
have "cntP s th' \<noteq> cntV s th'"+ −
proof+ −
-- {* The proof goes by contradiction, suppose otherwise: *}+ −
assume otherwise: "cntP s th' = cntV s th'"+ −
-- {* By applying @{thm eq_pv_blocked_persist} to this: *}+ −
from eq_pv_blocked_persist[OF neq_th' otherwise] + −
-- {* we have that @{term th'} can not be running at moment @{term "t@s"}: *}+ −
have "th' \<notin> running (t@s)" .+ −
-- {* This is obvious in contradiction with assumption @{thm is_running} *}+ −
thus False using is_running by simp+ −
qed+ −
-- {* However, the number of @{term V} is always less or equal to @{term P}: *}+ −
moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto+ −
-- {* Thesis is finally derived by combining the these two results: *}+ −
ultimately show ?thesis by auto+ −
qed+ −
+ −
+ −
text {*+ −
The following lemmas shows the blocking thread @{text th'} must be live + −
at the very beginning, i.e. the moment (or state) @{term s}. + −
+ −
The proof is a simple combination of the results above:+ −
*}+ −
lemma running_threads_inv: + −
assumes running': "th' \<in> running (t@s)"+ −
and neq_th': "th' \<noteq> th"+ −
shows "th' \<in> threads s"+ −
proof(rule ccontr) -- {* Proof by contradiction: *}+ −
assume otherwise: "th' \<notin> threads s" + −
have "th' \<notin> running (t @ s)"+ −
proof -+ −
from vat_s.cnp_cnv_eq[OF otherwise]+ −
have "cntP s th' = cntV s th'" .+ −
from eq_pv_blocked_persist[OF neq_th' this]+ −
show ?thesis .+ −
qed+ −
with running' show False by simp+ −
qed+ −
+ −
text {*+ −
The following lemma summarizes several foregoing + −
lemmas to give an overall picture of the blocking thread @{text "th'"}:+ −
*}+ −
lemma running_inversion: (* ddd, one of the main lemmas to present *)+ −
assumes running': "th' \<in> running (t@s)"+ −
and neq_th: "th' \<noteq> th"+ −
shows "th' \<in> threads s"+ −
and "\<not>detached s th'"+ −
and "cp (t@s) th' = preced th s"+ −
proof -+ −
from running_threads_inv[OF assms]+ −
show "th' \<in> threads s" .+ −
next+ −
from running_cntP_cntV_inv[OF running' neq_th]+ −
show "\<not>detached s th'" using vat_s.detached_eq by simp+ −
next+ −
from running_preced_inversion[OF running']+ −
show "cp (t@s) th' = preced th s" .+ −
qed+ −
+ −
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'"} + −
in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).+ −
+ −
Now, since @{term readys}-set is non-empty, there must be+ −
one in it which holds the highest @{term cp}-value, which, by definition, + −
is the @{term 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: *)+ −
obtains th' where "th' \<in> nancestors (tG (t @ s)) 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+ −
+ −
-- {* We are going to first show that this @{term th'} is running. *}+ −
+ −
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) + −
+ −
-- {* 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+ −
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+ −
+ −
+ −
text {*+ −
Now it is easy to see there is always a thread to run by case analysis+ −
on whether thread @{term th} is running: if the answer is yes, the + −
the running thread is obviously @{term th} itself; otherwise, the running+ −
thread is the @{text th'} given by lemma @{thm th_blockedE}.+ −
*}+ −
lemma live: "running (t @ s) \<noteq> {}"+ −
using th_blockedE by auto+ −
+ −
lemma blockedE:+ −
assumes "th \<notin> running (t @ s)"+ −
obtains th' where "th' \<in> nancestors (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"+ −
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+ −
+ −
+ −
lemma detached_not_running:+ −
assumes "detached (t @ s) th'"+ −
and "th' \<noteq> th"+ −
shows "th' \<notin> running (t @ s)"+ −
proof+ −
assume otherwise: "th' \<in> running (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:running_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 running_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 current locale, 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.+ −
+ −
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 runningE:+ −
assumes "th' \<in> running (t@s)"+ −
obtains (is_th) "th' = th"+ −
| (is_other) "th' \<in> blockers"+ −
using assms blockers_def running_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 does not die as long as the+ −
highest thread @{term th} is live.+ −
+ −
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:running_def)+ −
from readys_holdents_detached[OF this h(2)]+ −
have "detached (t @ s) th'" .+ −
from et.detached_not_running[OF this] assms[unfolded blockers_def]+ −
have "th' \<notin> running (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> 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)) 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> 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 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'" .+ −
moreover have "... \<le> occs (\<lambda>t'. th \<in> running (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> running (t@s)")+ −
case True+ −
thus ?thesis+ −
proof(rule ve.runningE)+ −
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> 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+ −
+ −
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> + −
\<not> detached (t'@s) th' \<longrightarrow> length (actions_of {th'} t') < span)"+ −
+ −
-- {*+ −
The difference between this @{text finite_span} and the former one is to allow the number+ −
of action steps to change with execution paths (i.e. different value of @{term "t'@s"}}).+ −
The @{term span} is a upper bound on these step numbers. + −
*}+ −
+ −
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> + −
\<not> detached (t'@s) th' \<longrightarrow> length (actions_of {th'} t') < span)"+ −
+ −
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> + −
\<not> detached (t'@s) th' \<longrightarrow> length (actions_of {th'} t') < span'" (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 "detached (t@s) th'")+ −
case True+ −
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> running (t @ s)" .+ −
moreover have "th' \<notin> running (t @ s)"+ −
proof -+ −
from extend_highest_gen.detached_not_running[OF h(3) True] 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)+ −
next+ −
case False+ −
from fs[rule_format, OF h(3) this] and actions_of_len_cons+ −
show ?thesis by (meson discrete order.trans) + −
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> running (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+ −
+ −
thm actions_split+ −
+ −
end+ −
+ −
+ −
+ −
+ −
end+ −