theory Correctness
imports PIPBasics
begin
(* hg cat -r 176 Correctness.thy *)
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 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
(* 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
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 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"}.
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: "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" (is "?L = ?R")
proof -
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
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.
(* eee *)
The proof is by contradiction:
If @{text th'} is running, it can be derived that @{text "th' = th"} which
is in contradiction with the assume @{text "th' \<noteq> th"}.
The derivation of @{text "th' = th"} uses @{thm preced_unique}, according to which
we need to show the @{text th'} and @{text th} have the same precedence. The proof
of this is based on the combination of the following two facts:
From @{thm vat_t.detached_intro} and assume
@{text "cntP (t@s) th' = cntV (t@s) th'"} it can be derived that
@{text th'} is detached. From this and @{thm detached_cp_preced}
it following the precedence of @{text th'} equals to its own @{text cp}-value.
Since @{text th'} is running, from this and @{thm
running_preced_inversion}, the precedence of @{text th'} equals to
the precedence of @{term th}.
By combining the above two results we have that @{text th'} and @{term
th} have the same precedence.
*}
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"
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` *}
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: *)
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 (* 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}, 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
-- {* 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 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:
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
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> {}"
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 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"
"th' \<noteq> th"
by (metis assms running_inversion(2) running_preced_inversion running_threads_inv th_blockedE)
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 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 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 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: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.
*}
end
(* ccc *)
fun postfixes where
"postfixes [] = []" |
"postfixes (x#xs) = xs # postfixes xs"
definition "up_to s t = map (\<lambda> t'. t'@s) (postfixes t)"
fun upto where
"upto s [] = []" |
"upto s (e # es) = (es @ s) # upto s es"
value "up_to [s3, s2, s1] [e5, e4, e3, e2, e1] "
value "upto [s3, s2, s1] [e5, e4, e3, e2, e1] "
lemma "upto s t = up_to s t"
apply(induct t arbitrary: s)
apply(auto simp add: up_to_def)
done
definition "occs' Q tt = length (filter Q (postfixes tt))"
lemma occs'_nil [simp]: "occs' Q [] = 0"
by (unfold occs'_def, simp)
lemma occs'_cons [simp]:
shows "occs' Q (x#xs) = (if Q xs then 1 + occs' Q xs else occs' Q xs)"
using assms
by (unfold occs'_def, simp)
lemma occs_len': "occs' Q t + occs' (\<lambda>e. \<not> Q e) t = length t"
unfolding occs'_def
by (induct t, auto)
lemma [simp]: "Q [] \<Longrightarrow> occs' Q [] + 1 = occs Q []"
by (unfold occs'_def, simp)
lemma [simp]: "\<not> Q [] \<Longrightarrow> occs' Q [] = occs Q []"
by (unfold occs'_def, simp)
lemma [simp]: "l \<noteq> [] \<Longrightarrow> Q l \<Longrightarrow> Suc (occs Q (tl l)) = occs Q l"
by (induct l, auto)
lemma [simp]: "l \<noteq> [] \<Longrightarrow> \<not> Q l \<Longrightarrow> (occs Q (tl l)) = occs Q l"
by (induct l, auto)
lemma "l \<noteq> [] \<Longrightarrow> occs' Q l = occs Q (tl l)"
proof(unfold occs'_def, induct l)
case (Cons a l)
show ?case
proof(cases "l = []")
case False
from Cons(1)[OF this] have "length (filter Q (postfixes l)) = occs Q (tl l)" .
with False
show ?thesis by auto
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
(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 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)"
-- {*
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.
*}
-- {* 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') < BC"
begin
text {*
The following lemmas show that the number of @{term Create}-operations is bound by @{term BC}:
*}
lemma create_bc:
shows "length (filter isCreate t) < BC"
by (meson extend_highest_gen_axioms finite_create)
text {*
The following @{term span}-function gives the upper bound of
operations take by each particular blocker.
*}
definition "span th' = (SOME span.
\<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>
((\<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)" )
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 by auto
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