--- 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
--- a/CpsG.thy Tue Jun 07 13:51:39 2016 +0100
+++ b/CpsG.thy Thu Jun 09 23:01:36 2016 +0100
@@ -4666,4 +4666,4 @@
end
-end
\ No newline at end of file
+end
--- a/Graphs.thy Tue Jun 07 13:51:39 2016 +0100
+++ b/Graphs.thy Thu Jun 09 23:01:36 2016 +0100
@@ -73,4 +73,4 @@
-end
\ No newline at end of file
+end
--- a/Implementation.thy Tue Jun 07 13:51:39 2016 +0100
+++ b/Implementation.thy Thu Jun 09 23:01:36 2016 +0100
@@ -2,14 +2,14 @@
imports PIPBasics
begin
-section {*
- This file contains lemmas used to guide the recalculation of current precedence
- after every step of execution (or system operation, or event),
+text {*
+
+ This file contains lemmas used to guide the recalculation of current
+ precedence after every step of execution (or system operation, or event),
which is the most tricky part in the implementation of PIP.
- Following convention, lemmas are grouped into locales corresponding to
- system operations, each explained in a separate section.
-*}
+ Following convention, lemmas are grouped into locales corresponding to
+ system operations, each explained in a separate section. *}
text {*
The following two lemmas are general about any valid system state,
@@ -22,17 +22,9 @@
lemma readys_root:
assumes "th \<in> readys s"
shows "root (RAG s) (Th th)"
-proof -
- { fix x
- assume "x \<in> ancestors (RAG s) (Th th)"
- hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def)
- from tranclD[OF this]
- obtain z where "(Th th, z) \<in> RAG s" by auto
- with assms(1) have False
- apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_raw)
- by (fold wq_def, blast)
- } thus ?thesis by (unfold root_def, auto)
-qed
+ unfolding root_def ancestors_def
+ using readys_RAG assms
+by (metis Collect_empty_eq Domain.DomainI trancl_domain)
lemma readys_in_no_subtree:
assumes "th \<in> readys s"
@@ -668,17 +660,18 @@
have "Th th \<notin> Range (RAG s)"
proof
assume "Th th \<in> Range (RAG s)"
- then obtain cs where "holding_raw (wq s) th cs"
- by (unfold Range_iff s_RAG_def, auto)
- with holdents_th_s[unfolded holdents_def]
- show False by (unfold holding_eq, auto)
+ then obtain cs where "holding s th cs"
+ by (simp add: holdents_RAG holdents_th_s)
+ then show False by (unfold holding_eq, auto)
qed
moreover have "Th th \<notin> Domain (RAG s)"
proof
assume "Th th \<in> Domain (RAG s)"
- then obtain cs where "waiting_raw (wq s) th cs"
- by (unfold Domain_iff s_RAG_def, auto)
- with th_ready_s show False by (unfold readys_def waiting_eq, auto)
+ then obtain cs where "waiting s th cs"
+ by (simp add: readys_RAG)
+ then show False
+ using RAG_es \<open>Th th \<in> Domain (RAG s)\<close>
+ th_not_live_es valid_trace.dm_RAG_threads vat_es.valid_trace_axioms by blast
qed
ultimately show ?thesis by (auto simp:Field_def)
qed
--- a/Journal/Paper.thy Tue Jun 07 13:51:39 2016 +0100
+++ b/Journal/Paper.thy Thu Jun 09 23:01:36 2016 +0100
@@ -31,15 +31,18 @@
Cons ("_::_" [78,77] 73) and
If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
vt ("valid'_state") and
- runing ("running") and
Prc ("'(_, _')") and
- holding ("holds") and
- waiting ("waits") and
+ holding_raw ("holds") and
+ holding ("Holds") and
+ waiting_raw ("waits") and
+ waiting ("Waits") and
+ dependants_raw ("dependants") and
+ dependants ("Dependants") and
Th ("T") and
Cs ("C") and
readys ("ready") and
preced ("prec") and
-(* preceds ("precs") and*)
+ preceds ("precs") and
cpreced ("cprec") and
cp ("cprec") and
holdents ("resources") and
@@ -330,10 +333,10 @@
\mbox{\begin{tabular}{lcl}
@{thm (lhs) threads.simps(1)} & @{text "\<equiv>"} &
@{thm (rhs) threads.simps(1)}\\
- @{thm (lhs) threads.simps(2)[where thread="th"]} & @{text "\<equiv>"} &
- @{thm (rhs) threads.simps(2)[where thread="th"]}\\
- @{thm (lhs) threads.simps(3)[where thread="th"]} & @{text "\<equiv>"} &
- @{thm (rhs) threads.simps(3)[where thread="th"]}\\
+ @{thm (lhs) threads.simps(2)} & @{text "\<equiv>"} &
+ @{thm (rhs) threads.simps(2)}\\
+ @{thm (lhs) threads.simps(3)} & @{text "\<equiv>"} &
+ @{thm (rhs) threads.simps(3)}\\
@{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\
\end{tabular}}
\end{isabelle}
@@ -345,12 +348,12 @@
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{lcl}
- @{thm (lhs) priority.simps(1)[where thread="th"]} & @{text "\<equiv>"} &
- @{thm (rhs) priority.simps(1)[where thread="th"]}\\
- @{thm (lhs) priority.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
- @{thm (rhs) priority.simps(2)[where thread="th" and thread'="th'"]}\\
- @{thm (lhs) priority.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
- @{thm (rhs) priority.simps(3)[where thread="th" and thread'="th'"]}\\
+ @{thm (lhs) priority.simps(1)} & @{text "\<equiv>"} &
+ @{thm (rhs) priority.simps(1)}\\
+ @{thm (lhs) priority.simps(2)} & @{text "\<equiv>"} &
+ @{thm (rhs) priority.simps(2)}\\
+ @{thm (lhs) priority.simps(3)} & @{text "\<equiv>"} &
+ @{thm (rhs) priority.simps(3)}\\
@{term "priority th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "priority th s"}\\
\end{tabular}}
\end{isabelle}
@@ -363,12 +366,12 @@
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{lcl}
- @{thm (lhs) last_set.simps(1)[where thread="th"]} & @{text "\<equiv>"} &
- @{thm (rhs) last_set.simps(1)[where thread="th"]}\\
- @{thm (lhs) last_set.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
- @{thm (rhs) last_set.simps(2)[where thread="th" and thread'="th'"]}\\
- @{thm (lhs) last_set.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
- @{thm (rhs) last_set.simps(3)[where thread="th" and thread'="th'"]}\\
+ @{thm (lhs) last_set.simps(1)} & @{text "\<equiv>"} &
+ @{thm (rhs) last_set.simps(1)}\\
+ @{thm (lhs) last_set.simps(2)} & @{text "\<equiv>"} &
+ @{thm (rhs) last_set.simps(2)}\\
+ @{thm (lhs) last_set.simps(3)} & @{text "\<equiv>"} &
+ @{thm (rhs) last_set.simps(3)}\\
@{term "last_set th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "last_set th s"}\\
\end{tabular}}
\end{isabelle}
@@ -380,14 +383,14 @@
state @{text s} is the pair of natural numbers defined as
\begin{isabelle}\ \ \ \ \ %%%
- @{thm preced_def[where thread="th"]}
+ @{thm preced_def}
\end{isabelle}
\noindent
We also use the abbreviation
\begin{isabelle}\ \ \ \ \ %%%
- ???preceds s ths
+ @{thm preceds_def}
\end{isabelle}
\noindent
@@ -432,8 +435,8 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{thm cs_holding_raw[where thread="th"]}\\
- @{thm cs_waiting_raw[where thread="th"]}
+ @{thm holding_raw_def[where thread="th"]}\\
+ @{thm waiting_raw_def[where thread="th"]}
\end{tabular}
\end{isabelle}
@@ -450,7 +453,7 @@
\end{isabelle}
\noindent
- Using @{term "holding"} and @{term waiting}, we can introduce \emph{Resource Allocation Graphs}
+ Using @{term "holding_raw"} and @{term waiting_raw}, we can introduce \emph{Resource Allocation Graphs}
(RAG), which represent the dependencies between threads and resources.
We represent RAGs as relations using pairs of the form
@@ -466,7 +469,7 @@
as the union of the sets of waiting and holding edges, namely
\begin{isabelle}\ \ \ \ \ %%%
- @{thm cs_RAG_raw}
+ @{thm RAG_raw_def}
\end{isabelle}
@@ -528,20 +531,20 @@
operation for relations, written ~@{term "trancl DUMMY"}. This gives
\begin{isabelle}\ \ \ \ \ %%%
- @{thm cs_dependants_def}
+ @{thm dependants_raw_def}
\end{isabelle}
- \noindent
- This definition needs to account for all threads that wait for a thread to
- release a resource. This means we need to include threads that transitively
- wait for a resource to be released (in the picture above this means the dependants
- of @{text "th\<^sub>0"} are @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which wait for resource @{text "cs\<^sub>1"},
- but also @{text "th\<^sub>3"},
- which cannot make any progress unless @{text "th\<^sub>2"} makes progress, which
- in turn needs to wait for @{text "th\<^sub>0"} to finish). If there is a circle of dependencies
- in a RAG, then clearly
- we have a deadlock. Therefore when a thread requests a resource,
- we must ensure that the resulting RAG is not circular. In practice, the
+ \noindent This definition needs to account for all threads that wait
+ for a thread to release a resource. This means we need to include
+ threads that transitively wait for a resource to be released (in the
+ picture above this means the dependants of @{text "th\<^sub>0"} are
+ @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which wait for
+ resource @{text "cs\<^sub>1"}, but also @{text "th\<^sub>3"}, which
+ cannot make any progress unless @{text "th\<^sub>2"} makes progress,
+ which in turn needs to wait for @{text "th\<^sub>0"} to finish). If
+ there is a circle of dependencies in a RAG, then clearly we have a
+ deadlock. Therefore when a thread requests a resource, we must
+ ensure that the resulting RAG is not circular. In practice, the
programmer has to ensure this.
@@ -699,7 +702,7 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@{thm readys_def}\\
- @{thm runing_def}
+ @{thm running_def}
\end{tabular}
\end{isabelle}
@@ -1001,7 +1004,7 @@
THENTHEN
- (here) %@ {thm [source] runing_inversion_4} @ {thm runing_inversion_4}
+ (here) %@ {thm [source] running_inversion_4} @ {thm running_inversion_4}
which explains what the @{term "th'"} looks like. Now, we have found the
@{term "th'"} which blocks @{term th}, we need to know more about it.
@@ -1015,7 +1018,7 @@
\begin{lemma}
- @{thm runing_cntP_cntV_inv}
+ @{thm running_cntP_cntV_inv}
\end{lemma}
\noindent
@@ -1024,7 +1027,7 @@
and @{const cntP} can be larger than @{term 1}.
\begin{lemma}\label{runninginversion}
- @{thm runing_inversion}
+ @{thm running_inversion}
\end{lemma}
explain tRAG
@@ -1107,7 +1110,7 @@
HERE??
%@ {thm[mode=IfThen] waiting_unique[of _ _ "cs1" "cs2"]}\\
%@ {thm[mode=IfThen] held_unique[of _ "th1" _ "th2"]}\\
- %@ {thm[mode=IfThen] runing_unique[of _ "th1" "th2"]}
+ %@ {thm[mode=IfThen] running_unique[of _ "th1" "th2"]}
\end{tabular}
\end{isabelle}
@@ -1241,7 +1244,7 @@
%\end{enumerate}
%The reason that only threads which already held some resoures
- %can be runing and block @{text "th"} is that if , otherwise, one thread
+ %can be running and block @{text "th"} is that if , otherwise, one thread
%does not hold any resource, it may never have its prioirty raised
%and will not get a chance to run. This fact is supported by
%lemma @{text "moment_blocked"}:
@@ -1296,8 +1299,8 @@
%\end{enumerate}
%The main theorem of this part is to characterizing the running thread during @{term "t"}
- %(@{text "runing_inversion_2"}):
- %@ {thm [display] runing_inversion_2}
+ %(@{text "running_inversion_2"}):
+ %@ {thm [display] running_inversion_2}
%According to this, if a thread is running, it is either @{term "th"} or was
%already live and held some resource
%at moment @{text "s"} (expressed by: @{text "cntV s th' < cntP s th'"}).
@@ -1824,4 +1827,4 @@
(*<*)
end
-(*>*)
\ No newline at end of file
+(*>*)
--- a/Max.thy Tue Jun 07 13:51:39 2016 +0100
+++ b/Max.thy Thu Jun 09 23:01:36 2016 +0100
@@ -75,4 +75,4 @@
qed
-end
\ No newline at end of file
+end
--- a/PIPBasics.thy Tue Jun 07 13:51:39 2016 +0100
+++ b/PIPBasics.thy Thu Jun 09 23:01:36 2016 +0100
@@ -3,15 +3,15 @@
begin
text {* (* ddd *)
+
Following the HOL convention of {\em definitional extension}, we have
- given a concise and miniature model of PIP. To assure ourselves of
- the correctness of this model, we are going to derive a series of
- expected properties out of it.
-
- This file contains the very basic properties, useful for self-assurance,
- as well as for deriving more advance properties concerning
- the correctness and implementation of PIP.
-*}
+ given a concise and miniature model of PIP. To assure ourselves of the
+ correctness of this model, we are going to derive a series of expected
+ properties out of it.
+
+ This file contains the very basic properties, useful for self-assurance,
+ as well as for deriving more advance properties concerning the correctness
+ and implementation of PIP. *}
section {* Generic auxiliary lemmas *}
@@ -135,9 +135,10 @@
by (drule_tac th_in_ne, unfold preced_def, auto intro: birth_time_lt)
text {*
- The follow lemma says if a resource is waited for, it must be held
- by someone else.
-*}
+
+ The following lemma says that if a resource is waited for, it must be held
+ by someone else. *}
+
lemma waiting_holding:
assumes "waiting (s::state) th cs"
obtains th' where "holding s th' cs"
@@ -150,33 +151,6 @@
from that[OF this] show ?thesis .
qed
-text {*
- The following four lemmas relate the @{term wq}
- and non-@{term wq} versions of @{term waiting}, @{term holding},
- @{term dependants} and @{term cp}.
-*}
-
-lemma waiting_eq: "waiting s th cs = waiting_raw (wq s) th cs"
- by (unfold s_waiting_def cs_waiting_raw wq_def, auto)
-
-lemma holding_eq: "holding (s::state) th cs = holding_raw (wq s) th cs"
- by (unfold s_holding_def wq_def cs_holding_raw, simp)
-
-lemma eq_dependants: "dependants_raw (wq s) = dependants s"
- by (simp add: s_dependants_abv wq_def)
-
-lemma cp_eq: "cp s th = cpreced (wq s) s th"
-unfolding cp_def wq_def
-apply(induct s rule: schs.induct)
-apply(simp add: Let_def cpreced_initial)
-apply(simp add: Let_def)
-apply(simp add: Let_def)
-apply(simp add: Let_def)
-apply(subst (2) schs.simps)
-apply(simp add: Let_def)
-apply(subst (2) schs.simps)
-apply(simp add: Let_def)
-done
text {*
The following @{text "children_RAG_alt_def"} relates
@@ -205,12 +179,12 @@
text {*
The following two lemmas show the inclusion relations
- among three key sets, namely @{term runing}, @{term readys}
+ among three key sets, namely @{term running}, @{term readys}
and @{term threads}.
*}
-lemma runing_ready:
- shows "runing s \<subseteq> readys s"
- unfolding runing_def readys_def
+lemma running_ready:
+ shows "running s \<subseteq> readys s"
+ unfolding running_def readys_def
by auto
lemma readys_threads:
@@ -224,8 +198,8 @@
In other words, a running thread must have got every
resource it has requested.
*}
-lemma runing_wqE:
- assumes "th \<in> runing s"
+lemma running_wqE:
+ assumes "th \<in> running s"
and "th \<in> set (wq s cs)"
obtains rest where "wq s cs = th#rest"
proof -
@@ -239,7 +213,7 @@
have "waiting s th cs"
by (unfold s_waiting_def, fold wq_def, auto)
with assms show False
- by (unfold runing_def readys_def, auto)
+ by (unfold running_def readys_def, auto)
qed
with eq_wq that show ?thesis by metis
qed
@@ -391,9 +365,6 @@
insert assms V, auto simp:cntV_def)
qed (insert assms, auto simp:cntV_def)
-lemma eq_RAG:
- "RAG_raw (wq s) = RAG s"
- by (unfold cs_RAG_raw s_RAG_def, auto)
text {*
The following three lemmas shows the shape
@@ -597,18 +568,22 @@
are in place.
*}
lemma cp_alt_def:
- "cp s th =
- Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
+ "cp s th = Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
proof -
- have "Max (the_preced s ` ({th} \<union> dependants_raw (wq s) th)) =
+ have "Max (the_preced s ` ({th} \<union> dependants s th)) =
Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})"
(is "Max (_ ` ?L) = Max (_ ` ?R)")
proof -
have "?L = ?R"
- by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_raw s_RAG_def subtree_def)
+ unfolding subtree_def
+ apply(auto)
+ apply (simp add: s_RAG_abv s_dependants_def wq_def)
+ by (simp add: rtrancl_eq_or_trancl s_RAG_abv s_dependants_def wq_def)
thus ?thesis by simp
qed
- thus ?thesis by (unfold cp_eq cpreced_def, fold the_preced_def, simp)
+ thus ?thesis
+ by (metis (no_types, lifting) cp_eq cpreced_def eq_dependants
+ f_image_eq the_preced_def)
qed
text {*
@@ -1060,8 +1035,8 @@
using assms unfolding is_p wq_def
by (auto simp:Let_def)
-lemma runing_th_s:
- shows "th \<in> runing s"
+lemma running_th_s:
+ shows "th \<in> running s"
proof -
from pip_e[unfolded is_p]
show ?thesis by (cases, simp)
@@ -1071,7 +1046,7 @@
shows "th \<notin> set (wq s cs)"
proof
assume otherwise: "th \<in> set (wq s cs)"
- from runing_wqE[OF runing_th_s this]
+ from running_wqE[OF running_th_s this]
obtain rest where eq_wq: "wq s cs = th#rest" by blast
with otherwise
have "holding s th cs"
@@ -1254,7 +1229,7 @@
from pip_e[unfolded is_exit]
show ?thesis
by (cases, unfold holdents_def s_holding_def, fold wq_def,
- auto elim!:runing_wqE)
+ auto elim!:running_wqE)
qed
lemma wq_threads_kept:
@@ -1350,8 +1325,8 @@
by (unfold is_p, simp)
lemma ready_th_s: "th \<in> readys s"
- using runing_th_s
- by (unfold runing_def, auto)
+ using running_th_s
+ by (unfold running_def, auto)
lemma live_th_s: "th \<in> threads s"
using readys_threads ready_th_s by auto
@@ -1474,7 +1449,7 @@
moreover then obtain cs where "n = Cs cs" by (unfold s_RAG_def, auto)
ultimately have "(Th th, Cs cs) \<in> RAG s" by simp
hence "th \<in> set (wq s cs)"
- by (unfold s_RAG_def, auto simp:cs_waiting_raw)
+ by (unfold s_RAG_def, auto simp: waiting_raw_def)
from wq_threads [OF this] show ?thesis .
qed
@@ -1482,8 +1457,8 @@
assumes "(Th th) \<in> Range (RAG s)"
shows "th \<in> threads s"
using assms
- by (unfold s_RAG_def cs_waiting_raw cs_holding_raw,
- auto intro:wq_threads)
+ unfolding s_RAG_def waiting_raw_def holding_raw_def
+using wq_threads by auto
lemma RAG_threads:
assumes "(Th th) \<in> Field (RAG s)"
@@ -1593,8 +1568,8 @@
shows "th' \<in> set rest"
using assms set_wq' by simp
-lemma runing_th_s:
- shows "th \<in> runing s"
+lemma running_th_s:
+ shows "th \<in> running s"
proof -
from pip_e[unfolded is_v]
show ?thesis by (cases, simp)
@@ -1619,10 +1594,10 @@
have "wq (e#s) c = wq s c" using False
by simp
hence "waiting s t c" using assms
- by (simp add: cs_waiting_raw waiting_eq)
+ by (simp add: waiting_raw_def waiting_eq)
hence "t \<notin> readys s" by (unfold readys_def, auto)
- hence "t \<notin> runing s" using runing_ready by auto
- with runing_th_s[folded otherwise] show ?thesis by auto
+ hence "t \<notin> running s" using running_ready by auto
+ with running_th_s[folded otherwise] show ?thesis by auto
qed
qed
@@ -1634,7 +1609,7 @@
have "wq (e#s) c = wq s c"
using assms(2) by auto
with assms(1) show ?thesis
- unfolding cs_waiting_raw waiting_eq by auto
+ unfolding waiting_raw_def waiting_eq by auto
qed
lemma holding_esI2:
@@ -1722,7 +1697,7 @@
fix x
assume "distinct x \<and> set x = set rest"
moreover have "t \<in> set rest"
- using assms(1) unfolding cs_waiting_raw waiting_eq wq_s_cs by auto
+ using assms(1) unfolding waiting_raw_def waiting_eq wq_s_cs by auto
ultimately show "t \<in> set x" by simp
qed
moreover have "t \<noteq> hd wq'"
@@ -1738,7 +1713,7 @@
proof(cases "c = cs")
case False
hence "wq (e#s) c = wq s c" by auto
- with assms have "waiting s t c" unfolding cs_waiting_raw waiting_eq by auto
+ with assms have "waiting s t c" unfolding waiting_raw_def waiting_eq by auto
from that(1)[OF False this] show ?thesis .
next
case True
@@ -1748,7 +1723,7 @@
moreover hence "t \<noteq> th" using assms neq_t_th by blast
moreover have "t \<in> set rest" by (simp add: `t \<in> set wq'` th'_in_inv)
ultimately have "waiting s t cs"
- by (metis cs_waiting_raw insert_iff list.sel(1) s_waiting_abv set_simps(2) wq_def wq_s_cs)
+ by (metis waiting_raw_def insert_iff list.sel(1) s_waiting_abv set_simps(2) wq_def wq_s_cs)
show ?thesis using that(2)
using True `t \<in> set wq'` `t \<noteq> taker` `waiting s t cs` eq_wq' by auto
qed
@@ -1845,7 +1820,7 @@
shows "waiting (e#s) t c"
proof -
have "c \<noteq> cs" using assms
- using rest_nil wq_s_cs unfolding cs_waiting_raw waiting_eq by auto
+ using rest_nil wq_s_cs unfolding waiting_raw_def waiting_eq by auto
from waiting_esI1[OF assms this]
show ?thesis .
qed
@@ -1856,7 +1831,7 @@
proof(cases "c = cs")
case False
hence "wq (e#s) c = wq s c" by auto
- with assms have "waiting s t c" unfolding cs_waiting_raw waiting_eq by auto
+ with assms have "waiting s t c" unfolding waiting_raw_def waiting_eq by auto
from that(1)[OF False this] show ?thesis .
next
case True
@@ -2077,7 +2052,7 @@
assumes "waiting s th' cs'"
shows "waiting (e#s) th' cs'"
using assms
- unfolding th_not_in_wq waiting_eq cs_waiting_raw
+ unfolding th_not_in_wq waiting_eq waiting_raw_def
by (metis append_is_Nil_conv butlast_snoc hd_append2 in_set_butlastD
list.distinct(1) split_list wq_es_cs wq_neq_simp)
@@ -2087,7 +2062,7 @@
proof(cases "cs' = cs")
case False
hence "wq (e#s) cs' = wq s cs'" by simp
- with assms show ?thesis unfolding cs_holding_raw holding_eq by auto
+ with assms show ?thesis unfolding holding_raw_def holding_eq by auto
next
case True
from assms[unfolded s_holding_def, folded wq_def]
@@ -2096,14 +2071,14 @@
hence "wq (e#s) cs' = th'#(rest@[th])"
by (simp add: True wq_es_cs)
thus ?thesis
- by (simp add: cs_holding_raw holding_eq)
+ by (simp add: holding_raw_def holding_eq)
qed
end
lemma (in valid_trace_p) th_not_waiting: "\<not> waiting s th c"
proof -
have "th \<in> readys s"
- using runing_ready runing_th_s by blast
+ using running_ready running_th_s by blast
thus ?thesis
by (unfold readys_def, auto)
qed
@@ -2119,7 +2094,7 @@
proof -
from wq_es_cs'
have "th \<in> set (wq (e#s) cs)" "th = hd (wq (e#s) cs)" by auto
- thus ?thesis unfolding cs_holding_raw holding_eq by blast
+ thus ?thesis unfolding holding_raw_def holding_eq by blast
qed
lemma RAG_edge: "(Cs cs, Th th) \<in> RAG (e#s)"
@@ -2144,7 +2119,7 @@
next
case False
have "holding s th' cs'" using assms
- using False unfolding cs_holding_raw holding_eq by auto
+ using False unfolding holding_raw_def holding_eq by auto
from that(1)[OF False this] show ?thesis .
qed
@@ -2214,7 +2189,7 @@
by (simp add: wq_es_cs wq_s_cs)
lemma waiting_es_th_cs: "waiting (e#s) th cs"
- using th_not_in_wq waiting_eq wq_es_cs' wq_s_cs unfolding cs_waiting_raw by auto
+ using th_not_in_wq waiting_eq wq_es_cs' wq_s_cs unfolding waiting_raw_def by auto
lemma RAG_edge: "(Th th, Cs cs) \<in> RAG (e#s)"
by (unfold s_RAG_def, fold waiting_eq, insert waiting_es_th_cs, auto)
@@ -2227,7 +2202,7 @@
case False
hence "wq (e#s) cs' = wq s cs'" by simp
with assms show ?thesis using that
- unfolding cs_holding_raw holding_eq by auto
+ unfolding holding_raw_def holding_eq by auto
next
case True
with assms show ?thesis
@@ -2250,7 +2225,7 @@
next
case False
hence "th' = th \<and> cs' = cs"
- by (metis assms cs_waiting_raw holder_def list.sel(1) rotate1.simps(2)
+ by (metis assms waiting_raw_def holder_def list.sel(1) rotate1.simps(2)
set_ConsD set_rotate1 waiting_eq wq_es_cs wq_es_cs' wq_neq_simp)
with that(2) show ?thesis by metis
qed
@@ -2361,8 +2336,8 @@
proof(induct rule:ind)
case Nil
show ?case
- by (auto simp: s_RAG_def cs_waiting_raw
- cs_holding_raw wq_def acyclic_def)
+ by (auto simp: s_RAG_def waiting_raw_def
+ holding_raw_def wq_def acyclic_def)
next
case (Cons s e)
interpret vt_e: valid_trace_e s e using Cons by simp
@@ -2794,8 +2769,8 @@
proof(induct rule:ind)
case Nil
show ?case
- by (auto simp: s_RAG_def cs_waiting_raw
- cs_holding_raw wq_def acyclic_def)
+ by (auto simp: s_RAG_def waiting_raw_def
+ holding_raw_def wq_def acyclic_def)
next
case (Cons s e)
interpret vt_e: valid_trace_e s e using Cons by simp
@@ -3084,7 +3059,8 @@
next
case False
from False and th_in have "Th th \<in> Domain (RAG s)"
- by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_raw Domain_def)
+ by (auto simp: readys_def s_waiting_def s_RAG_def wq_def waiting_raw_def
+ Domain_def)
from chain_building [rule_format, OF this]
show ?thesis by auto
qed
@@ -3115,13 +3091,13 @@
The following two lemmas shows there is at most one running thread
in the system.
*}
-lemma runing_unique:
- assumes runing_1: "th1 \<in> runing s"
- and runing_2: "th2 \<in> runing s"
+lemma running_unique:
+ assumes running_1: "th1 \<in> running s"
+ and running_2: "th2 \<in> running s"
shows "th1 = th2"
proof -
- from runing_1 and runing_2 have "cp s th1 = cp s th2"
- unfolding runing_def by auto
+ from running_1 and running_2 have "cp s th1 = cp s th2"
+ unfolding running_def by auto
from this[unfolded cp_alt_def]
have eq_max:
"Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th1)}) =
@@ -3152,7 +3128,7 @@
proof(cases rule:subtreeE)
case 1
hence "th1' = th1" by simp
- with runing_1 show ?thesis by (auto simp:runing_def readys_def)
+ with running_1 show ?thesis by (auto simp:running_def readys_def)
next
case 2
from this(2)
@@ -3167,7 +3143,7 @@
proof(cases rule:subtreeE)
case 1
hence "th2' = th2" by simp
- with runing_2 show ?thesis by (auto simp:runing_def readys_def)
+ with running_2 show ?thesis by (auto simp:running_def readys_def)
next
case 2
from this(2)
@@ -3203,8 +3179,8 @@
from tranclD[OF this]
obtain cs where "waiting s th1 cs"
by (unfold s_RAG_def, fold waiting_eq, auto)
- with runing_1 show False
- by (unfold runing_def readys_def, auto)
+ with running_1 show False
+ by (unfold running_def readys_def, auto)
qed
ultimately have "xs2 = xs1" by simp
from rpath_dest_eq[OF rp1 rp2[unfolded this]]
@@ -3219,8 +3195,8 @@
from tranclD[OF this]
obtain cs where "waiting s th2 cs"
by (unfold s_RAG_def, fold waiting_eq, auto)
- with runing_2 show False
- by (unfold runing_def readys_def, auto)
+ with running_2 show False
+ by (unfold running_def readys_def, auto)
qed
ultimately have "xs2 = xs1" by simp
from rpath_dest_eq[OF rp1 rp2[unfolded this]]
@@ -3228,15 +3204,15 @@
qed
qed
-lemma card_runing: "card (runing s) \<le> 1"
-proof(cases "runing s = {}")
+lemma card_running: "card (running s) \<le> 1"
+proof(cases "running s = {}")
case True
thus ?thesis by auto
next
case False
- then obtain th where [simp]: "th \<in> runing s" by auto
- from runing_unique[OF this]
- have "runing s = {th}" by auto
+ then obtain th where [simp]: "th \<in> running s" by auto
+ from running_unique[OF this]
+ have "running s = {th}" by auto
thus ?thesis by auto
qed
@@ -3635,7 +3611,7 @@
case (thread_P)
moreover have "(Cs cs, Th th) \<in> RAG s"
using otherwise th_not_in_wq
- unfolding cs_holding_raw holding_eq by auto
+ unfolding holding_raw_def holding_eq by auto
ultimately show ?thesis by auto
qed
qed
@@ -3819,15 +3795,15 @@
by (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto)
lemma th_ready_s [simp]: "th \<in> readys s"
- using runing_th_s
- by (unfold runing_def readys_def, auto)
+ using running_th_s
+ by (unfold running_def readys_def, auto)
lemma th_live_s [simp]: "th \<in> threads s"
using th_ready_s by (unfold readys_def, auto)
lemma th_ready_es [simp]: "th \<in> readys (e#s)"
- using runing_th_s neq_t_th
- by (unfold is_v runing_def readys_def, auto)
+ using running_th_s neq_t_th
+ by (unfold is_v running_def readys_def, auto)
lemma th_live_es [simp]: "th \<in> threads (e#s)"
using th_ready_es by (unfold readys_def, auto)
@@ -3858,7 +3834,7 @@
"\<not> waiting s th c"
proof -
have "th \<in> readys s"
- using runing_ready runing_th_s by blast
+ using running_ready running_th_s by blast
thus ?thesis
by (unfold readys_def, auto)
qed
@@ -4478,14 +4454,14 @@
proof -
from pip_e[unfolded is_exit]
show ?thesis
- by (cases, unfold runing_def readys_def, simp)
+ by (cases, unfold running_def readys_def, simp)
qed
lemma th_ready_s [simp]: "th \<in> readys s"
proof -
from pip_e[unfolded is_exit]
show ?thesis
- by (cases, unfold runing_def, simp)
+ by (cases, unfold running_def, simp)
qed
lemma th_not_live_es [simp]: "th \<notin> threads (e#s)"
@@ -4625,14 +4601,14 @@
proof -
from pip_e[unfolded is_set]
show ?thesis
- by (cases, unfold runing_def readys_def, simp)
+ by (cases, unfold running_def readys_def, simp)
qed
lemma th_ready_s [simp]: "th \<in> readys s"
proof -
from pip_e[unfolded is_set]
show ?thesis
- by (cases, unfold runing_def, simp)
+ by (cases, unfold running_def, simp)
qed
lemma th_not_live_es [simp]: "th \<in> threads (e#s)"
@@ -5111,7 +5087,7 @@
assumes "PIP s e"
and "actor e = th"
and "\<not> isCreate e"
- shows "th \<in> runing s"
+ shows "th \<in> running s"
using assms
by (cases, auto)
@@ -5127,7 +5103,7 @@
assume "(a, Th th) \<in> RAG s"
with assms[unfolded holdents_test]
show False
- by (cases a, auto simp:cs_RAG_raw s_RAG_abv)
+ by (cases a, auto simp:RAG_raw_def s_RAG_abv)
qed
qed
@@ -5142,7 +5118,7 @@
assume "(Th th, b) \<in> RAG s"
with assms[unfolded readys_def s_waiting_def]
show False
- by (cases b, auto simp:cs_RAG_raw s_RAG_abv cs_waiting_raw)
+ by (cases b, auto simp: RAG_raw_def s_RAG_abv waiting_raw_def)
qed
qed
--- a/PIPDefs.thy Tue Jun 07 13:51:39 2016 +0100
+++ b/PIPDefs.thy Thu Jun 09 23:01:36 2016 +0100
@@ -7,29 +7,29 @@
chapter {* Definitions *}
text {*
- In this section, the formal model of Priority Inheritance Protocol (PIP) is presented.
- The model is based on Paulson's inductive protocol verification method, where
- the state of the system is modelled as a list of events (trace) happened so far with the
- latest event put at the head.
-*}
+
+ In this section, the formal model of Priority Inheritance Protocol (PIP)
+ is presented. The model is based on Paulson's inductive protocol
+ verification method, where the state of the system is modelled as a list
+ of events (trace) happened so far with the latest event put at the head.
+ *}
text {*
- To define events, the identifiers of {\em threads},
- {\em priority} and {\em critical resources } (abbreviated as @{text "cs"})
- need to be represented. All three are represetned using standard
- Isabelle/HOL type @{typ "nat"}:
-*}
+
+ To define events, the identifiers of {\em threads}, {\em priority} and
+ {\em critical resources } (abbreviated as @{text "cs"}) need to be
+ represented. All three are represetned using standard Isabelle/HOL type
+ @{typ "nat"}: *}
type_synonym thread = nat -- {* Type for thread identifiers. *}
type_synonym priority = nat -- {* Type for priorities. *}
type_synonym cs = nat -- {* Type for critical sections (or critical resources). *}
text {*
- \noindent
- The abstraction of Priority Inheritance Protocol (PIP) is set at the system call level.
- Every system call is represented as an event. The format of events is defined
- defined as follows:
- *}
+
+ \noindent The abstraction of Priority Inheritance Protocol (PIP) is set at
+ the system call level. Every system call is represented as an event. The
+ format of events is defined defined as follows: *}
datatype event =
Create thread priority -- {* Thread @{text "thread"} is created with priority @{text "priority"}. *}
@@ -61,173 +61,166 @@
"isV _ = False"
text {*
- As mentioned earlier, in Paulson's inductive method, the states of system are represented as lists
- of events, which is defined by the following type @{text "state"}: *}
+
+ As mentioned earlier, in Paulson's inductive method, the states of system
+ are represented as lists of events, which is defined by the following type
+ @{text "state"}: *}
type_synonym state = "event list"
-text {*
- Resource Allocation Graphs (RAG for short) are used extensively in our formal analysis.
- The following type @{text "node"} is used to represent the two types of nodes in RAGs. *}
-datatype node =
- Th "thread" -- {* Node for a thread. *}
-| Cs "cs" -- {* Node for a critical resource. *}
+text {*
-text {*
- The function @{text "threads"} is used to calculate the set of live threads (@{text "threads s"})
- in state @{text "s"}. *}
+ The function @{text "threads"} is used to calculate the set of live
+ threads (@{text "threads s"}) in state @{text "s"}. *}
fun threads :: "state \<Rightarrow> thread set"
where
-- {* At the start of the system, the set of threads is empty: *}
"threads [] = {}" |
-- {* New thread is added to the @{text "threads"}: *}
- "threads (Create thread prio#s) = {thread} \<union> threads s" |
+ "threads (Create th prio#s) = {th} \<union> threads s" |
-- {* Finished thread is removed: *}
- "threads (Exit thread # s) = (threads s) - {thread}" |
+ "threads (Exit th # s) = (threads s) - {th}" |
-- {* Other kind of events does not affect the value of @{text "threads"}: *}
- "threads (e#s) = threads s"
+ "threads (e # s) = threads s"
text {*
- \noindent The function @{text "threads"} defined above is one of the
- so called {\em observation function}s which forms the very basis of
- Paulson's inductive protocol verification method. Each observation
- function {\em observes} one particular aspect (or attribute) of the
- system. For example, the attribute observed by @{text "threads s"}
- is the set of threads living in state @{text "s"}. The protocol
- being modelled The decision made the protocol being modelled is
- based on the {\em observation}s returned by {\em observation
- function}s. Since {\observation function}s forms the very basis on
- which Paulson's inductive method is based, there will be a lot of
+ \noindent The function @{text "threads"} is one of the {\em observation
+ function}s which forms the very basis of Paulson's inductive protocol
+ verification method. Each observation function {\em observes} one
+ particular aspect (or attribute) of the system. For example, the attribute
+ observed by @{text "threads s"} is the set of threads living in state
+ @{text "s"}. The protocol being modelled The decision made the protocol
+ being modelled is based on the {\em observation}s returned by {\em
+ observation function}s. Since {\observation function}s forms the very
+ basis on which Paulson's inductive method is based, there will be a lot of
such observation functions introduced in the following. In fact, any
function which takes event list as argument is a {\em observation
- function}. *}
+ function}. *}
text {*
\noindent Observation @{text "priority th s"} is the {\em original
- priority} of thread @{text "th"} in state @{text "s"}. The {\em
- original priority} is the priority assigned to a thread when it is
- created or when it is reset by system call (represented by event
- @{text "Set thread priority"}). *}
+ priority} of thread @{text "th"} in state @{text "s"}. The {\em original
+ priority} is the priority assigned to a thread when it is created or when
+ it is reset by system call (represented by event @{text "Set thread
+ priority"}). *}
fun priority :: "thread \<Rightarrow> state \<Rightarrow> priority"
where
-- {* @{text "0"} is assigned to threads which have never been created: *}
- "priority thread [] = 0" |
- "priority thread (Create thread' prio#s) =
- (if thread' = thread then prio else priority thread s)" |
- "priority thread (Set thread' prio#s) =
- (if thread' = thread then prio else priority thread s)" |
- "priority thread (e#s) = priority thread s"
+ "priority th [] = 0" |
+ "priority th (Create th' prio # s) =
+ (if th' = th then prio else priority th s)" |
+ "priority th (Set th' prio # s) =
+ (if th' = th then prio else priority th s)" |
+ "priority th (e # s) = priority th s"
text {*
- \noindent Observation @{text "last_set th s"} is the last time when
- the priority of thread @{text "th"} is set, observed from state
- @{text "s"}. The time in the system is measured by the number of
- events happened so far since the very beginning. *}
+ \noindent Observation @{text "last_set th s"} is the last time when the
+ priority of thread @{text "th"} is set, observed from state @{text "s"}.
+ The time in the system is measured by the number of events happened so far
+ since the very beginning. *}
fun last_set :: "thread \<Rightarrow> state \<Rightarrow> nat"
where
- "last_set thread [] = 0" |
- "last_set thread ((Create thread' prio)#s) =
- (if (thread = thread') then length s else last_set thread s)" |
- "last_set thread ((Set thread' prio)#s) =
- (if (thread = thread') then length s else last_set thread s)" |
- "last_set thread (_#s) = last_set thread s"
+ "last_set th [] = 0" |
+ "last_set th ((Create th' prio) # s) =
+ (if (th = th') then length s else last_set th s)" |
+ "last_set th ((Set th' prio) # s) =
+ (if (th = th') then length s else last_set th s)" |
+ "last_set th (_ # s) = last_set th s"
text {*
- \noindent The {\em precedence} is a notion derived from {\em
- priority}, where the {\em precedence} of a thread is the combination
- of its {\em original priority} and {\em time} the priority is set.
- The intention is to discriminate threads with the same priority by
- giving threads whose priority is assigned earlier higher
- precedences, becasue such threads are more urgent to finish. This
- explains the following definition: *}
+ \noindent The {\em precedence} is a notion derived from {\em priority},
+ where the {\em precedence} of a thread is the combination of its {\em
+ original priority} and the {\em time} the priority was set. The intention
+ is to discriminate threads with the same priority by giving threads whose
+ priority is assigned earlier higher precedences, because such threads are
+ assumed more urgent to finish. *}
definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
- where "preced thread s \<equiv> Prc (priority thread s) (last_set thread s)"
+ where "preced th s \<equiv> Prc (priority th s) (last_set th s)"
+definition preceds :: "thread set \<Rightarrow> state \<Rightarrow> precedence set"
+ where "preceds ths s \<equiv> {preced th s | th. th \<in> ths}"
text {*
- \noindent A number of important notions in PIP are represented as
- the following functions, defined in terms of the waiting queues of
- the system, where the waiting queues , as a whole, is represented by
- the @{text "wq"} argument of every notion function. The @{text
- "wq"} argument is itself a functions which maps every critical
- resource @{text "cs"} to the list of threads which are holding or
- waiting for it. The thread at the head of this list is designated
- as the thread which is current holding the resrouce, which is
- slightly different from tradition where all threads in the waiting
- queue are considered as waiting for the resource. *}
+ \noindent A number of important notions in PIP are represented as the
+ following functions, defined in terms of the waiting queues of the system,
+ where the waiting queues, as a whole, is represented by the @{text "wq"}
+ argument of every notion function. The @{text "wq"} argument is itself a
+ functions which maps every critical resource @{text "cs"} to the list of
+ threads which are holding or waiting for it. The thread at the head of
+ this list is designated as the thread which is current holding the
+ resource, which is slightly different from tradition where all threads in
+ the waiting queue are considered as waiting for the resource. *}
-(*
-consts
- holding :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"
- waiting :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"
- RAG :: "'b \<Rightarrow> (node \<times> node) set"
- dependants :: "'b \<Rightarrow> thread \<Rightarrow> thread set"
-*)
+text {*
--- {*
- \begin{minipage}{0.9\textwidth}
- This meaning of @{text "wq"} is reflected in the following definition of
- @{text "holding wq th cs"}, where @{text "holding wq th cs"} means thread
- @{text "th"} is holding the critical resource @{text "cs"}. This decision
- is based on @{text "wq"}.
- \end{minipage}
- *}
+ \begin{minipage}{0.9\textwidth} This meaning of @{text "wq"} is reflected
+ in the following definition of @{text "holding wq th cs"}, where @{text
+ "holding wq th cs"} means thread @{text "th"} is holding the critical
+ resource @{text "cs"}. This decision is based on @{text "wq"}.
+ \end{minipage} *}
definition
- cs_holding_raw:
"holding_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread = hd (wq cs))"
+text {*
+
+ \begin{minipage}{0.9\textwidth} In accordance with the definition of
+ @{text "holding wq th cs"}, a thread @{text "th"} is considered waiting
+ for @{text "cs"} if it is in the {\em waiting queue} of critical resource
+ @{text "cs"}, but not at the head. This is reflected in the definition of
+ @{text "waiting wq th cs"} as follows: \end{minipage} *}
definition
- -- {*
- \begin{minipage}{0.9\textwidth}
- In accordance with the definition of @{text "holding wq th cs"}, a thread
- @{text "th"} is considered waiting for @{text "cs"} if it is in the {\em
- waiting queue} of critical resource @{text "cs"}, but not at the head.
- This is reflected in the definition of @{text "waiting wq th cs"} as
- follows:
- \end{minipage}
- *}
+ "waiting_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"
+
+text {*
+
+ Resource Allocation Graphs (RAG for short) are used extensively in our
+ formal analysis. The following type @{text "node"} is used to represent
+ the two types of nodes in RAGs. *}
- cs_waiting_raw:
- "waiting_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"
+datatype node =
+ Th "thread" -- {* Node for a thread. *}
+| Cs "cs" -- {* Node for a critical resource. *}
+
+
+text {*
+
+ \begin{minipage}{0.9\textwidth} @{text "RAG wq"} generates RAG (a binary
+ relations on @{text "node"}) out of waiting queues of the system
+ (represented by the @{text "wq"} argument): \end{minipage} *}
definition
- -- {*
- \begin{minipage}{0.9\textwidth}
- @{text "RAG wq"} generates RAG (a binary relations on @{text "node"}) out
- of waiting queues of the system (represented by the @{text "wq"}
- argument): \end{minipage}
- *}
+ RAG_raw :: "(cs \<Rightarrow> thread list) => (node * node) set"
+where
+ "RAG_raw wq \<equiv>
+ {(Th th, Cs cs) | th cs. waiting_raw wq th cs} \<union>
+ {(Cs cs, Th th) | cs th. holding_raw wq th cs}"
- cs_RAG_raw:
- "RAG_raw (wq::cs \<Rightarrow> thread list) \<equiv>
- {(Th th, Cs cs) | th cs. waiting_raw wq th cs} \<union> {(Cs cs, Th th) | cs th. holding_raw wq th cs}"
+text {*
+
+ \begin{minipage}{0.9\textwidth} The following @{text "dependants wq th"}
+ represents the set of threads which are RAGing on thread @{text "th"} in
+ Resource Allocation Graph @{text "RAG wq"}. Here, "RAGing" means waiting
+ directly or indirectly on the critical resource. \end{minipage} *}
definition
- -- {*
- \begin{minipage}{0.9\textwidth}
- The following @{text "dependants wq th"} represents the set of threads
- which are RAGing on thread @{text "th"} in Resource Allocation Graph
- @{text "RAG wq"}. Here, "RAGing" means waiting directly or indirectly on
- the critical resource.
- \end{minipage}
- *}
-
- cs_dependants_def:
- "dependants_raw (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (RAG_raw wq)^+}"
+ dependants_raw :: "(cs \<Rightarrow> thread list) \<Rightarrow> thread \<Rightarrow> thread set"
+where
+ "dependants_raw wq th \<equiv> {th' . (Th th', Th th) \<in> (RAG_raw wq)^+}"
text {*
+
\noindent The following @{text "cpreced s th"} gives the {\em current
precedence} of thread @{text "th"} under state @{text "s"}. The definition
of @{text "cpreced"} reflects the basic idea of Priority Inheritance that
@@ -235,39 +228,35 @@
the maximum of all its dependants, i.e. the threads which are waiting
directly or indirectly waiting for some resources from it. If no such
thread exits, @{text "th"}'s {\em current precedence} equals its original
- precedence, i.e. @{text "preced th s"}.
-*}
+ precedence, i.e. @{text "preced th s"}. *}
-definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"
- where "cpreced wq s = (\<lambda>th. Max ((\<lambda>th'. preced th' s) ` ({th} \<union> dependants_raw wq th)))"
+definition
+ cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"
+ where
+ "cpreced wq s th = Max ((\<lambda>th'. preced th' s) ` ({th} \<union> dependants_raw wq th))"
text {*
+
Notice that the current precedence (@{text "cpreced"}) of one thread
- @{text "th"} can be boosted (becoming larger than its own precedence) by
- those threads in the @{text "dependants wq th"}-set. If one thread get
- boosted, we say it inherits the priority (or, more precisely, the
- precedence) of its dependants. This is how the word "Inheritance" in
- Priority Inheritance Protocol comes.
-*}
+ @{text "th"} can be boosted (increased) by those threads in the @{text
+ "dependants wq th"}-set. If one thread gets boosted, we say it inherits
+ the priority (or, more precisely, the precedence) of its dependants. This
+ is whrere the word "Inheritance" in Priority Inheritance Protocol comes
+ from. *}
-(*<*)
-lemma
- cpreced_def2:
- "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants_raw wq th})"
- unfolding cpreced_def image_def
+lemma cpreced_def2:
+ "cpreced wq s th \<equiv> Max ({preced th s} \<union> preceds (dependants_raw wq th) s)"
+ unfolding cpreced_def image_def preceds_def
apply(rule eq_reflection)
apply(rule_tac f="Max" in arg_cong)
by (auto)
-(*>*)
-
text {*
\noindent Assuming @{text "qs"} be the waiting queue of a critical
resource, the following abbreviation "release qs" is the waiting queue
after the thread holding the resource (which is thread at the head of
- @{text "qs"}) released the resource:
-*}
+ @{text "qs"}) released the resource: *}
abbreviation
"release qs \<equiv> case qs of
@@ -275,6 +264,7 @@
| (_#qs') => (SOME q. distinct q \<and> set q = set qs')"
text {*
+
\noindent It can be seen from the definition that the thread at the head
of @{text "qs"} is removed from the return value, and the value @{term
"q"} is an reordering of @{text "qs'"}, the tail of @{text "qs"}. Through
@@ -284,22 +274,22 @@
little better different from common sense that the thread who comes the
earliest should take over. The intention of this definition is to show
that the choice of which thread to take over the release resource does not
- affect the correctness of the PIP protocol.
-*}
+ affect the correctness of the PIP protocol. *}
text {*
+
The data structure used by the operating system for scheduling is referred
to as {\em schedule state}. It is represented as a record consisting of a
function assigning waiting queue to resources (to be used as the @{text
"wq"} argument in @{text "holding"}, @{text "waiting"} and @{text "RAG"},
- etc) and a function assigning precedence to threads:
- *}
+ etc) and a function assigning precedence to threads: *}
record schedule_state =
wq_fun :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *}
cprec_fun :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *}
text {*
+
\noindent The following two abbreviations (@{text "all_unlocked"} and
@{text "initial_cprec"}) are used to set the initial values of the @{text
"wq_fun"} @{text "cprec_fun"} fields respectively of the @{text
@@ -315,27 +305,28 @@
"all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)"
-text {* \noindent
- The initial current precedence for a thread can be anything, because there is no thread then.
- We simply assume every thread has precedence @{text "Prc 0 0"}.
- *}
+text {*
+
+ \noindent The initial current precedence for a thread can be anything,
+ because there is no thread then. We simply assume every thread has
+ precedence @{text "Prc 0 0"}. *}
abbreviation
"initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0"
-text {* \noindent
- The following function @{text "schs"} is used to calculate the system's schedule state @{text "schs s"}
- out of the current system state @{text "s"}. It is the central function to model Priority Inheritance:
- *}
-fun schs :: "state \<Rightarrow> schedule_state"
- where
- -- {*
+text {*
+
+ \noindent The following function @{text "schs"} is used to calculate the
+ system's schedule state @{text "schs s"} out of the current system state
+ @{text "s"}. It is the central function to model Priority Inheritance.
+
\begin{minipage}{0.9\textwidth}
- Setting the initial value of the @{text "schedule_state"} record (see the explanations above).
+ Setting the initial value of the @{text "schedule_state"} record
+ (see the explanations above).
\end{minipage}
*}
- "schs [] = (| wq_fun = all_unlocked, cprec_fun = initial_cprec |)" |
+
-- {*
\begin{minipage}{0.9\textwidth}
@@ -368,7 +359,11 @@
by the happening event) or @{text "new_wq"} (if the value of @{text "wq_fun"} is changed).
\end{minipage}
*}
- "schs (Create th prio # s) =
+
+fun schs :: "state \<Rightarrow> schedule_state"
+ where
+ "schs [] = (| wq_fun = all_unlocked, cprec_fun = initial_cprec |)"
+| "schs (Create th prio # s) =
(let wq = wq_fun (schs s) in
(|wq_fun = wq, cprec_fun = cpreced wq (Create th prio # s)|))"
| "schs (Exit th # s) =
@@ -394,50 +389,34 @@
lemma cpreced_initial:
"cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"
+apply(rule ext)
apply(simp add: cpreced_def)
-apply(simp add: cs_dependants_def cs_RAG_raw cs_waiting_raw cs_holding_raw)
+apply(simp add: dependants_raw_def RAG_raw_def waiting_raw_def holding_raw_def)
apply(simp add: preced_def)
done
-lemma sch_old_def:
- "schs (e#s) = (let ps = schs s in
- let pwq = wq_fun ps in
- let nwq = case e of
- P th cs \<Rightarrow> pwq(cs:=(pwq cs @ [th])) |
- V th cs \<Rightarrow> let nq = case (pwq cs) of
- [] \<Rightarrow> [] |
- (_#qs) \<Rightarrow> (SOME q. distinct q \<and> set q = set qs)
- in pwq(cs:=nq) |
- _ \<Rightarrow> pwq
- in let ncp = cpreced nwq (e#s) in
- \<lparr>wq_fun = nwq, cprec_fun = ncp\<rparr>
- )"
-apply(cases e)
-apply(simp_all)
-done
+text {*
+ \noindent The following @{text "wq"} is a shorthand for @{text "wq_fun"}.
+ *}
-text {*
- \noindent
- The following @{text "wq"} is a shorthand for @{text "wq_fun"}.
- *}
definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list"
where "wq s = wq_fun (schs s)"
-text {* \noindent
- The following @{text "cp"} is a shorthand for @{text "cprec_fun"}.
- *}
+text {*
+
+ \noindent The following @{text "cp"} is a shorthand for @{text
+ "cprec_fun"}. *}
+
definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"
where "cp s \<equiv> cprec_fun (schs s)"
-text {* \noindent
- Functions @{text "holding"}, @{text "waiting"}, @{text "RAG"} and
- @{text "dependants"} still have the
- same meaning, but redefined so that they no longer RAG on the
- fictitious {\em waiting queue function}
- @{text "wq"}, but on system state @{text "s"}.
- *}
+text {*
+ \noindent Functions @{text "holding"}, @{text "waiting"}, @{text "RAG"}
+ and @{text "dependants"} still have the same meaning, but redefined so
+ that they no longer RAG on the fictitious {\em waiting queue function}
+ @{text "wq"}, but on system state @{text "s"}. *}
definition
s_holding_abv:
@@ -455,56 +434,93 @@
s_dependants_abv:
"dependants (s::state) \<equiv> dependants_raw (wq_fun (schs s))"
+text {*
+
+ The following four lemmas relate the @{term wq} and non-@{term wq}
+ versions of @{term waiting}, @{term holding}, @{term dependants} and
+ @{term cp}. *}
+
+lemma waiting_eq:
+ shows "waiting s th cs = waiting_raw (wq s) th cs"
+ by (simp add: s_waiting_abv wq_def)
+
+lemma holding_eq:
+ shows "holding s th cs = holding_raw (wq s) th cs"
+ by (simp add: s_holding_abv wq_def)
+
+lemma eq_dependants:
+ shows "dependants_raw (wq s) = dependants s"
+ by (simp add: s_dependants_abv wq_def)
+
+lemma cp_eq:
+ shows "cp s th = cpreced (wq s) s th"
+unfolding cp_def wq_def
+apply(induct s rule: schs.induct)
+apply(simp add: Let_def cpreced_initial)
+apply(simp add: Let_def)
+apply(simp add: Let_def)
+apply(simp add: Let_def)
+apply(subst (2) schs.simps)
+apply(simp add: Let_def)
+apply(subst (2) schs.simps)
+apply(simp add: Let_def)
+done
text {*
- The following lemma can be proved easily, and the meaning is obvious.
- *}
+
+ The following lemma can be proved easily, and the meaning is obvious. *}
lemma
s_holding_def:
"holding (s::state) th cs \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th = hd (wq_fun (schs s) cs))"
- by (auto simp:s_holding_abv wq_def cs_holding_raw)
+ by (auto simp:s_holding_abv wq_def holding_raw_def)
lemma s_waiting_def:
"waiting (s::state) th cs \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th \<noteq> hd (wq_fun (schs s) cs))"
- by (auto simp:s_waiting_abv wq_def cs_waiting_raw)
+ by (auto simp:s_waiting_abv wq_def waiting_raw_def)
lemma s_RAG_def:
"RAG (s::state) =
- {(Th th, Cs cs) | th cs. waiting_raw (wq s) th cs} \<union> {(Cs cs, Th th) | cs th. holding_raw (wq s) th cs}"
- by (auto simp:s_RAG_abv wq_def cs_RAG_raw)
+ {(Th th, Cs cs) | th cs. waiting_raw (wq s) th cs} \<union>
+ {(Cs cs, Th th) | cs th. holding_raw (wq s) th cs}"
+ by (auto simp:s_RAG_abv wq_def RAG_raw_def)
-lemma
- s_dependants_def:
- "dependants (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (RAG_raw (wq s))^+}"
- by (auto simp:s_dependants_abv wq_def cs_dependants_def)
+lemma eq_RAG:
+ "RAG_raw (wq s) = RAG s"
+ by (unfold RAG_raw_def s_RAG_def, auto)
+
+
+lemma s_dependants_def:
+ shows "dependants (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (RAG s)^+}"
+using dependants_raw_def eq_RAG s_dependants_abv wq_def by auto
text {*
+
The following function @{text "readys"} calculates the set of ready
threads. A thread is {\em ready} for running if it is a live thread and it
- is not waiting for any critical resource.
- *}
+ is not waiting for any critical resource. *}
definition readys :: "state \<Rightarrow> thread set"
where "readys s \<equiv> {th . th \<in> threads s \<and> (\<forall> cs. \<not> waiting s th cs)}"
text {*
- \noindent The following function @{text "runing"} calculates the set of
- running thread, which is the ready thread with the highest precedence.
- *}
+
+ \noindent The following function @{text "running"} calculates the set of
+ running thread, which is the ready thread with the highest precedence. *}
-definition runing :: "state \<Rightarrow> thread set"
- where "runing s \<equiv> {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"
+definition running :: "state \<Rightarrow> thread set"
+ where "running s \<equiv> {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"
text {*
+
\noindent Notice that the definition of @{text "running"} reflects the
preemptive scheduling strategy, because, if the @{text "running"}-thread
- (the one in @{text "runing"} set) lowered its precedence by resetting its
+ (the one in @{text "running"} set) lowered its precedence by resetting its
own priority to a lower one, it will lose its status of being the max in
- @{text "ready"}-set and be superseded.
-*}
+ @{text "ready"}-set and be superseded. *}
text {*
+
\noindent The following function @{text "holdents s th"} returns the set
of resources held by thread @{text "th"} in state @{text "s"}. *}
@@ -520,15 +536,18 @@
unfolding wq_def
by (simp)
-text {* \noindent
- According to the convention of Paulson's inductive method,
- the decision made by a protocol that event @{text "e"} is eligible to happen next under state @{text "s"}
- is expressed as @{text "step s e"}. The predicate @{text "step"} is inductively defined as
- follows (notice how the decision is based on the {\em observation function}s
- defined above, and also notice how a complicated protocol is modeled by a few simple
- observations, and how such a kind of simplicity gives rise to improved trust on
- faithfulness):
- *}
+text {*
+
+ \noindent According to the convention of Paulson's inductive method, the
+ decision made by a protocol that event @{text "e"} is eligible to happen
+ next under state @{text "s"} is expressed as @{text "step s e"}. The
+ predicate @{text "step"} is inductively defined as follows (notice how the
+ decision is based on the {\em observation function}s defined above, and
+ also notice how a complicated protocol is modeled by a few simple
+ observations, and how such a kind of simplicity gives rise to improved
+ trust on faithfulness): *}
+
+
inductive step :: "state \<Rightarrow> event \<Rightarrow> bool"
where
-- {*
@@ -538,7 +557,7 @@
-- {*
A thread can exit if it no longer hold any resource:
*}
- thread_exit: "\<lbrakk>thread \<in> runing s; holdents s thread = {}\<rbrakk> \<Longrightarrow> step s (Exit thread)" |
+ thread_exit: "\<lbrakk>thread \<in> running s; holdents s thread = {}\<rbrakk> \<Longrightarrow> step s (Exit thread)" |
-- {*
\begin{minipage}{0.9\textwidth}
A thread can request for an critical resource @{text "cs"}, if it is running and
@@ -547,7 +566,7 @@
carefully programmed so that deadlock can not happen:
\end{minipage}
*}
- thread_P: "\<lbrakk>thread \<in> runing s; (Cs cs, Th thread) \<notin> (RAG s)^+\<rbrakk> \<Longrightarrow>
+ thread_P: "\<lbrakk>thread \<in> running s; (Cs cs, Th thread) \<notin> (RAG s)^+\<rbrakk> \<Longrightarrow>
step s (P thread cs)" |
-- {*
\begin{minipage}{0.9\textwidth}
@@ -555,7 +574,7 @@
if it is running and holding that resource:
\end{minipage}
*}
- thread_V: "\<lbrakk>thread \<in> runing s; holding s thread cs\<rbrakk> \<Longrightarrow> step s (V thread cs)" |
+ thread_V: "\<lbrakk>thread \<in> running s; holding s thread cs\<rbrakk> \<Longrightarrow> step s (V thread cs)" |
-- {*
\begin{minipage}{0.9\textwidth}
A thread can adjust its own priority as long as it is current running.
@@ -564,24 +583,26 @@
function,
\end{minipage}
*}
- thread_set: "\<lbrakk>thread \<in> runing s\<rbrakk> \<Longrightarrow> step s (Set thread prio)"
+ thread_set: "\<lbrakk>thread \<in> running s\<rbrakk> \<Longrightarrow> step s (Set thread prio)"
text {*
- In Paulson's inductive method, every protocol is defined by such a @{text "step"}
- predicate. For instance, the predicate @{text "step"} given above
- defines the PIP protocol. So, it can also be called "PIP".
-*}
+
+ In Paulson's inductive method, every protocol is defined by such a @{text
+ "step"} predicate. For instance, the predicate @{text "step"} given above
+ defines the PIP protocol. So, it can also be called "PIP". *}
abbreviation
"PIP \<equiv> step"
-text {* \noindent
- For any protocol defined by a @{text "step"} predicate,
- the fact that @{text "s"} is a legal state in
- the protocol is expressed as: @{text "vt step s"}, where
- the predicate @{text "vt"} can be defined as the following:
- *}
+text {*
+
+ \noindent For any protocol defined by a @{text "step"} predicate, the fact
+ that @{text "s"} is a legal state in the protocol is expressed as: @{text
+ "vt step s"}, where the predicate @{text "vt"} can be defined as the
+ following: *}
+
+
inductive vt :: "state \<Rightarrow> bool"
where
-- {* Empty list @{text "[]"} is a legal state in any protocol:*}
@@ -596,15 +617,16 @@
*}
vt_cons[intro]: "\<lbrakk>vt s; step s e\<rbrakk> \<Longrightarrow> vt (e#s)"
-text {* \noindent
- It is easy to see that the definition of @{text "vt"} is generic. It can be applied to
- any specific protocol specified by a @{text "step"}-predicate to get the set of
- legal states of that particular protocol.
- *}
+text {*
+
+ \noindent It is easy to see that the definition of @{text "vt"} is
+ generic. It can be applied to any specific protocol specified by a @{text
+ "step"}-predicate to get the set of legal states of that particular
+ protocol. *}
text {*
- The following are two very basic properties of @{text "vt"}.
-*}
+
+ The following are two very basic properties of @{text "vt"}. *}
lemma step_back_vt: "vt (e#s) \<Longrightarrow> vt s"
by(ind_cases "vt (e#s)", simp)
@@ -700,7 +722,7 @@
lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)"
by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv
- s_holding_abv cs_RAG_raw, auto)
+ s_holding_abv RAG_raw_def, auto)
lemma tRAG_alt_def:
"tRAG s = {(Th th1, Th th2) | th1 th2.
--- a/RTree.thy Tue Jun 07 13:51:39 2016 +0100
+++ b/RTree.thy Thu Jun 09 23:01:36 2016 +0100
@@ -1751,4 +1751,4 @@
declare RTree.plus_rpath[rule del]
-end
\ No newline at end of file
+end
--- a/Test.thy Tue Jun 07 13:51:39 2016 +0100
+++ b/Test.thy Thu Jun 09 23:01:36 2016 +0100
@@ -786,4 +786,4 @@
thm waits_def waits2_def
-end
\ No newline at end of file
+end
Binary file journal.pdf has changed