theory ExtGG
imports PrioG CpsG
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
(* ccc *)
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 {*
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.
*}
lemma pv_blocked_pre:
assumes th'_in: "th' \<in> threads (t@s)"
and 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' = th"
proof(rule preced_unique)
show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R")
proof -
have "?L = cp (t@s) th'"
by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp)
also have "... = cp (t @ s) th" using otherwise
by (metis (mono_tags, lifting) mem_Collect_eq
runing_def th_cp_max vat_t.max_cp_readys_threads)
also have "... = ?R" by (metis th_cp_preced th_kept)
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
lemmas pv_blocked = pv_blocked_pre[folded detached_eq]
lemma runing_precond_pre:
fixes th'
assumes th'_in: "th' \<in> threads s"
and eq_pv: "cntP s th' = cntV s th'"
and neq_th': "th' \<noteq> th"
shows "th' \<in> threads (t@s) \<and>
cntP (t@s) th' = cntV (t@s) th'"
proof(induct rule:ind)
case (Cons e t)
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(cases e)
case (P thread cs)
show ?thesis
proof -
have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"
proof -
have "thread \<noteq> th'"
proof -
have "step (t@s) (P thread cs)" using Cons P by auto
thus ?thesis
proof(cases)
assume "thread \<in> runing (t@s)"
moreover have "th' \<notin> runing (t@s)" using Cons(5)
by (metis neq_th' vat_t.pv_blocked_pre)
ultimately show ?thesis by auto
qed
qed with Cons show ?thesis
by (unfold P, simp add:cntP_def cntV_def count_def)
qed
moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold P, simp)
ultimately show ?thesis by auto
qed
next
case (V thread cs)
show ?thesis
proof -
have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"
proof -
have "thread \<noteq> th'"
proof -
have "step (t@s) (V thread cs)" using Cons V by auto
thus ?thesis
proof(cases)
assume "thread \<in> runing (t@s)"
moreover have "th' \<notin> runing (t@s)" using Cons(5)
by (metis neq_th' vat_t.pv_blocked_pre)
ultimately show ?thesis by auto
qed
qed with Cons show ?thesis
by (unfold V, simp add:cntP_def cntV_def count_def)
qed
moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold V, simp)
ultimately show ?thesis by auto
qed
next
case (Create thread prio')
show ?thesis
proof -
have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"
proof -
have "thread \<noteq> th'"
proof -
have "step (t@s) (Create thread prio')" using Cons Create by auto
thus ?thesis using Cons(5) by (cases, auto)
qed with Cons show ?thesis
by (unfold Create, simp add:cntP_def cntV_def count_def)
qed
moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold Create, simp)
ultimately show ?thesis by auto
qed
next
case (Exit thread)
show ?thesis
proof -
have neq_thread: "thread \<noteq> th'"
proof -
have "step (t@s) (Exit thread)" using Cons Exit by auto
thus ?thesis apply (cases) using Cons(5)
by (metis neq_th' vat_t.pv_blocked_pre)
qed
hence "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" using Cons
by (unfold Exit, simp add:cntP_def cntV_def count_def)
moreover have "th' \<in> threads ((e # t) @ s)" using Cons neq_thread
by (unfold Exit, simp)
ultimately show ?thesis by auto
qed
next
case (Set thread prio')
with Cons
show ?thesis
by (auto simp:cntP_def cntV_def count_def)
qed
next
case Nil
with assms
show ?case by auto
qed
text {* Changing counting balance to detachedness *}
lemmas runing_precond_pre_dtc = runing_precond_pre
[folded vat_t.detached_eq vat_s.detached_eq]
lemma runing_precond:
fixes th'
assumes th'_in: "th' \<in> threads s"
and neq_th': "th' \<noteq> th"
and is_runing: "th' \<in> runing (t@s)"
shows "cntP s th' > cntV s th'"
using assms
proof -
have "cntP s th' \<noteq> cntV s th'"
by (metis is_runing neq_th' pv_blocked_pre runing_precond_pre th'_in)
moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto
ultimately show ?thesis by auto
qed
lemma moment_blocked_pre:
assumes neq_th': "th' \<noteq> th"
and th'_in: "th' \<in> threads ((moment i t)@s)"
and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'"
shows "cntP ((moment (i+j) t)@s) th' = cntV ((moment (i+j) t)@s) th' \<and>
th' \<in> threads ((moment (i+j) t)@s)"
proof -
interpret h_i: red_extend_highest_gen _ _ _ _ _ i
by (unfold_locales)
interpret h_j: red_extend_highest_gen _ _ _ _ _ "i+j"
by (unfold_locales)
interpret h: extend_highest_gen "((moment i t)@s)" th prio tm "moment j (restm i t)"
proof(unfold_locales)
show "vt (moment i t @ s)" by (metis h_i.vt_t)
next
show "th \<in> threads (moment i t @ s)" by (metis h_i.th_kept)
next
show "preced th (moment i t @ s) =
Max (cp (moment i t @ s) ` threads (moment i t @ s))"
by (metis h_i.th_cp_max h_i.th_cp_preced h_i.th_kept)
next
show "preced th (moment i t @ s) = Prc prio tm" by (metis h_i.th_kept preced_th)
next
show "vt (moment j (restm i t) @ moment i t @ s)"
using moment_plus_split by (metis add.commute append_assoc h_j.vt_t)
next
fix th' prio'
assume "Create th' prio' \<in> set (moment j (restm i t))"
thus "prio' \<le> prio" using assms
by (metis Un_iff add.commute h_j.create_low moment_plus_split set_append)
next
fix th' prio'
assume "Set th' prio' \<in> set (moment j (restm i t))"
thus "th' \<noteq> th \<and> prio' \<le> prio"
by (metis Un_iff add.commute h_j.set_diff_low moment_plus_split set_append)
next
fix th'
assume "Exit th' \<in> set (moment j (restm i t))"
thus "th' \<noteq> th"
by (metis Un_iff add.commute h_j.exit_diff moment_plus_split set_append)
qed
show ?thesis
by (metis add.commute append_assoc eq_pv h.runing_precond_pre
moment_plus_split neq_th' th'_in)
qed
lemma moment_blocked_eqpv:
assumes neq_th': "th' \<noteq> th"
and th'_in: "th' \<in> threads ((moment i t)@s)"
and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'"
and le_ij: "i \<le> j"
shows "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th' \<and>
th' \<in> threads ((moment j t)@s) \<and>
th' \<notin> runing ((moment j t)@s)"
proof -
from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij
have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'"
and h2: "th' \<in> threads ((moment j t)@s)" by auto
moreover have "th' \<notin> runing ((moment j t)@s)"
proof -
interpret h: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales)
show ?thesis
using h.pv_blocked_pre h1 h2 neq_th' by auto
qed
ultimately show ?thesis by auto
qed
(* The foregoing two lemmas are preparation for this one, but
in long run can be combined. Maybe I am wrong.
*)
lemma moment_blocked:
assumes neq_th': "th' \<noteq> th"
and th'_in: "th' \<in> threads ((moment i t)@s)"
and dtc: "detached (moment i t @ s) th'"
and le_ij: "i \<le> j"
shows "detached (moment j t @ s) th' \<and>
th' \<in> threads ((moment j t)@s) \<and>
th' \<notin> runing ((moment j t)@s)"
proof -
interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales)
interpret h_j: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales)
have cnt_i: "cntP (moment i t @ s) th' = cntV (moment i t @ s) th'"
by (metis dtc h_i.detached_elim)
from moment_blocked_eqpv[OF neq_th' th'_in cnt_i le_ij]
show ?thesis by (metis h_j.detached_intro)
qed
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
text {*
The situation when @{term "th"} is blocked is analyzed by the following lemmas.
*}
text {*
The following lemmas shows the running thread @{text "th'"}, if it is different from
@{term th}, must be live at the very beginning. By the term {\em the very beginning},
we mean the moment where the formal investigation starts, i.e. the moment (or state)
@{term s}.
*}
lemma runing_inversion_0:
assumes neq_th': "th' \<noteq> th"
and runing': "th' \<in> runing (t@s)"
shows "th' \<in> threads s"
proof -
-- {* The proof is by contradiction: *}
{ assume otherwise: "\<not> ?thesis"
have "th' \<notin> runing (t @ s)"
proof -
-- {* Since @{term "th'"} is running at time @{term "t@s"}, so it exists that time. *}
have th'_in: "th' \<in> threads (t@s)" using runing' by (simp add:runing_def readys_def)
-- {* However, @{text "th'"} does not exist at very beginning. *}
have th'_notin: "th' \<notin> threads (moment 0 t @ s)" using otherwise
by (metis append.simps(1) moment_zero)
-- {* Therefore, there must be a moment during @{text "t"}, when
@{text "th'"} came into being. *}
-- {* Let us suppose the moment being @{text "i"}: *}
from p_split_gen[OF th'_in th'_notin]
obtain i where lt_its: "i < length t"
and le_i: "0 \<le> i"
and pre: " th' \<notin> threads (moment i t @ s)" (is "th' \<notin> threads ?pre")
and post: "(\<forall>i'>i. th' \<in> threads (moment i' t @ s))" by (auto)
interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales)
interpret h_i': red_extend_highest_gen _ _ _ _ _ "(Suc i)" by (unfold_locales)
from lt_its have "Suc i \<le> length t" by auto
-- {* Let us also suppose the event which makes this change is @{text e}: *}
from moment_head[OF this] obtain e where
eq_me: "moment (Suc i) t = e # moment i t" by blast
hence "vt (e # (moment i t @ s))" by (metis append_Cons h_i'.vt_t)
hence "PIP (moment i t @ s) e" by (cases, simp)
-- {* It can be derived that this event @{text "e"}, which
gives birth to @{term "th'"} must be a @{term "Create"}: *}
from create_pre[OF this, of th']
obtain prio where eq_e: "e = Create th' prio"
by (metis append_Cons eq_me lessI post pre)
have h1: "th' \<in> threads (moment (Suc i) t @ s)" using post by auto
have h2: "cntP (moment (Suc i) t @ s) th' = cntV (moment (Suc i) t@ s) th'"
proof -
have "cntP (moment i t@s) th' = cntV (moment i t@s) th'"
by (metis h_i.cnp_cnv_eq pre)
thus ?thesis by (simp add:eq_me eq_e cntP_def cntV_def count_def)
qed
show ?thesis
using moment_blocked_eqpv [OF neq_th' h1 h2, of "length t"] lt_its moment_ge
by auto
qed
with `th' \<in> runing (t@s)`
have False by simp
} thus ?thesis by auto
qed
text {*
The second lemma says, if the running thread @{text th'} is different from
@{term th}, then this @{text th'} must in the possession of some resources
at the very beginning.
To ease the reasoning of resource possession of one particular thread,
we used two auxiliary functions @{term cntV} and @{term cntP},
which are the counters of @{term P}-operations and
@{term V}-operations respectively.
If the number of @{term V}-operation is less than the number of
@{term "P"}-operations, the thread must have some unreleased resource.
*}
lemma runing_inversion_1: (* ddd *)
assumes neq_th': "th' \<noteq> th"
and runing': "th' \<in> runing (t@s)"
-- {* thread @{term "th'"} is a live on in state @{term "s"} and
it has some unreleased resource. *}
shows "th' \<in> threads s \<and> cntV s th' < cntP s th'"
proof -
-- {* The proof is a simple composition of @{thm runing_inversion_0} and
@{thm runing_precond}: *}
-- {* By applying @{thm runing_inversion_0} to assumptions,
it can be shown that @{term th'} is live in state @{term s}: *}
have "th' \<in> threads s" using runing_inversion_0[OF assms(1,2)] .
-- {* Then the thesis is derived easily by applying @{thm runing_precond}: *}
with runing_precond [OF this neq_th' runing'] show ?thesis by simp
qed
text {*
The following lemma is just a rephrasing of @{thm runing_inversion_1}:
*}
lemma runing_inversion_2:
assumes runing': "th' \<in> runing (t@s)"
shows "th' = th \<or> (th' \<noteq> th \<and> th' \<in> threads s \<and> cntV s th' < cntP s th')"
proof -
from runing_inversion_1[OF _ runing']
show ?thesis by auto
qed
lemma runing_inversion_3:
assumes runing': "th' \<in> runing (t@s)"
and neq_th: "th' \<noteq> th"
shows "th' \<in> threads s \<and> (cntV s th' < cntP s th' \<and> cp (t@s) th' = preced th s)"
by (metis neq_th runing' runing_inversion_2 runing_preced_inversion)
lemma runing_inversion_4:
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"
apply (metis neq_th runing' runing_inversion_2)
apply (metis neq_th pv_blocked runing' runing_inversion_2 runing_precond_pre_dtc)
by (metis neq_th runing' runing_inversion_3)
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 *)
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