theory Correctness
imports PIPBasics
begin
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)
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 ((\<lambda> th'. preced th' s) ` threads s)"
by (fold max_cp_eq, unfold eq_cp_s_th, insert highest, simp)
lemma highest_preced_thread: "preced th s = Max ((\<lambda> th'. preced th' s) ` threads s)"
by (fold eq_cp_s_th, unfold highest_cp_preced, simp)
lemma highest': "cp s th = Max (cp s ` threads s)"
proof -
from highest_cp_preced max_cp_eq[symmetric]
show ?thesis by simp
qed
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 (unfold the_preced_def, 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 (smt Collect_cong Setcompr_eq_image mem_Collect_eq the_thread.simps)
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: "cp (t@s) th = Max (cp (t@s) ` threads (t@s))"
using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger
lemma th_cp_preced: "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)
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 runing_preced_inversion:
assumes runing': "th' \<in> runing (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 runing_def, auto)
also have "\<dots> = ?R"
by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads)
finally show ?thesis .
qed
section {* The `blocking thread` *}
text {*
Counting of the number of @{term "P"} and @{term "V"} operations
is the cornerstone of a large number of the following proofs.
The reason is that this counting is quite easy to calculate and
convenient to use in the reasoning.
The following lemma shows that the counting controls whether
a thread is running or not.
*} (* ccc *)
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> runing (t@s)"
proof
assume otherwise: "th' \<in> runing (t@s)"
show False
proof -
have th'_in: "th' \<in> threads (t@s)"
using otherwise readys_threads runing_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 (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp)
-- {* Since @{term "th'"} is running by @{thm otherwise},
it has the highest @{term cp}-value, by definition,
which in turn equals to the @{term cp}-value of @{term th}. *}
also have "... = ?R"
using runing_preced_inversion[OF otherwise] th_kept by simp
finally show ?thesis .
qed
qed (auto simp: th'_in th_kept)
moreover have "th' \<noteq> th" using neq_th' .
ultimately 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
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'"
-- {* Then the actor of @{term e} must be @{term th'} and @{term e}
must be a @{term P}-event: *}
hence "isP e" "actor e = th'" by (auto simp:cntP_diff_inv)
with vat_t.actor_inv[OF Cons(2)]
-- {* According to @{thm actor_inv}, @{term th'} must be running at
the moment @{term "t@s"}: *}
have "th' \<in> runing (t@s)" by (cases e, auto)
-- {* 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> runing (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'"
hence "isV e" "actor e = th'" by (auto simp:cntV_diff_inv)
with vat_t.actor_inv[OF Cons(2)]
have "th' \<in> runing (t@s)" by (cases e, auto)
moreover have "th' \<notin> runing (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> runing (t@s)"
using assms
by (simp add: eq_pv_blocked eq_pv_persist)
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.
The following lemmas will give us such a picture:
*}
text {*
The following lemma shows the blocking thread @{term th'}
must hold some resource in the very beginning.
*}
lemma runing_cntP_cntV_inv: (* ddd *)
assumes is_runing: "th' \<in> runing (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> runing (t@s)" .
-- {* This is obvious in contradiction with assumption @{thm is_runing} *}
thus False using is_runing 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 runing_threads_inv:
assumes runing': "th' \<in> runing (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> runing (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 runing' 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 runing_inversion: (* ddd, one of the main lemmas to present *)
assumes runing': "th' \<in> runing (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 runing_threads_inv[OF assms]
show "th' \<in> threads s" .
next
from runing_cntP_cntV_inv[OF runing' neq_th]
show "\<not>detached s th'" using vat_s.detached_eq by simp
next
from runing_preced_inversion[OF runing']
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 runing}-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> runing (t@s)"
obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
"th' \<in> runing (t@s)"
proof -
-- {* According to @{thm vat_t.th_chain_to_ready}, either
@{term "th"} is in @{term "readys"} or there is path leading from it to
one thread in @{term "readys"}. *}
have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+)"
using th_kept vat_t.th_chain_to_ready by auto
-- {* However, @{term th} can not be in @{term readys}, because otherwise, since
@{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *}
moreover have "th \<notin> readys (t@s)"
using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto
-- {* So, there must be a path from @{term th} to another thread @{text "th'"} in
term @{term readys}: *}
ultimately obtain th' where th'_in: "th' \<in> readys (t@s)"
and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto
-- {* We are going to show that this @{term th'} is running. *}
have "th' \<in> runing (t@s)"
proof -
-- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *}
have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R")
proof -
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.range_in 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
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 ?thesis .
qed
-- {* Now, since @{term th'} holds the highest @{term cp}
and we have already show it is in @{term readys},
it is @{term runing} by definition. *}
with `th' \<in> readys (t@s)` show ?thesis by (simp add: runing_def)
qed
-- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}
moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)
ultimately show ?thesis using that by metis
qed
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: "runing (t@s) \<noteq> {}"
proof(cases "th \<in> runing (t@s)")
case True thus ?thesis by auto
next
case False
thus ?thesis using th_blockedE by auto
qed
end
end