--- a/Correctness.thy Tue Jun 07 13:51:39 2016 +0100
+++ b/Correctness.thy Thu Jun 09 23:01:36 2016 +0100
@@ -498,12 +498,12 @@
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)"
+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 runing_def, auto)
+ 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 .
@@ -525,7 +525,7 @@
@{text th'}s @{term cp}-value equals to its own precedence.
On the other hand, since @{text th'} is running, by @{thm
- runing_preced_inversion}, its @{term cp}-value equals to the
+ running_preced_inversion}, its @{term cp}-value equals to the
precedence of @{term th}.
Combining the above two resukts we have that @{text th'} and @{term
@@ -538,13 +538,13 @@
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)"
+ shows "th' \<notin> running (t@s)"
proof
- assume otherwise: "th' \<in> runing (t@s)"
+ assume otherwise: "th' \<in> running (t@s)"
show False
proof -
have th'_in: "th' \<in> threads (t@s)"
- using otherwise readys_threads runing_def by auto
+ using otherwise readys_threads running_def by auto
have "th' = th"
proof(rule preced_unique)
-- {* The proof goes like this:
@@ -559,12 +559,12 @@
equals its @{term preced}-value: *}
have "?L = cp (t@s) th'"
by (unfold cp_eq cpreced_def eq_dependants vat_t.eq_pv_dependants[OF eq_pv], simp)
- -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion},
+ -- {* Since @{term "th'"} is running, by @{thm running_preced_inversion},
its @{term cp}-value equals @{term "preced th s"},
which equals to @{term "?R"} by simplification: *}
also have "... = ?R"
- thm runing_preced_inversion
- using runing_preced_inversion[OF otherwise] by simp
+ thm running_preced_inversion
+ using running_preced_inversion[OF otherwise] by simp
finally show ?thesis .
qed
qed (auto simp: th'_in th_kept)
@@ -600,11 +600,11 @@
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> runing (t@s)"
+ 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> runing (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
@@ -618,8 +618,8 @@
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> runing (t@s)" by (cases, auto)
- moreover have "th' \<notin> runing (t@s)"
+ 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
@@ -637,7 +637,7 @@
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)"
+ shows "th' \<notin> running (t@s)"
using assms
by (simp add: eq_pv_blocked eq_pv_persist)
@@ -645,8 +645,8 @@
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)"
+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
@@ -660,9 +660,9 @@
-- {* 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
+ 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
@@ -677,40 +677,40 @@
The proof is a simple combination of the results above:
*}
-lemma runing_threads_inv:
- assumes runing': "th' \<in> runing (t@s)"
+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> runing (t @ 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 runing' show False by simp
+ 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 runing_inversion: (* ddd, one of the main lemmas to present *)
- assumes runing': "th' \<in> runing (t@s)"
+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 runing_threads_inv[OF assms]
+ from running_threads_inv[OF assms]
show "th' \<in> threads s" .
next
- from runing_cntP_cntV_inv[OF runing' neq_th]
+ from running_cntP_cntV_inv[OF running' neq_th]
show "\<not>detached s th'" using vat_s.detached_eq by simp
next
- from runing_preced_inversion[OF runing']
+ from running_preced_inversion[OF running']
show "cp (t@s) th' = preced th s" .
qed
@@ -723,13 +723,13 @@
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 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> runing (t@s)"
+ assumes "th \<notin> running (t@s)"
obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
- "th' \<in> runing (t@s)"
+ "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
@@ -737,15 +737,15 @@
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"}. *}
+ @{term th} holds the highest @{term cp}-value, it must be @{term "running"}. *}
moreover have "th \<notin> readys (t@s)"
- using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto
+ 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> runing (t@s)"
+ 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")
@@ -783,8 +783,8 @@
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)
+ 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)"
@@ -793,26 +793,26 @@
qed
lemma (* new proof of th_blockedE *)
- assumes "th \<notin> runing (t @ s)"
+ assumes "th \<notin> running (t @ s)"
obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
- "th' \<in> runing (t @ s)"
+ "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 "runing"}. This would
+ highest @{term cp}-value, it must be @{term "running"}. This would
violate our assumption. *}
have "th \<notin> readys (t @ s)"
- using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto
+ 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> runing (t @ s)"
+ 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")
@@ -852,8 +852,8 @@
qed
-- {* Now, since @{term th'} holds the highest @{term cp}-value in readys,
- it is @{term runing} by definition. *}
- with `th' \<in> readys (t @ s)` show "th' \<in> runing (t @ s)" by (simp add: runing_def)
+ 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}: *}
@@ -863,8 +863,8 @@
qed
lemma th_blockedE_pretty:
- assumes "th \<notin> runing (t@s)"
- shows "\<exists>th'. Th th' \<in> ancestors (RAG (t @ s)) (Th th) \<and> th' \<in> runing (t@s)"
+ 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 {*
@@ -873,8 +873,8 @@
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)")
+lemma live: "running (t@s) \<noteq> {}"
+proof(cases "th \<in> running (t@s)")
case True thus ?thesis by auto
next
case False
@@ -882,25 +882,25 @@
qed
lemma blockedE:
- assumes "th \<notin> runing (t@s)"
+ assumes "th \<notin> running (t@s)"
obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
- "th' \<in> runing (t@s)"
+ "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 runing_inversion(2) runing_preced_inversion runing_threads_inv th_blockedE)
+by (metis assms running_inversion(2) running_preced_inversion running_threads_inv th_blockedE)
-lemma detached_not_runing:
+lemma detached_not_running:
assumes "detached (t@s) th'"
and "th' \<noteq> th"
- shows "th' \<notin> runing (t@s)"
+ shows "th' \<notin> running (t@s)"
proof
- assume otherwise: "th' \<in> runing (t @ s)"
+ 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:runing_def)
+ 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
@@ -911,7 +911,7 @@
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 runing_def readys_def, auto)
+ 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
@@ -945,11 +945,11 @@
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 runingE:
- assumes "th' \<in> runing (t@s)"
+lemma runningE:
+ assumes "th' \<in> running (t@s)"
obtains (is_th) "th' = th"
| (is_other) "th' \<in> blockers"
- using assms blockers_def runing_inversion(2) by auto
+ using assms blockers_def running_inversion(2) by auto
text {*
The following lemma shows that the number of blockers are finite.
@@ -1009,11 +1009,11 @@
have False
proof(cases)
case h: (thread_exit)
- hence "th' \<in> readys (t@s)" by (auto simp:runing_def)
+ 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_runing[OF this] assms[unfolded blockers_def]
- have "th' \<notin> runing (t @ s)" by auto
+ 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
@@ -1094,7 +1094,7 @@
*}
lemma actions_th_occs_pre:
assumes "t = e'#t'"
- shows "length (actions_of {th} t) \<le> occs (\<lambda> t'. th \<in> runing (t'@s)) 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')
@@ -1111,7 +1111,7 @@
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> runing s" by simp
+ 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
@@ -1124,7 +1124,7 @@
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> runing (t' @ s)) t1"
+ 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")
@@ -1132,7 +1132,7 @@
from ve'.th_no_create[OF _ this]
have "\<not> isCreate e" by auto
from PIP_actorE[OF h(2) True this]
- have "th \<in> runing (t@s)" by simp
+ 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
@@ -1149,12 +1149,12 @@
lemma really needed in later proofs.
*}
lemma actions_th_occs:
- shows "length (actions_of {th} t) \<le> occs (\<lambda> t'. th \<in> runing (t'@s)) t"
+ 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> runing (t' @ s)) t'" .
- moreover have "... \<le> occs (\<lambda>t'. th \<in> runing (t' @ s)) t"
+ 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)
@@ -1187,10 +1187,10 @@
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> runing (t@s)")
+ proof(cases "actor e \<in> running (t@s)")
case True
thus ?thesis
- proof(rule ve.runingE)
+ 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"
@@ -1273,17 +1273,17 @@
*}
theorem bound_priority_inversion:
- "occs (\<lambda> t'. th \<notin> runing (t'@s)) t \<le>
+ "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> runing (t'@s))"
+ 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> runing (t'@s)) t" (is "?L1 \<le> ?R1")
+ \<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
@@ -1400,12 +1400,12 @@
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> runing (t @ s)" .
- moreover have "th' \<notin> runing (t @ s)"
+ have "th' \<in> running (t @ s)" .
+ moreover have "th' \<notin> running (t @ s)"
proof -
from False h(4) h(5) have "length (actions_of {th'} t) = span" by simp
from fs[rule_format, OF h(3) this] have "detached (t @ s) th'" .
- from extend_highest_gen.detached_not_runing[OF h(3) this] assms
+ from extend_highest_gen.detached_not_running[OF h(3) this] assms
show ?thesis by (auto simp:blockers_def)
qed
ultimately show False by simp
@@ -1441,7 +1441,7 @@
blocked occurrences of the most urgent thread @{term th} is finitely bounded:
*}
theorem priority_inversion_is_finite:
- "occs (\<lambda> t'. th \<notin> runing (t'@s)) t \<le>
+ "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