made some modifications.
--- a/CpsG.thy Wed Mar 12 10:08:20 2014 +0000
+++ b/CpsG.thy Tue May 06 14:36:40 2014 +0100
@@ -255,8 +255,8 @@
"children s th \<equiv> {th'. \<exists> cs. (Th th', Cs cs) \<in> depend s \<and> (Cs cs, Th th) \<in> depend s}"
unfolding child_def children_def by simp
-lemma children_dependents: "children s th \<subseteq> dependents (wq s) th"
- by (unfold children_def child_def cs_dependents_def, auto simp:eq_depend)
+lemma children_dependants: "children s th \<subseteq> dependants (wq s) th"
+ by (unfold children_def child_def cs_dependants_def, auto simp:eq_depend)
lemma child_unique:
assumes vt: "vt s"
@@ -446,20 +446,20 @@
show "\<And>a b c. \<lbrakk>(a, b) \<in> depend s; (a, c) \<in> depend s\<rbrakk> \<Longrightarrow> b = c" by auto
qed
-lemma dependents_child_unique:
+lemma dependants_child_unique:
fixes s th th1 th2 th3
assumes vt: "vt s"
and ch1: "(Th th1, Th th) \<in> child s"
and ch2: "(Th th2, Th th) \<in> child s"
- and dp1: "th3 \<in> dependents s th1"
- and dp2: "th3 \<in> dependents s th2"
+ and dp1: "th3 \<in> dependants s th1"
+ and dp2: "th3 \<in> dependants s th2"
shows "th1 = th2"
proof -
{ assume neq: "th1 \<noteq> th2"
from dp1 have dp1: "(Th th3, Th th1) \<in> (depend s)^+"
- by (simp add:s_dependents_def eq_depend)
+ by (simp add:s_dependants_def eq_depend)
from dp2 have dp2: "(Th th3, Th th2) \<in> (depend s)^+"
- by (simp add:s_dependents_def eq_depend)
+ by (simp add:s_dependants_def eq_depend)
from unique_depend_p[OF vt dp1 dp2] and neq
have "(Th th1, Th th2) \<in> (depend s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (depend s)\<^sup>+" by auto
hence False
@@ -479,90 +479,90 @@
shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"
proof(unfold cp_eq_cpreced_f cpreced_def)
let ?f = "(\<lambda>th. preced th s)"
- show "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) =
- Max ({preced th s} \<union> (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th)"
+ show "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)) =
+ Max ({preced th s} \<union> (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))) ` children s th)"
proof(cases " children s th = {}")
case False
- have "(\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th =
- {Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) | th' . th' \<in> children s th}"
+ have "(\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))) ` children s th =
+ {Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) | th' . th' \<in> children s th}"
(is "?L = ?R")
by auto
also have "\<dots> =
- Max ` {((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) | th' . th' \<in> children s th}"
+ Max ` {((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) | th' . th' \<in> children s th}"
(is "_ = Max ` ?C")
by auto
finally have "Max ?L = Max (Max ` ?C)" by auto
also have "\<dots> = Max (\<Union> ?C)"
proof(rule Max_Union[symmetric])
- from children_dependents[of s th] finite_threads[OF vt] and dependents_threads[OF vt, of th]
- show "finite {(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+ from children_dependants[of s th] finite_threads[OF vt] and dependants_threads[OF vt, of th]
+ show "finite {(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
by (auto simp:finite_subset)
next
from False
- show "{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th} \<noteq> {}"
+ show "{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th} \<noteq> {}"
by simp
next
- show "\<And>A. A \<in> {(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th} \<Longrightarrow>
+ show "\<And>A. A \<in> {(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th} \<Longrightarrow>
finite A \<and> A \<noteq> {}"
apply (auto simp:finite_subset)
proof -
fix th'
- from finite_threads[OF vt] and dependents_threads[OF vt, of th']
- show "finite ((\<lambda>th. preced th s) ` dependents (wq s) th')" by (auto simp:finite_subset)
+ from finite_threads[OF vt] and dependants_threads[OF vt, of th']
+ show "finite ((\<lambda>th. preced th s) ` dependants (wq s) th')" by (auto simp:finite_subset)
qed
qed
- also have "\<dots> = Max ((\<lambda>th. preced th s) ` dependents (wq s) th)"
+ also have "\<dots> = Max ((\<lambda>th. preced th s) ` dependants (wq s) th)"
(is "Max ?A = Max ?B")
proof -
have "?A = ?B"
proof
- show "\<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}
- \<subseteq> (\<lambda>th. preced th s) ` dependents (wq s) th"
+ show "\<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}
+ \<subseteq> (\<lambda>th. preced th s) ` dependants (wq s) th"
proof
fix x
- assume "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+ assume "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
then obtain th' where
th'_in: "th' \<in> children s th"
- and x_in: "x \<in> ?f ` ({th'} \<union> dependents (wq s) th')" by auto
- hence "x = ?f th' \<or> x \<in> (?f ` dependents (wq s) th')" by auto
- thus "x \<in> ?f ` dependents (wq s) th"
+ and x_in: "x \<in> ?f ` ({th'} \<union> dependants (wq s) th')" by auto
+ hence "x = ?f th' \<or> x \<in> (?f ` dependants (wq s) th')" by auto
+ thus "x \<in> ?f ` dependants (wq s) th"
proof
assume "x = preced th' s"
- with th'_in and children_dependents
- show "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th" by auto
+ with th'_in and children_dependants
+ show "x \<in> (\<lambda>th. preced th s) ` dependants (wq s) th" by auto
next
- assume "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th'"
+ assume "x \<in> (\<lambda>th. preced th s) ` dependants (wq s) th'"
moreover note th'_in
- ultimately show " x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th"
- by (unfold cs_dependents_def children_def child_def, auto simp:eq_depend)
+ ultimately show " x \<in> (\<lambda>th. preced th s) ` dependants (wq s) th"
+ by (unfold cs_dependants_def children_def child_def, auto simp:eq_depend)
qed
qed
next
- show "?f ` dependents (wq s) th
- \<subseteq> \<Union>{?f ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+ show "?f ` dependants (wq s) th
+ \<subseteq> \<Union>{?f ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
proof
fix x
- assume x_in: "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th"
+ assume x_in: "x \<in> (\<lambda>th. preced th s) ` dependants (wq s) th"
then obtain th' where
eq_x: "x = ?f th'" and dp: "(Th th', Th th) \<in> (depend s)^+"
- by (auto simp:cs_dependents_def eq_depend)
+ by (auto simp:cs_dependants_def eq_depend)
from depend_children[OF dp]
have "th' \<in> children s th \<or> (\<exists>th3. th3 \<in> children s th \<and> (Th th', Th th3) \<in> (depend s)\<^sup>+)" .
- thus "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+ thus "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
proof
assume "th' \<in> children s th"
with eq_x
- show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+ show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
by auto
next
assume "\<exists>th3. th3 \<in> children s th \<and> (Th th', Th th3) \<in> (depend s)\<^sup>+"
then obtain th3 where th3_in: "th3 \<in> children s th"
and dp3: "(Th th', Th th3) \<in> (depend s)\<^sup>+" by auto
- show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+ show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th') |th'. th' \<in> children s th}"
proof -
from dp3
- have "th' \<in> dependents (wq s) th3"
- by (auto simp:cs_dependents_def eq_depend)
+ have "th' \<in> dependants (wq s) th3"
+ by (auto simp:cs_dependants_def eq_depend)
with eq_x th3_in show ?thesis by auto
qed
qed
@@ -570,34 +570,34 @@
qed
thus ?thesis by simp
qed
- finally have "Max ((\<lambda>th. preced th s) ` dependents (wq s) th) = Max (?L)"
+ finally have "Max ((\<lambda>th. preced th s) ` dependants (wq s) th) = Max (?L)"
(is "?X = ?Y") by auto
- moreover have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) =
+ moreover have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)) =
max (?f th) ?X"
proof -
- have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) =
- Max ({?f th} \<union> ?f ` (dependents (wq s) th))" by simp
- also have "\<dots> = max (Max {?f th}) (Max (?f ` (dependents (wq s) th)))"
+ have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)) =
+ Max ({?f th} \<union> ?f ` (dependants (wq s) th))" by simp
+ also have "\<dots> = max (Max {?f th}) (Max (?f ` (dependants (wq s) th)))"
proof(rule Max_Un, auto)
- from finite_threads[OF vt] and dependents_threads[OF vt, of th]
- show "finite ((\<lambda>th. preced th s) ` dependents (wq s) th)" by (auto simp:finite_subset)
+ from finite_threads[OF vt] and dependants_threads[OF vt, of th]
+ show "finite ((\<lambda>th. preced th s) ` dependants (wq s) th)" by (auto simp:finite_subset)
next
- assume "dependents (wq s) th = {}"
- with False and children_dependents show False by auto
+ assume "dependants (wq s) th = {}"
+ with False and children_dependants show False by auto
qed
also have "\<dots> = max (?f th) ?X" by simp
finally show ?thesis .
qed
moreover have "Max ({preced th s} \<union>
- (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th) =
+ (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))) ` children s th) =
max (?f th) ?Y"
proof -
have "Max ({preced th s} \<union>
- (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th) =
+ (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))) ` children s th) =
max (Max {preced th s}) ?Y"
proof(rule Max_Un, auto)
- from finite_threads[OF vt] dependents_threads[OF vt, of th] children_dependents [of s th]
- show "finite ((\<lambda>th. Max (insert (preced th s) ((\<lambda>th. preced th s) ` dependents (wq s) th))) `
+ from finite_threads[OF vt] dependants_threads[OF vt, of th] children_dependants [of s th]
+ show "finite ((\<lambda>th. Max (insert (preced th s) ((\<lambda>th. preced th s) ` dependants (wq s) th))) `
children s th)"
by (auto simp:finite_subset)
next
@@ -609,11 +609,11 @@
ultimately show ?thesis by auto
next
case True
- moreover have "dependents (wq s) th = {}"
+ moreover have "dependants (wq s) th = {}"
proof -
{ fix th'
- assume "th' \<in> dependents (wq s) th"
- hence " (Th th', Th th) \<in> (depend s)\<^sup>+" by (simp add:cs_dependents_def eq_depend)
+ assume "th' \<in> dependants (wq s) th"
+ hence " (Th th', Th th) \<in> (depend s)\<^sup>+" by (simp add:cs_dependants_def eq_depend)
from depend_children[OF this] and True
have "False" by auto
} thus ?thesis by auto
@@ -648,46 +648,46 @@
lemma eq_cp_pre:
fixes th'
assumes neq_th: "th' \<noteq> th"
- and nd: "th \<notin> dependents s th'"
+ and nd: "th \<notin> dependants s th'"
shows "cp s th' = cp s' th'"
apply (unfold cp_eq_cpreced cpreced_def)
proof -
- have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
- by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
+ have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
+ by (unfold cs_dependants_def, auto simp:eq_dep eq_depend)
moreover {
fix th1
- assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
- hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+ assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
+ hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
hence "preced th1 s = preced th1 s'"
proof
assume "th1 = th'"
with eq_preced[OF neq_th]
show "preced th1 s = preced th1 s'" by simp
next
- assume "th1 \<in> dependents (wq s') th'"
+ assume "th1 \<in> dependants (wq s') th'"
with nd and eq_dp have "th1 \<noteq> th"
- by (auto simp:eq_depend cs_dependents_def s_dependents_def eq_dep)
+ by (auto simp:eq_depend cs_dependants_def s_dependants_def eq_dep)
from eq_preced[OF this] show "preced th1 s = preced th1 s'" by simp
qed
- } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
+ } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
by (auto simp:image_def)
- thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+ thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
qed
-lemma no_dependents:
+lemma no_dependants:
assumes "th' \<noteq> th"
- shows "th \<notin> dependents s th'"
+ shows "th \<notin> dependants s th'"
proof
- assume h: "th \<in> dependents s th'"
+ assume h: "th \<in> dependants s th'"
from step_back_step [OF vt_s[unfolded s_def]]
have "step s' (Set th prio)" .
hence "th \<in> runing s'" by (cases, simp)
hence rd_th: "th \<in> readys s'"
by (simp add:readys_def runing_def)
from h have "(Th th, Th th') \<in> (depend s')\<^sup>+"
- by (unfold s_dependents_def, unfold eq_depend, unfold eq_dep, auto)
+ by (unfold s_dependants_def, unfold eq_depend, unfold eq_dep, auto)
from tranclD[OF this]
obtain z where "(Th th, z) \<in> depend s'" by auto
with rd_th show "False"
@@ -701,19 +701,19 @@
assumes neq_th: "th' \<noteq> th"
shows "cp s th' = cp s' th'"
proof(rule eq_cp_pre [OF neq_th])
- from no_dependents[OF neq_th]
- show "th \<notin> dependents s th'" .
+ from no_dependants[OF neq_th]
+ show "th \<notin> dependants s th'" .
qed
lemma eq_up:
fixes th' th''
- assumes dp1: "th \<in> dependents s th'"
- and dp2: "th' \<in> dependents s th''"
+ assumes dp1: "th \<in> dependants s th'"
+ and dp2: "th' \<in> dependants s th''"
and eq_cps: "cp s th' = cp s' th'"
shows "cp s th'' = cp s' th''"
proof -
from dp2
- have "(Th th', Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def)
+ have "(Th th', Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependants_def)
from depend_child[OF vt_s this[unfolded eq_depend]]
have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .
moreover { fix n th''
@@ -726,7 +726,7 @@
and ch': "(Th th', y) \<in> (child s)\<^sup>+"
from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
with ih have eq_cpy:"cp s thy = cp s' thy" by blast
- from dp1 have "(Th th, Th th') \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend)
+ from dp1 have "(Th th, Th th') \<in> (depend s)^+" by (auto simp:s_dependants_def eq_depend)
moreover from child_depend_p[OF ch'] and eq_y
have "(Th th', Th thy) \<in> (depend s)^+" by simp
ultimately have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by auto
@@ -761,11 +761,11 @@
from children_no_dep[OF vt_s _ _ this] and
th1_in y_ch eq_y show False by (auto simp:children_def)
qed
- have "th \<notin> dependents s th1"
+ have "th \<notin> dependants s th1"
proof
- assume h:"th \<in> dependents s th1"
- from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)
- from dependents_child_unique[OF vt_s _ _ h this]
+ assume h:"th \<in> dependants s th1"
+ from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_depend)
+ from dependants_child_unique[OF vt_s _ _ h this]
th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
with False show False by auto
qed
@@ -793,7 +793,7 @@
assume "th'' = th"
with dp1 dp'
have "(Th th, Th th) \<in> (depend s)^+"
- by (auto simp:child_def s_dependents_def eq_depend)
+ by (auto simp:child_def s_dependants_def eq_depend)
with wf_trancl[OF wf_depend[OF vt_s]]
show False by auto
qed
@@ -811,17 +811,17 @@
proof
assume eq_th1: "th1 = th"
with dp1 have "(Th th1, Th th') \<in> (depend s)^+"
- by (auto simp:s_dependents_def eq_depend)
+ by (auto simp:s_dependants_def eq_depend)
from children_no_dep[OF vt_s _ _ this]
th1_in dp'
show False by (auto simp:children_def)
qed
thus ?thesis
proof(rule eq_cp_pre)
- show "th \<notin> dependents s th1"
+ show "th \<notin> dependants s th1"
proof
- assume "th \<in> dependents s th1"
- from dependents_child_unique[OF vt_s _ _ this dp1]
+ assume "th \<in> dependants s th1"
+ from dependants_child_unique[OF vt_s _ _ this dp1]
th1_in dp' have "th1 = th'"
by (auto simp:children_def)
with False show False by auto
@@ -843,12 +843,12 @@
lemma eq_up_self:
fixes th' th''
- assumes dp: "th \<in> dependents s th''"
+ assumes dp: "th \<in> dependants s th''"
and eq_cps: "cp s th = cp s' th"
shows "cp s th'' = cp s' th''"
proof -
from dp
- have "(Th th, Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def)
+ have "(Th th, Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependants_def)
from depend_child[OF vt_s this[unfolded eq_depend]]
have ch_th': "(Th th, Th th'') \<in> (child s)\<^sup>+" .
moreover { fix n th''
@@ -894,11 +894,11 @@
from children_no_dep[OF vt_s _ _ this] and
th1_in y_ch eq_y show False by (auto simp:children_def)
qed
- have "th \<notin> dependents s th1"
+ have "th \<notin> dependants s th1"
proof
- assume h:"th \<in> dependents s th1"
- from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)
- from dependents_child_unique[OF vt_s _ _ h this]
+ assume h:"th \<in> dependants s th1"
+ from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_depend)
+ from dependants_child_unique[OF vt_s _ _ h this]
th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
with False show False by auto
qed
@@ -926,7 +926,7 @@
assume "th'' = th"
with dp dp'
have "(Th th, Th th) \<in> (depend s)^+"
- by (auto simp:child_def s_dependents_def eq_depend)
+ by (auto simp:child_def s_dependants_def eq_depend)
with wf_trancl[OF wf_depend[OF vt_s]]
show False by auto
qed
@@ -943,10 +943,10 @@
assume neq_th1: "th1 \<noteq> th"
thus ?thesis
proof(rule eq_cp_pre)
- show "th \<notin> dependents s th1"
+ show "th \<notin> dependants s th1"
proof
- assume "th \<in> dependents s th1"
- hence "(Th th, Th th1) \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend)
+ assume "th \<in> dependants s th1"
+ hence "(Th th, Th th1) \<in> (depend s)^+" by (auto simp:s_dependants_def eq_depend)
from children_no_dep[OF vt_s _ _ this]
and th1_in dp' show False
by (auto simp:children_def)
@@ -1046,16 +1046,16 @@
and nt show ?thesis by (auto intro:next_th_unique)
qed
-lemma dependents_kept:
+lemma dependants_kept:
fixes th''
assumes neq1: "th'' \<noteq> th"
and neq2: "th'' \<noteq> th'"
- shows "dependents (wq s) th'' = dependents (wq s') th''"
+ shows "dependants (wq s) th'' = dependants (wq s') th''"
proof(auto)
fix x
- assume "x \<in> dependents (wq s) th''"
+ assume "x \<in> dependants (wq s) th''"
hence dp: "(Th x, Th th'') \<in> (depend s)^+"
- by (auto simp:cs_dependents_def eq_depend)
+ by (auto simp:cs_dependants_def eq_depend)
{ fix n
have "(n, Th th'') \<in> (depend s)^+ \<Longrightarrow> (n, Th th'') \<in> (depend s')^+"
proof(induct rule:converse_trancl_induct)
@@ -1120,13 +1120,13 @@
qed
}
from this[OF dp]
- show "x \<in> dependents (wq s') th''"
- by (auto simp:cs_dependents_def eq_depend)
+ show "x \<in> dependants (wq s') th''"
+ by (auto simp:cs_dependants_def eq_depend)
next
fix x
- assume "x \<in> dependents (wq s') th''"
+ assume "x \<in> dependants (wq s') th''"
hence dp: "(Th x, Th th'') \<in> (depend s')^+"
- by (auto simp:cs_dependents_def eq_depend)
+ by (auto simp:cs_dependants_def eq_depend)
{ fix n
have "(n, Th th'') \<in> (depend s')^+ \<Longrightarrow> (n, Th th'') \<in> (depend s)^+"
proof(induct rule:converse_trancl_induct)
@@ -1209,8 +1209,8 @@
qed
}
from this[OF dp]
- show "x \<in> dependents (wq s) th''"
- by (auto simp:cs_dependents_def eq_depend)
+ show "x \<in> dependants (wq s) th''"
+ by (auto simp:cs_dependants_def eq_depend)
qed
lemma cp_kept:
@@ -1219,18 +1219,18 @@
and neq2: "th'' \<noteq> th'"
shows "cp s th'' = cp s' th''"
proof -
- from dependents_kept[OF neq1 neq2]
- have "dependents (wq s) th'' = dependents (wq s') th''" .
+ from dependants_kept[OF neq1 neq2]
+ have "dependants (wq s) th'' = dependants (wq s') th''" .
moreover {
fix th1
- assume "th1 \<in> dependents (wq s) th''"
+ assume "th1 \<in> dependants (wq s) th''"
have "preced th1 s = preced th1 s'"
by (unfold s_def, auto simp:preced_def)
}
moreover have "preced th'' s = preced th'' s'"
by (unfold s_def, auto simp:preced_def)
- ultimately have "((\<lambda>th. preced th s) ` ({th''} \<union> dependents (wq s) th'')) =
- ((\<lambda>th. preced th s') ` ({th''} \<union> dependents (wq s') th''))"
+ ultimately have "((\<lambda>th. preced th s) ` ({th''} \<union> dependants (wq s) th'')) =
+ ((\<lambda>th. preced th s') ` ({th''} \<union> dependants (wq s') th''))"
by (auto simp:image_def)
thus ?thesis
by (unfold cp_eq_cpreced cpreced_def, simp)
@@ -1352,8 +1352,8 @@
shows "cp s th' = cp s' th'"
apply (unfold cp_eq_cpreced cpreced_def)
proof -
- have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
- apply (unfold cs_dependents_def, unfold eq_depend)
+ have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
+ apply (unfold cs_dependants_def, unfold eq_depend)
proof -
from eq_child
have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}"
@@ -1364,21 +1364,21 @@
qed
moreover {
fix th1
- assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
- hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+ assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
+ hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
hence "preced th1 s = preced th1 s'"
proof
assume "th1 = th'"
show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
next
- assume "th1 \<in> dependents (wq s') th'"
+ assume "th1 \<in> dependants (wq s') th'"
show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
qed
- } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
+ } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
by (auto simp:image_def)
- thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+ thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
qed
end
@@ -1496,8 +1496,8 @@
shows "cp s th' = cp s' th'"
apply (unfold cp_eq_cpreced cpreced_def)
proof -
- have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
- apply (unfold cs_dependents_def, unfold eq_depend)
+ have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
+ apply (unfold cs_dependants_def, unfold eq_depend)
proof -
from eq_child
have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}"
@@ -1508,21 +1508,21 @@
qed
moreover {
fix th1
- assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
- hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+ assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
+ hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
hence "preced th1 s = preced th1 s'"
proof
assume "th1 = th'"
show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
next
- assume "th1 \<in> dependents (wq s') th'"
+ assume "th1 \<in> dependants (wq s') th'"
show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
qed
- } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
+ } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
by (auto simp:image_def)
- thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+ thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
qed
end
@@ -1597,7 +1597,7 @@
lemma eq_cp:
fixes th'
- assumes nd: "th \<notin> dependents s th'"
+ assumes nd: "th \<notin> dependants s th'"
shows "cp s th' = cp s' th'"
apply (unfold cp_eq_cpreced cpreced_def)
proof -
@@ -1607,13 +1607,13 @@
with child_depend_eq[OF vt_s]
have "(Th th, Th th') \<in> (depend s)\<^sup>+" by simp
with nd show False
- by (simp add:s_dependents_def eq_depend)
+ by (simp add:s_dependants_def eq_depend)
qed
- have eq_dp: "dependents (wq s) th' = dependents (wq s') th'"
+ have eq_dp: "dependants (wq s) th' = dependants (wq s') th'"
proof(auto)
- fix x assume " x \<in> dependents (wq s) th'"
- thus "x \<in> dependents (wq s') th'"
- apply (auto simp:cs_dependents_def eq_depend)
+ fix x assume " x \<in> dependants (wq s) th'"
+ thus "x \<in> dependants (wq s') th'"
+ apply (auto simp:cs_dependants_def eq_depend)
proof -
assume "(Th x, Th th') \<in> (depend s)\<^sup>+"
with child_depend_eq[OF vt_s] have "(Th x, Th th') \<in> (child s)\<^sup>+" by simp
@@ -1622,9 +1622,9 @@
show "(Th x, Th th') \<in> (depend s')\<^sup>+" by simp
qed
next
- fix x assume "x \<in> dependents (wq s') th'"
- thus "x \<in> dependents (wq s) th'"
- apply (auto simp:cs_dependents_def eq_depend)
+ fix x assume "x \<in> dependants (wq s') th'"
+ thus "x \<in> dependants (wq s) th'"
+ apply (auto simp:cs_dependants_def eq_depend)
proof -
assume "(Th x, Th th') \<in> (depend s')\<^sup>+"
with child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
@@ -1636,22 +1636,22 @@
qed
moreover {
fix th1 have "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
- } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
+ } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
by (auto simp:image_def)
- thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+ thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
qed
lemma eq_up:
fixes th' th''
- assumes dp1: "th \<in> dependents s th'"
- and dp2: "th' \<in> dependents s th''"
+ assumes dp1: "th \<in> dependants s th'"
+ and dp2: "th' \<in> dependants s th''"
and eq_cps: "cp s th' = cp s' th'"
shows "cp s th'' = cp s' th''"
proof -
from dp2
- have "(Th th', Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def)
+ have "(Th th', Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependants_def)
from depend_child[OF vt_s this[unfolded eq_depend]]
have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .
moreover {
@@ -1665,7 +1665,7 @@
and ch': "(Th th', y) \<in> (child s)\<^sup>+"
from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
with ih have eq_cpy:"cp s thy = cp s' thy" by blast
- from dp1 have "(Th th, Th th') \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend)
+ from dp1 have "(Th th, Th th') \<in> (depend s)^+" by (auto simp:s_dependants_def eq_depend)
moreover from child_depend_p[OF ch'] and eq_y
have "(Th th', Th thy) \<in> (depend s)^+" by simp
ultimately have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by auto
@@ -1690,11 +1690,11 @@
from children_no_dep[OF vt_s _ _ this] and
th1_in y_ch eq_y show False by (auto simp:children_def)
qed
- have "th \<notin> dependents s th1"
+ have "th \<notin> dependants s th1"
proof
- assume h:"th \<in> dependents s th1"
- from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)
- from dependents_child_unique[OF vt_s _ _ h this]
+ assume h:"th \<in> dependants s th1"
+ from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_depend)
+ from dependants_child_unique[OF vt_s _ _ h this]
th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
with False show False by auto
qed
@@ -1711,7 +1711,7 @@
assume "(Cs cs, Th th'') \<in> depend s'"
with depend_s have cs_th': "(Cs cs, Th th'') \<in> depend s" by auto
from dp1 have "(Th th, Th th') \<in> (depend s)^+"
- by (auto simp:s_dependents_def eq_depend)
+ by (auto simp:s_dependants_def eq_depend)
from converse_tranclE[OF this]
obtain cs1 where h1: "(Th th, Cs cs1) \<in> depend s"
and h2: "(Cs cs1 , Th th') \<in> (depend s)\<^sup>+"
@@ -1772,17 +1772,17 @@
proof
assume eq_th1: "th1 = th"
with dp1 have "(Th th1, Th th') \<in> (depend s)^+"
- by (auto simp:s_dependents_def eq_depend)
+ by (auto simp:s_dependants_def eq_depend)
from children_no_dep[OF vt_s _ _ this]
th1_in dp'
show False by (auto simp:children_def)
qed
show ?thesis
proof(rule eq_cp)
- show "th \<notin> dependents s th1"
+ show "th \<notin> dependants s th1"
proof
- assume "th \<in> dependents s th1"
- from dependents_child_unique[OF vt_s _ _ this dp1]
+ assume "th \<in> dependants s th1"
+ from dependants_child_unique[OF vt_s _ _ this dp1]
th1_in dp' have "th1 = th'"
by (auto simp:children_def)
with False show False by auto
@@ -1799,7 +1799,7 @@
assume "(Cs cs, Th th'') \<in> depend s'"
with depend_s have cs_th': "(Cs cs, Th th'') \<in> depend s" by auto
from dp1 have "(Th th, Th th') \<in> (depend s)^+"
- by (auto simp:s_dependents_def eq_depend)
+ by (auto simp:s_dependants_def eq_depend)
from converse_tranclE[OF this]
obtain cs1 where h1: "(Th th, Cs cs1) \<in> depend s"
and h2: "(Cs cs1 , Th th') \<in> (depend s)\<^sup>+"
@@ -1863,10 +1863,10 @@
shows "cp s th' = cp s' th'"
apply (unfold cp_eq_cpreced cpreced_def)
proof -
- have nd: "th \<notin> dependents s th'"
+ have nd: "th \<notin> dependants s th'"
proof
- assume "th \<in> dependents s th'"
- hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependents_def eq_depend)
+ assume "th \<in> dependants s th'"
+ hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependants_def eq_depend)
with eq_dep have "(Th th, Th th') \<in> (depend s')^+" by simp
from converse_tranclE[OF this]
obtain y where "(Th th, y) \<in> depend s'" by auto
@@ -1879,31 +1879,31 @@
with in_th show ?thesis by simp
qed
qed
- have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
- by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
+ have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
+ by (unfold cs_dependants_def, auto simp:eq_dep eq_depend)
moreover {
fix th1
- assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
- hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+ assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
+ hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
hence "preced th1 s = preced th1 s'"
proof
assume "th1 = th'"
with neq_th
show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
next
- assume "th1 \<in> dependents (wq s') th'"
+ assume "th1 \<in> dependants (wq s') th'"
with nd and eq_dp have "th1 \<noteq> th"
- by (auto simp:eq_depend cs_dependents_def s_dependents_def eq_dep)
+ by (auto simp:eq_depend cs_dependants_def s_dependants_def eq_dep)
thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
qed
- } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
+ } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
by (auto simp:image_def)
- thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+ thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
qed
-lemma nil_dependents: "dependents s th = {}"
+lemma nil_dependants: "dependants s th = {}"
proof -
from step_back_step[OF vt_s[unfolded s_def]]
show ?thesis
@@ -1911,11 +1911,11 @@
assume "th \<notin> threads s'"
from not_thread_holdents[OF step_back_vt[OF vt_s[unfolded s_def]] this]
have hdn: " holdents s' th = {}" .
- have "dependents s' th = {}"
+ have "dependants s' th = {}"
proof -
- { assume "dependents s' th \<noteq> {}"
+ { assume "dependants s' th \<noteq> {}"
then obtain th' where dp: "(Th th', Th th) \<in> (depend s')^+"
- by (auto simp:s_dependents_def eq_depend)
+ by (auto simp:s_dependants_def eq_depend)
from tranclE[OF this] obtain cs' where
"(Cs cs', Th th) \<in> depend s'" by (auto simp:s_depend_def)
with hdn
@@ -1923,13 +1923,13 @@
} thus ?thesis by auto
qed
thus ?thesis
- by (unfold s_def s_dependents_def eq_depend depend_create_unchanged, simp)
+ by (unfold s_def s_dependants_def eq_depend depend_create_unchanged, simp)
qed
qed
lemma eq_cp_th: "cp s th = preced th s"
apply (unfold cp_eq_cpreced cpreced_def)
- by (insert nil_dependents, unfold s_dependents_def cs_dependents_def, auto)
+ by (insert nil_dependants, unfold s_dependants_def cs_dependants_def, auto)
end
@@ -1951,10 +1951,10 @@
shows "cp s th' = cp s' th'"
apply (unfold cp_eq_cpreced cpreced_def)
proof -
- have nd: "th \<notin> dependents s th'"
+ have nd: "th \<notin> dependants s th'"
proof
- assume "th \<in> dependents s th'"
- hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependents_def eq_depend)
+ assume "th \<in> dependants s th'"
+ hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependants_def eq_depend)
with eq_dep have "(Th th, Th th') \<in> (depend s')^+" by simp
from converse_tranclE[OF this]
obtain cs' where bk: "(Th th, Cs cs') \<in> depend s'"
@@ -1968,28 +1968,28 @@
by (auto simp:cs_waiting_def wq_def)
qed
qed
- have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
- by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
+ have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
+ by (unfold cs_dependants_def, auto simp:eq_dep eq_depend)
moreover {
fix th1
- assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
- hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+ assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
+ hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
hence "preced th1 s = preced th1 s'"
proof
assume "th1 = th'"
with neq_th
show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
next
- assume "th1 \<in> dependents (wq s') th'"
+ assume "th1 \<in> dependants (wq s') th'"
with nd and eq_dp have "th1 \<noteq> th"
- by (auto simp:eq_depend cs_dependents_def s_dependents_def eq_dep)
+ by (auto simp:eq_depend cs_dependants_def s_dependants_def eq_dep)
thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
qed
- } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
+ } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
by (auto simp:image_def)
- thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
- Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+ thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+ Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
qed
end
--- a/ExtGG.thy Wed Mar 12 10:08:20 2014 +0000
+++ b/ExtGG.thy Tue May 06 14:36:40 2014 +0100
@@ -2,21 +2,21 @@
imports PrioG
begin
-lemma birth_time_lt: "s \<noteq> [] \<Longrightarrow> birthtime th s < length s"
+lemma birth_time_lt: "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
apply (induct s, simp)
proof -
fix a s
- assume ih: "s \<noteq> [] \<Longrightarrow> birthtime th s < length s"
+ assume ih: "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
and eq_as: "a # s \<noteq> []"
- show "birthtime th (a # s) < length (a # s)"
+ show "last_set th (a # s) < length (a # s)"
proof(cases "s \<noteq> []")
case False
from False show ?thesis
- by (cases a, auto simp:birthtime.simps)
+ by (cases a, auto simp:last_set.simps)
next
case True
from ih [OF True] show ?thesis
- by (cases a, auto simp:birthtime.simps)
+ by (cases a, auto simp:last_set.simps)
qed
qed
@@ -46,18 +46,18 @@
proof -
from highest and max_cp_eq[OF vt_s]
have is_max: "preced th s = Max ((\<lambda>th. preced th s) ` threads s)" by simp
- have sbs: "({th} \<union> dependents (wq s) th) \<subseteq> threads s"
+ have sbs: "({th} \<union> dependants (wq s) th) \<subseteq> threads s"
proof -
- from threads_s and dependents_threads[OF vt_s, of th]
+ from threads_s and dependants_threads[OF vt_s, of th]
show ?thesis by auto
qed
show ?thesis
proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI)
- show "preced th s \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)" by simp
+ show "preced th s \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)" by simp
next
fix y
- assume "y \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)"
- then obtain th1 where th1_in: "th1 \<in> ({th} \<union> dependents (wq s) th)"
+ assume "y \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)"
+ then obtain th1 where th1_in: "th1 \<in> ({th} \<union> dependants (wq s) th)"
and eq_y: "y = preced th1 s" by auto
show "y \<le> preced th s"
proof(unfold is_max, rule Max_ge)
@@ -69,7 +69,7 @@
qed
next
from sbs and finite_threads[OF vt_s]
- show "finite ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))"
+ show "finite ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))"
by (auto intro:finite_subset)
qed
qed
@@ -469,7 +469,7 @@
by (unfold cp_eq_cpreced, simp)
also have "\<dots> = ?R"
proof(unfold cpreced_def)
- show "Max ((\<lambda>th. preced th (t @ s)) ` ({th} \<union> dependents (wq (t @ s)) th)) =
+ show "Max ((\<lambda>th. preced th (t @ s)) ` ({th} \<union> dependants (wq (t @ s)) th)) =
Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))"
(is "Max (?f ` ({th} \<union> ?A)) = Max (?f ` ?B)")
proof(cases "?A = {}")
@@ -479,7 +479,7 @@
proof(rule Max_insert)
show "finite (?f ` ?A)"
proof -
- from dependents_threads[OF vt_t]
+ from dependants_threads[OF vt_t]
have "?A \<subseteq> threads (t@s)" .
moreover from finite_threads[OF vt_t] have "finite \<dots>" .
ultimately show ?thesis
@@ -497,7 +497,7 @@
next
show "?f ` ?A \<subseteq> ?f ` ?B"
proof -
- have "?A \<subseteq> ?B" by (rule dependents_threads[OF vt_t])
+ have "?A \<subseteq> ?B" by (rule dependants_threads[OF vt_t])
thus ?thesis by auto
qed
next
@@ -566,8 +566,8 @@
finally have h: "cp (t @ s) th' = preced th (t @ s)" .
show False
proof -
- have "dependents (wq (t @ s)) th' = {}"
- by (rule count_eq_dependents [OF vt_t eq_pv])
+ have "dependants (wq (t @ s)) th' = {}"
+ by (rule count_eq_dependants [OF vt_t eq_pv])
moreover have "preced th' (t @ s) \<noteq> preced th (t @ s)"
proof
assume "preced th' (t @ s) = preced th (t @ s)"
@@ -983,13 +983,13 @@
proof -
have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"
proof -
- have " Max ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependents (wq (t @ s)) th')) =
+ have " Max ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th')) =
preced th (t@s)"
proof(rule Max_eqI)
fix y
- assume "y \<in> (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependents (wq (t @ s)) th')"
+ assume "y \<in> (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th')"
then obtain th1 where
- h1: "th1 = th' \<or> th1 \<in> dependents (wq (t @ s)) th'"
+ h1: "th1 = th' \<or> th1 \<in> dependants (wq (t @ s)) th'"
and eq_y: "y = preced th1 (t@s)" by auto
show "y \<le> preced th (t @ s)"
proof -
@@ -1003,8 +1003,8 @@
assume "th1 = th'"
with th'_in show ?thesis by (simp add:readys_def)
next
- assume "th1 \<in> dependents (wq (t @ s)) th'"
- with dependents_threads [OF vt_t]
+ assume "th1 \<in> dependants (wq (t @ s)) th'"
+ with dependants_threads [OF vt_t]
show "th1 \<in> threads (t @ s)" by auto
qed
with eq_y show " y \<in> (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)" by simp
@@ -1015,15 +1015,15 @@
ultimately show ?thesis by auto
qed
next
- from finite_threads[OF vt_t] dependents_threads [OF vt_t, of th']
- show "finite ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependents (wq (t @ s)) th'))"
+ from finite_threads[OF vt_t] dependants_threads [OF vt_t, of th']
+ show "finite ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th'))"
by (auto intro:finite_subset)
next
from dp
- have "th \<in> dependents (wq (t @ s)) th'"
- by (unfold cs_dependents_def, auto simp:eq_depend)
+ have "th \<in> dependants (wq (t @ s)) th'"
+ by (unfold cs_dependants_def, auto simp:eq_depend)
thus "preced th (t @ s) \<in>
- (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependents (wq (t @ s)) th')"
+ (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th')"
by auto
qed
moreover have "\<dots> = Max (cp (t @ s) ` readys (t @ s))"
--- a/Journal/Paper.thy Wed Mar 12 10:08:20 2014 +0000
+++ b/Journal/Paper.thy Tue May 06 14:36:40 2014 +0100
@@ -11,7 +11,6 @@
Cons ("_::_" [78,77] 73) and
vt ("valid'_state") and
runing ("running") and
- birthtime ("last'_set") and
If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
Prc ("'(_, _')") and
holding ("holds") and
@@ -22,10 +21,8 @@
depend ("RAG") and
preced ("prec") and
cpreced ("cprec") and
- dependents ("dependants") and
cp ("cprec") and
holdents ("resources") and
- original_priority ("priority") and
DUMMY ("\<^raw:\mbox{$\_\!\_$}>")
@@ -83,7 +80,7 @@
implemented. This includes VxWorks (a proprietary real-time OS used
in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's
ASIMO robot, etc.) and ThreadX (another proprietary real-time OS
- used in HP inkjet printers \cite{ThreadX}), but also
+ used in nearly all HP inkjet printers \cite{ThreadX}), but also
the POSIX 1003.1c Standard realised for
example in libraries for FreeBSD, Solaris and Linux.
@@ -92,7 +89,7 @@
This is in contrast to \emph{Priority Ceiling}
\cite{Sha90}, another solution to the Priority Inversion problem,
which requires static analysis of the program in order to prevent
- Priority Inversion, and also in contrast to the Windows NT scheduler, which avoids
+ Priority Inversion, and also in contrast to the approach taken in the Windows NT scheduler, which avoids
this problem by randomly boosting the priority of ready low-priority threads
(see for instance~\cite{WINDOWSNT}).
However, there has also been strong criticism against
@@ -141,11 +138,12 @@
point to a subtlety that had been
overlooked in the informal proof by Sha et al. They specify in
\cite{Sha90} that after the thread (whose priority has been raised)
- completes its critical section and releases the lock, it ``returns
- to its original priority level.'' This leads them to believe that an
- implementation of PIP is ``rather straightforward''~\cite{Sha90}.
+ completes its critical section and releases the lock, it ``{\it returns
+ to its original priority level}''. This leads them to believe that an
+ implementation of PIP is ``{\it rather straightforward}''~\cite{Sha90}.
Unfortunately, as Yodaiken and Moylan et al.~point out, this behaviour is too
- simplistic. Consider the case where the low priority thread $L$
+ simplistic. Moylan et al.~write that there are ``{\it some hidden traps}''.
+ Consider the case where the low priority thread $L$
locks \emph{two} resources, and two high-priority threads $H$ and
$H'$ each wait for one of them. If $L$ releases one resource
so that $H$, say, can proceed, then we still have Priority Inversion
@@ -153,8 +151,8 @@
behaviour for $L$ is to switch to the highest remaining priority of
the threads that it blocks. A similar error is made in the textbook
\cite[Section 2.3.1]{book} which specifies for a process that
- inherited a higher priority and exits a critical section ``it resumes
- the priority it had at the point of entry into the critical section''.
+ inherited a higher priority and exits a critical section ``{\it it resumes
+ the priority it had at the point of entry into the critical section}''.
While \cite{book} and
\cite{Sha90} are the only formal publications we have
@@ -184,9 +182,59 @@
in the reference implementation of PIP in PINTOS. This fact, however, is important
for an efficient implementation of PIP, because we can give the lock
to the thread with the highest priority so that it terminates more
- quickly. We were also able to generalise the scheduler of Sha
+ quickly. We were also being able to generalise the scheduler of Sha
et al.~\cite{Sha90} to the practically relevant case where critical
- sections can overlap.
+ sections can overlap; see Figure~\ref{overlap} below for an example of
+ this restriction. In the existing literature there is no
+ proof and also no prove method that cover this generalised case.
+
+ \begin{figure}
+ \begin{center}
+ \begin{tikzpicture}[scale=1]
+ %%\draw[step=2mm] (0,0) grid (10,2);
+ \draw [->,line width=0.6mm] (0,0) -- (10,0);
+ \draw [->,line width=0.6mm] (0,1.5) -- (10,1.5);
+ \draw [line width=0.6mm, pattern=horizontal lines] (0.8,0) rectangle (4,0.5);
+ \draw [line width=0.6mm, pattern=north east lines] (3.0,0) rectangle (6,0.5);
+ \draw [line width=0.6mm, pattern=vertical lines] (5.0,0) rectangle (9,0.5);
+
+ \draw [line width=0.6mm, pattern=horizontal lines] (0.6,1.5) rectangle (4.0,2);
+ \draw [line width=0.6mm, pattern=north east lines] (1.0,1.5) rectangle (3.4,2);
+ \draw [line width=0.6mm, pattern=vertical lines] (5.0,1.5) rectangle (8.8,2);
+
+ \node at (0.8,-0.3) {@{term "P\<^sub>1"}};
+ \node at (3.0,-0.3) {@{term "P\<^sub>2"}};
+ \node at (4.0,-0.3) {@{term "V\<^sub>1"}};
+ \node at (5.0,-0.3) {@{term "P\<^sub>3"}};
+ \node at (6.0,-0.3) {@{term "V\<^sub>2"}};
+ \node at (9.0,-0.3) {@{term "V\<^sub>3"}};
+
+ \node at (0.6,1.2) {@{term "P\<^sub>1"}};
+ \node at (1.0,1.2) {@{term "P\<^sub>2"}};
+ \node at (3.4,1.2) {@{term "V\<^sub>2"}};
+ \node at (4.0,1.2) {@{term "V\<^sub>1"}};
+ \node at (5.0,1.2) {@{term "P\<^sub>3"}};
+ \node at (8.8,1.2) {@{term "V\<^sub>3"}};
+ \node at (10.3,0) {$t$};
+ \node at (10.3,1.5) {$t$};
+
+ \node at (-0.3,0.2) {$b)$};
+ \node at (-0.3,1.7) {$a)$};
+ \end{tikzpicture}\mbox{}\\[-10mm]\mbox{}
+ \end{center}
+ \caption{Assume a process is over time locking and unlocking, say, three resources.
+ The locking requests are labelled @{term "P\<^sub>1"}, @{term "P\<^sub>2"}, and @{term "P\<^sub>3"}
+ respectively, and the corresponding unlocking operations are labelled
+ @{term "V\<^sub>1"}, @{term "V\<^sub>2"}, and @{term "V\<^sub>3"}.
+ Then graph $a)$ shows \emph{properly nested} critical sections as required
+ by Sha et al.~\cite{Sha90} in their proof---the sections must either be contained within
+ each other
+ (the section @{term "P\<^sub>2"}--@{term "V\<^sub>2"} is contained in @{term "P\<^sub>1"}--@{term "V\<^sub>1"}) or
+ be independent (@{term "P\<^sub>3"}--@{term "V\<^sub>3"} is independent from the other
+ two). Graph $b)$ shows the general case where
+ the locking and unlocking of different critical sections can
+ overlap.\label{overlap}}
+ \end{figure}
*}
section {* Formal Model of the Priority Inheritance Protocol\label{model} *}
@@ -205,9 +253,9 @@
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}
\isacommand{datatype} event
- & @{text "="} & @{term "Create thread priority"}\\
+ & @{text "="} & @{term "Create thread priority\<iota>"}\\
& @{text "|"} & @{term "Exit thread"} \\
- & @{text "|"} & @{term "Set thread priority"} & {\rm reset of the priority for} @{text thread}\\
+ & @{text "|"} & @{term "Set thread priority\<iota>"} & {\rm reset of the priority for} @{text thread}\\
& @{text "|"} & @{term "P thread cs"} & {\rm request of resource} @{text "cs"} {\rm by} @{text "thread"}\\
& @{text "|"} & @{term "V thread cs"} & {\rm release of resource} @{text "cs"} {\rm by} @{text "thread"}
\end{tabular}}
@@ -235,37 +283,37 @@
\end{isabelle}
\noindent
- In this definition @{term "DUMMY # DUMMY"} stands for list-cons.
+ In this definition @{term "DUMMY # DUMMY"} stands for list-cons and @{term "[]"} for the empty list.
Another function calculates the priority for a thread @{text "th"}, which is
defined as
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{lcl}
- @{thm (lhs) original_priority.simps(1)[where thread="th"]} & @{text "\<equiv>"} &
- @{thm (rhs) original_priority.simps(1)[where thread="th"]}\\
- @{thm (lhs) original_priority.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
- @{thm (rhs) original_priority.simps(2)[where thread="th" and thread'="th'"]}\\
- @{thm (lhs) original_priority.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
- @{thm (rhs) original_priority.simps(3)[where thread="th" and thread'="th'"]}\\
- @{term "original_priority th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "original_priority th s"}\\
+ @{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'"]}\\
+ @{term "priority th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "priority th s"}\\
\end{tabular}}
\end{isabelle}
\noindent
In this definition we set @{text 0} as the default priority for
threads that have not (yet) been created. The last function we need
- calculates the ``time'', or index, at which time a process had its
+ calculates the ``time'', or index, at which time a thread had its
priority last set.
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{lcl}
- @{thm (lhs) birthtime.simps(1)[where thread="th"]} & @{text "\<equiv>"} &
- @{thm (rhs) birthtime.simps(1)[where thread="th"]}\\
- @{thm (lhs) birthtime.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
- @{thm (rhs) birthtime.simps(2)[where thread="th" and thread'="th'"]}\\
- @{thm (lhs) birthtime.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
- @{thm (rhs) birthtime.simps(3)[where thread="th" and thread'="th'"]}\\
- @{term "birthtime th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "birthtime th s"}\\
+ @{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'"]}\\
+ @{term "last_set th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "last_set th s"}\\
\end{tabular}}
\end{isabelle}
@@ -286,8 +334,15 @@
taking into account the time when the priority was last set. We order precedences so
that threads with the same priority get a higher precedence if their priority has been
set earlier, since for such threads it is more urgent to finish their work. In an implementation
- this choice would translate to a quite natural FIFO-scheduling of processes with
- the same priority.
+ this choice would translate to a quite natural FIFO-scheduling of threads with
+ the same priority.
+
+ Moylan et al.~\cite{deinheritance} considered the alternative of
+ ``time-slicing'' threads with equal priority, but found that it does not lead to
+ advantages in practice. On the contrary, according to their work having a policy
+ like our FIFO-scheduling of threads with equal priority reduces the number of
+ tasks involved in the inheritance process and thus minimises the number
+ of potentially expensive thread-switches.
Next, we introduce the concept of \emph{waiting queues}. They are
lists of threads associated with every resource. The first thread in
@@ -385,7 +440,7 @@
so that every thread can be in the possession of several resources, that is
it has potentially several incoming holding edges in the RAG, but has at most one outgoing
waiting edge. The reason is that when a thread asks for resource that is locked
- already, then the process is blocked and cannot ask for another resource.
+ already, then the thread is blocked and cannot ask for another resource.
Clearly, also every resource can only have at most one outgoing holding edge---indicating
that the resource is locked. In this way we can always start at a thread waiting for a
resource and ``chase'' outgoing arrows leading to a single root of a tree.
@@ -394,16 +449,16 @@
The use of relations for representing RAGs allows us to conveniently define
the notion of the \emph{dependants} of a thread using the transitive closure
- operation for relations. This gives
+ operation for relations, written ~@{term "trancl DUMMY"}. This gives
\begin{isabelle}\ \ \ \ \ %%%
- @{thm cs_dependents_def}
+ @{thm cs_dependants_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 being released (in the picture above this means the dependants
+ 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
@@ -648,7 +703,7 @@
assumption on how different resources can be locked and released relative to each
other. In our model it is possible that critical sections overlap. This is in
contrast to Sha et al \cite{Sha90} who require that critical sections are
- properly nested.
+ properly nested (recall Fig.~\ref{overlap}).
A valid state of PIP can then be conveniently be defined as follows:
@@ -785,7 +840,15 @@
finite bound does not guarantee absence of indefinite Priority
Inversion. For this we further have to assume that every thread
gives up its resources after a finite amount of time. We found that
- this assumption is awkward to formalise in our model. Therefore we
+ this assumption is awkward to formalise in our model. There are mainly
+ two reasons: First, we do not specify what ``running'' the code of a
+ thread means, for example by giving an operational semantics for
+ machine instructions. Therefore we cannot characterise what are ``good''
+ programs that contain for every looking request also a corresponding
+ unlocking request for a resource. (HERE)
+
+
+ Therefore we
leave it out and let the programmer assume the responsibility to
program threads in such a benign manner (in addition to causing no
circularity in the RAG). In this detail, we do not
@@ -941,8 +1004,8 @@
% @ {thm [display] not_thread_holdents}
%\item When the number of @{text "P"} equals the number of @{text "V"}, the relevant
% thread does not hold any critical resource, therefore no thread can depend on it
- % (@{text "count_eq_dependents"}):
- % @ {thm [display] count_eq_dependents}
+ % (@{text "count_eq_dependants"}):
+ % @ {thm [display] count_eq_dependants}
%\end{enumerate}
%The reason that only threads which already held some resoures
@@ -1257,7 +1320,7 @@
@{text "then"} @{thm (concl) eq_up}.
\end{tabular}
\end{isabelle}
-
+
\noindent
This lemma states that if an intermediate @{term cp}-value does not change, then
the procedure can also stop, because none of its dependent threads will
@@ -1269,7 +1332,13 @@
be recalculated for an event. This information is provided by the lemmas we proved.
We confirmed that our observations translate into practice by implementing
our version of PIP on top of PINTOS, a small operating system written in C and used for teaching at
- Stanford University \cite{PINTOS}. To implement PIP, we only need to modify the kernel
+ Stanford University \cite{PINTOS}. An alternative would have been the small Xv6 operating
+ system used for teaching at MIT \cite{Xv6link,Xv6}. However this operating system implements
+ a simple round robin scheduler that lacks stubs for dealing with priorities. This
+ is inconvenient for our purposes.
+
+
+ To implement PIP in PINTOS, we only need to modify the kernel
functions corresponding to the events in our formal model. The events translate to the following
function interface in PINTOS:
@@ -1450,7 +1519,15 @@
the next thread which takes over a lock is irrelevant for the correctness
of PIP. Moreover, we eliminated a crucial restriction present in
the proof of Sha et al.: they require that critical sections nest properly,
- whereas our scheduler allows critical sections to overlap.
+ whereas our scheduler allows critical sections to overlap. What we
+ are not able to do is to mechanically ``synthesise'' an actual implementation
+ from our formalisation. To do so for C-code seems quite hard and is beyond
+ current technology available for Isabelle. Also our proof-method based
+ on events is not ``computational'' in the sense of having a concrete
+ algorithm behind it: our formalisation is really more about the
+ specification of PIP and ensuring that it has the desired properties
+ (the informal specification by Sha et al.~did not).
+
PIP is a scheduling algorithm for single-processor systems. We are
now living in a multi-processor world. Priority Inversion certainly
--- a/Journal/document/root.bib Wed Mar 12 10:08:20 2014 +0000
+++ b/Journal/document/root.bib Tue May 06 14:36:40 2014 +0100
@@ -1,3 +1,19 @@
+
+
+@TechReport{Xv6,
+ author = {R.~Cox and F.~Kaashoek and R.~Morris},
+ title = {{X}v6: {A} {S}imple, {U}nix-like {T}eaching {O}perating {S}ystem},
+ institution = {MIT},
+ year = {2012}
+}
+
+@Misc{Xv6link,
+ author = {R.~Cox and F.~Kaashoek and R.~Morris},
+ title = {{Xv6}},
+ note = {\url{http://pdos.csail.mit.edu/6.828/2012/xv6.html}},
+}
+
+
@inproceedings{ThreadX,
author = {Y.~Wang and M.~Saksena},
title = {{S}cheduling {F}ixed-{P}riority {T}asks with {P}reemption {T}hreshold},
@@ -62,7 +78,7 @@
}
@phdthesis{Brandenburg11,
- Author = {Bj\"{o}rn B. Brandenburg},
+ Author = {B.~B.~Brandenburg},
School = {The University of North Carolina at Chapel Hill},
Title = {{S}cheduling and {L}ocking in
{M}ultiprocessor {R}eal-{T}ime {O}perating {S}ystems},
--- a/Journal/document/root.tex Wed Mar 12 10:08:20 2014 +0000
+++ b/Journal/document/root.tex Tue May 06 14:36:40 2014 +0100
@@ -18,6 +18,7 @@
\usepackage{url}
\usepackage{color}
\usepackage{courier}
+\usetikzlibrary{patterns}
\usepackage{listings}
\lstset{language=C,
numbers=left,
@@ -49,7 +50,10 @@
\begin{document}
\renewcommand{\thefootnote}{$\star$}
-\footnotetext[1]{This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}.}
+\footnotetext[1]{This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}.
+Compared with that paper we give an actual implementation of our formalised scheduling
+algorithm in C and the operating system PINTOS. Our implementation follows closely all results
+we proved about optimisations.}
\renewcommand{\thefootnote}{\arabic{footnote}}
\title{Priority Inheritance Protocol Proved Correct}
@@ -73,11 +77,11 @@
a solution proposed earlier. We also generalise the original informal proof to the
practically relevant case where critical sections can
overlap. Our formalisation in Isabelle/HOL not just
-uncovers facts not mentioned in the literature, but also shows how to
-efficiently implement this protocol. Earlier correct implementations
+uncovers facts not mentioned in the literature, but also helps with
+implementing efficiently this protocol. Earlier correct implementations
were criticised as too inefficient. Our formalisation is based on
Paulson's inductive approach to verifying protocols; our implementation
-builds on top of the small PINTOS operating system.\medskip
+builds on top of the small PINTOS operating system used for teaching.\medskip
%{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof,
%real-time systems, Isabelle/HOL
--- a/PrioG.thy Wed Mar 12 10:08:20 2014 +0000
+++ b/PrioG.thy Tue May 06 14:36:40 2014 +0100
@@ -375,15 +375,15 @@
by auto
-lemma birthtime_lt: "th \<in> threads s \<Longrightarrow> birthtime th s < length s"
+lemma last_set_lt: "th \<in> threads s \<Longrightarrow> last_set th s < length s"
apply (induct s, auto)
by (case_tac a, auto split:if_splits)
-lemma birthtime_unique:
- "\<lbrakk>birthtime th1 s = birthtime th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk>
+lemma last_set_unique:
+ "\<lbrakk>last_set th1 s = last_set th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk>
\<Longrightarrow> th1 = th2"
apply (induct s, auto)
- by (case_tac a, auto split:if_splits dest:birthtime_lt)
+ by (case_tac a, auto split:if_splits dest:last_set_lt)
lemma preced_unique :
assumes pcd_eq: "preced th1 s = preced th2 s"
@@ -391,8 +391,8 @@
and th_in2: " th2 \<in> threads s"
shows "th1 = th2"
proof -
- from pcd_eq have "birthtime th1 s = birthtime th2 s" by (simp add:preced_def)
- from birthtime_unique [OF this th_in1 th_in2]
+ from pcd_eq have "last_set th1 s = last_set th2 s" by (simp add:preced_def)
+ from last_set_unique [OF this th_in1 th_in2]
show ?thesis .
qed
@@ -2100,8 +2100,8 @@
proof -
from runing_1 and runing_2 have "cp s th1 = cp s th2"
by (unfold runing_def, simp)
- hence eq_max: "Max ((\<lambda>th. preced th s) ` ({th1} \<union> dependents (wq s) th1)) =
- Max ((\<lambda>th. preced th s) ` ({th2} \<union> dependents (wq s) th2))"
+ hence eq_max: "Max ((\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)) =
+ Max ((\<lambda>th. preced th s) ` ({th2} \<union> dependants (wq s) th2))"
(is "Max (?f ` ?A) = Max (?f ` ?B)")
by (unfold cp_eq_cpreced cpreced_def)
obtain th1' where th1_in: "th1' \<in> ?A" and eq_f_th1: "?f th1' = Max (?f ` ?A)"
@@ -2110,7 +2110,7 @@
proof -
have "finite ?A"
proof -
- have "finite (dependents (wq s) th1)"
+ have "finite (dependants (wq s) th1)"
proof-
have "finite {th'. (Th th', Th th1) \<in> (depend (wq s))\<^sup>+}"
proof -
@@ -2128,7 +2128,7 @@
qed
ultimately show ?thesis by (auto intro:finite_subset)
qed
- thus ?thesis by (simp add:cs_dependents_def)
+ thus ?thesis by (simp add:cs_dependants_def)
qed
thus ?thesis by simp
qed
@@ -2149,7 +2149,7 @@
proof -
have "finite ?B"
proof -
- have "finite (dependents (wq s) th2)"
+ have "finite (dependants (wq s) th2)"
proof-
have "finite {th'. (Th th', Th th2) \<in> (depend (wq s))\<^sup>+}"
proof -
@@ -2167,7 +2167,7 @@
qed
ultimately show ?thesis by (auto intro:finite_subset)
qed
- thus ?thesis by (simp add:cs_dependents_def)
+ thus ?thesis by (simp add:cs_dependants_def)
qed
thus ?thesis by simp
qed
@@ -2186,12 +2186,12 @@
have eq_preced: "preced th1' s = preced th2' s" by auto
hence eq_th12: "th1' = th2'"
proof (rule preced_unique)
- from th1_in have "th1' = th1 \<or> (th1' \<in> dependents (wq s) th1)" by simp
+ from th1_in have "th1' = th1 \<or> (th1' \<in> dependants (wq s) th1)" by simp
thus "th1' \<in> threads s"
proof
- assume "th1' \<in> dependents (wq s) th1"
+ assume "th1' \<in> dependants (wq s) th1"
hence "(Th th1') \<in> Domain ((depend s)^+)"
- apply (unfold cs_dependents_def cs_depend_def s_depend_def)
+ apply (unfold cs_dependants_def cs_depend_def s_depend_def)
by (auto simp:Domain_def)
hence "(Th th1') \<in> Domain (depend s)" by (simp add:trancl_domain)
from dm_depend_threads[OF vt this] show ?thesis .
@@ -2201,12 +2201,12 @@
by (unfold runing_def readys_def, auto)
qed
next
- from th2_in have "th2' = th2 \<or> (th2' \<in> dependents (wq s) th2)" by simp
+ from th2_in have "th2' = th2 \<or> (th2' \<in> dependants (wq s) th2)" by simp
thus "th2' \<in> threads s"
proof
- assume "th2' \<in> dependents (wq s) th2"
+ assume "th2' \<in> dependants (wq s) th2"
hence "(Th th2') \<in> Domain ((depend s)^+)"
- apply (unfold cs_dependents_def cs_depend_def s_depend_def)
+ apply (unfold cs_dependants_def cs_depend_def s_depend_def)
by (auto simp:Domain_def)
hence "(Th th2') \<in> Domain (depend s)" by (simp add:trancl_domain)
from dm_depend_threads[OF vt this] show ?thesis .
@@ -2216,21 +2216,21 @@
by (unfold runing_def readys_def, auto)
qed
qed
- from th1_in have "th1' = th1 \<or> th1' \<in> dependents (wq s) th1" by simp
+ from th1_in have "th1' = th1 \<or> th1' \<in> dependants (wq s) th1" by simp
thus ?thesis
proof
assume eq_th': "th1' = th1"
- from th2_in have "th2' = th2 \<or> th2' \<in> dependents (wq s) th2" by simp
+ from th2_in have "th2' = th2 \<or> th2' \<in> dependants (wq s) th2" by simp
thus ?thesis
proof
assume "th2' = th2" thus ?thesis using eq_th' eq_th12 by simp
next
- assume "th2' \<in> dependents (wq s) th2"
- with eq_th12 eq_th' have "th1 \<in> dependents (wq s) th2" by simp
+ assume "th2' \<in> dependants (wq s) th2"
+ with eq_th12 eq_th' have "th1 \<in> dependants (wq s) th2" by simp
hence "(Th th1, Th th2) \<in> (depend s)^+"
- by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
+ by (unfold cs_dependants_def s_depend_def cs_depend_def, simp)
hence "Th th1 \<in> Domain ((depend s)^+)"
- apply (unfold cs_dependents_def cs_depend_def s_depend_def)
+ apply (unfold cs_dependants_def cs_depend_def s_depend_def)
by (auto simp:Domain_def)
hence "Th th1 \<in> Domain (depend s)" by (simp add:trancl_domain)
then obtain n where d: "(Th th1, n) \<in> depend s" by (auto simp:Domain_def)
@@ -2243,16 +2243,16 @@
thus ?thesis by simp
qed
next
- assume th1'_in: "th1' \<in> dependents (wq s) th1"
- from th2_in have "th2' = th2 \<or> th2' \<in> dependents (wq s) th2" by simp
+ assume th1'_in: "th1' \<in> dependants (wq s) th1"
+ from th2_in have "th2' = th2 \<or> th2' \<in> dependants (wq s) th2" by simp
thus ?thesis
proof
assume "th2' = th2"
- with th1'_in eq_th12 have "th2 \<in> dependents (wq s) th1" by simp
+ with th1'_in eq_th12 have "th2 \<in> dependants (wq s) th1" by simp
hence "(Th th2, Th th1) \<in> (depend s)^+"
- by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
+ by (unfold cs_dependants_def s_depend_def cs_depend_def, simp)
hence "Th th2 \<in> Domain ((depend s)^+)"
- apply (unfold cs_dependents_def cs_depend_def s_depend_def)
+ apply (unfold cs_dependants_def cs_depend_def s_depend_def)
by (auto simp:Domain_def)
hence "Th th2 \<in> Domain (depend s)" by (simp add:trancl_domain)
then obtain n where d: "(Th th2, n) \<in> depend s" by (auto simp:Domain_def)
@@ -2264,12 +2264,12 @@
by (auto simp:eq_waiting)
thus ?thesis by simp
next
- assume "th2' \<in> dependents (wq s) th2"
- with eq_th12 have "th1' \<in> dependents (wq s) th2" by simp
+ assume "th2' \<in> dependants (wq s) th2"
+ with eq_th12 have "th1' \<in> dependants (wq s) th2" by simp
hence h1: "(Th th1', Th th2) \<in> (depend s)^+"
- by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
+ by (unfold cs_dependants_def s_depend_def cs_depend_def, simp)
from th1'_in have h2: "(Th th1', Th th1) \<in> (depend s)^+"
- by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
+ by (unfold cs_dependants_def s_depend_def cs_depend_def, simp)
show ?thesis
proof(rule dchain_unique[OF vt h1 _ h2, symmetric])
from runing_1 show "th1 \<in> readys s" by (simp add:runing_def)
@@ -2415,10 +2415,10 @@
"depend (wq s) = depend s"
by (unfold cs_depend_def s_depend_def, auto)
-lemma count_eq_dependents:
+lemma count_eq_dependants:
assumes vt: "vt s"
and eq_pv: "cntP s th = cntV s th"
- shows "dependents (wq s) th = {}"
+ shows "dependants (wq s) th = {}"
proof -
from cnp_cnv_cncs[OF vt] and eq_pv
have "cntCS s th = 0"
@@ -2429,9 +2429,9 @@
by (simp add:holdents_test)
qed
ultimately have h: "{cs. (Cs cs, Th th) \<in> depend s} = {}"
- by (unfold cntCS_def holdents_test cs_dependents_def, auto)
+ by (unfold cntCS_def holdents_test cs_dependants_def, auto)
show ?thesis
- proof(unfold cs_dependents_def)
+ proof(unfold cs_dependants_def)
{ assume "{th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+} \<noteq> {}"
then obtain th' where "(Th th', Th th) \<in> (depend (wq s))\<^sup>+" by auto
hence "False"
@@ -2448,10 +2448,10 @@
qed
qed
-lemma dependents_threads:
+lemma dependants_threads:
fixes s th
assumes vt: "vt s"
- shows "dependents (wq s) th \<subseteq> threads s"
+ shows "dependants (wq s) th \<subseteq> threads s"
proof
{ fix th th'
assume h: "th \<in> {th'a. (Th th'a, Th th') \<in> (depend (wq s))\<^sup>+}"
@@ -2466,9 +2466,9 @@
have "th \<in> threads s" .
} note hh = this
fix th1
- assume "th1 \<in> dependents (wq s) th"
+ assume "th1 \<in> dependants (wq s) th"
hence "th1 \<in> {th'a. (Th th'a, Th th) \<in> (depend (wq s))\<^sup>+}"
- by (unfold cs_dependents_def, simp)
+ by (unfold cs_dependants_def, simp)
from hh [OF this] show "th1 \<in> threads s" .
qed
@@ -2495,7 +2495,7 @@
assumes vt: "vt s"
and th_in: "th \<in> threads s"
shows "cp s th \<le> Max ((\<lambda> th. (preced th s)) ` threads s)"
-proof(unfold cp_eq_cpreced cpreced_def cs_dependents_def)
+proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def)
show "Max ((\<lambda>th. preced th s) ` ({th} \<union> {th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+}))
\<le> Max ((\<lambda>th. preced th s) ` threads s)"
(is "Max (?f ` ?A) \<le> Max (?f ` ?B)")
@@ -2518,9 +2518,9 @@
assumes vt: "vt s"
shows "preced th s \<le> cp s th"
proof(unfold cp_eq_cpreced preced_def cpreced_def, simp)
- show "Prc (original_priority th s) (birthtime th s)
- \<le> Max (insert (Prc (original_priority th s) (birthtime th s))
- ((\<lambda>th. Prc (original_priority th s) (birthtime th s)) ` dependents (wq s) th))"
+ show "Prc (priority th s) (last_set th s)
+ \<le> Max (insert (Prc (priority th s) (last_set th s))
+ ((\<lambda>th. Prc (priority th s) (last_set th s)) ` dependants (wq s) th))"
(is "?l \<le> Max (insert ?l ?A)")
proof(cases "?A = {}")
case False
@@ -2544,7 +2544,7 @@
qed
ultimately show ?thesis by (auto intro:finite_subset)
qed
- thus ?thesis by (simp add:cs_dependents_def)
+ thus ?thesis by (simp add:cs_dependants_def)
qed
thus ?thesis by simp
qed
@@ -2629,28 +2629,28 @@
and tm_chain:"(Th tm, Th th') \<in> (depend s)\<^sup>+" by auto
have "cp s th' = ?f tm"
proof(subst cp_eq_cpreced, subst cpreced_def, rule Max_eqI)
- from dependents_threads[OF vt] finite_threads[OF vt]
- show "finite ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th'))"
+ from dependants_threads[OF vt] finite_threads[OF vt]
+ show "finite ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th'))"
by (auto intro:finite_subset)
next
- fix p assume p_in: "p \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')"
+ fix p assume p_in: "p \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')"
from tm_max have " preced tm s = Max ((\<lambda>th. preced th s) ` threads s)" .
moreover have "p \<le> \<dots>"
proof(rule Max_ge)
from finite_threads[OF vt]
show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
next
- from p_in and th'_in and dependents_threads[OF vt, of th']
+ from p_in and th'_in and dependants_threads[OF vt, of th']
show "p \<in> (\<lambda>th. preced th s) ` threads s"
by (auto simp:readys_def)
qed
ultimately show "p \<le> preced tm s" by auto
next
- show "preced tm s \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')"
+ show "preced tm s \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')"
proof -
from tm_chain
- have "tm \<in> dependents (wq s) th'"
- by (unfold cs_dependents_def s_depend_def cs_depend_def, auto)
+ have "tm \<in> dependants (wq s) th'"
+ by (unfold cs_dependants_def s_depend_def cs_depend_def, auto)
thus ?thesis by auto
qed
qed
@@ -2667,12 +2667,12 @@
apply (unfold cp_eq_cpreced cpreced_def)
apply (rule Max_mono)
proof -
- from dependents_threads [OF vt, of th1] th1_in
- show "(\<lambda>th. preced th s) ` ({th1} \<union> dependents (wq s) th1) \<subseteq>
+ from dependants_threads [OF vt, of th1] th1_in
+ show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<subseteq>
(\<lambda>th. preced th s) ` threads s"
by (auto simp:readys_def)
next
- show "(\<lambda>th. preced th s) ` ({th1} \<union> dependents (wq s) th1) \<noteq> {}" by simp
+ show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}" by simp
next
from finite_threads[OF vt]
show " finite ((\<lambda>th. preced th s) ` threads s)" by simp
@@ -2691,14 +2691,14 @@
have cp_eq_p: "cp s tm = preced tm s"
proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI)
fix y
- assume hy: "y \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependents (wq s) tm)"
+ assume hy: "y \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm)"
show "y \<le> preced tm s"
proof -
{ fix y'
- assume hy' : "y' \<in> ((\<lambda>th. preced th s) ` dependents (wq s) tm)"
+ assume hy' : "y' \<in> ((\<lambda>th. preced th s) ` dependants (wq s) tm)"
have "y' \<le> preced tm s"
proof(unfold tm_max, rule Max_ge)
- from hy' dependents_threads[OF vt, of tm]
+ from hy' dependants_threads[OF vt, of tm]
show "y' \<in> (\<lambda>th. preced th s) ` threads s" by auto
next
from finite_threads[OF vt]
@@ -2707,11 +2707,11 @@
} with hy show ?thesis by auto
qed
next
- from dependents_threads[OF vt, of tm] finite_threads[OF vt]
- show "finite ((\<lambda>th. preced th s) ` ({tm} \<union> dependents (wq s) tm))"
+ from dependants_threads[OF vt, of tm] finite_threads[OF vt]
+ show "finite ((\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm))"
by (auto intro:finite_subset)
next
- show "preced tm s \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependents (wq s) tm)"
+ show "preced tm s \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm)"
by simp
qed
moreover have "Max (cp s ` readys s) = cp s tm"
@@ -2731,11 +2731,11 @@
from finite_threads[OF vt]
show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
next
- show "(\<lambda>th. preced th s) ` ({th1} \<union> dependents (wq s) th1) \<noteq> {}"
+ show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}"
by simp
next
- from dependents_threads[OF vt, of th1] th1_readys
- show "(\<lambda>th. preced th s) ` ({th1} \<union> dependents (wq s) th1)
+ from dependants_threads[OF vt, of th1] th1_readys
+ show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)
\<subseteq> (\<lambda>th. preced th s) ` threads s"
by (auto simp:readys_def)
qed
--- a/PrioGDef.thy Wed Mar 12 10:08:20 2014 +0000
+++ b/PrioGDef.thy Tue May 06 14:36:40 2014 +0100
@@ -68,38 +68,38 @@
Functions such as @{text "threads"}, which extract information out of system states, are called
{\em observing functions}. A series of observing functions will be defined in the sequel in order to
model the protocol.
- Observing function @{text "original_priority"} calculates
+ Observing function @{text "priority"} calculates
the {\em original priority} of thread @{text "th"} in state @{text "s"}, expressed as
- : @{text "original_priority th s" }. The {\em original priority} is the priority
+ : @{text "priority th s" }. The {\em original priority} is the priority
assigned to a thread when it is created or when it is reset by system call
@{text "Set thread priority"}.
*}
-fun original_priority :: "thread \<Rightarrow> state \<Rightarrow> priority"
+fun priority :: "thread \<Rightarrow> state \<Rightarrow> priority"
where
-- {* @{text "0"} is assigned to threads which have never been created: *}
- "original_priority thread [] = 0" |
- "original_priority thread (Create thread' prio#s) =
- (if thread' = thread then prio else original_priority thread s)" |
- "original_priority thread (Set thread' prio#s) =
- (if thread' = thread then prio else original_priority thread s)" |
- "original_priority thread (e#s) = original_priority thread s"
+ "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"
text {*
\noindent
In the following,
- @{text "birthtime th s"} is the time when thread @{text "th"} is created,
+ @{text "last_set th s"} is the time when thread @{text "th"} is created,
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 birthtime :: "thread \<Rightarrow> state \<Rightarrow> nat"
+fun last_set :: "thread \<Rightarrow> state \<Rightarrow> nat"
where
- "birthtime thread [] = 0" |
- "birthtime thread ((Create thread' prio)#s) =
- (if (thread = thread') then length s else birthtime thread s)" |
- "birthtime thread ((Set thread' prio)#s) =
- (if (thread = thread') then length s else birthtime thread s)" |
- "birthtime thread (e#s) = birthtime thread s"
+ "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"
text {*
\noindent
@@ -110,7 +110,7 @@
This explains the following definition:
*}
definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
- where "preced thread s \<equiv> Prc (original_priority thread s) (birthtime thread s)"
+ where "preced thread s \<equiv> Prc (priority thread s) (last_set thread s)"
text {*
@@ -122,7 +122,7 @@
holding :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"
waiting :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"
depend :: "'b \<Rightarrow> (node \<times> node) set"
- dependents :: "'b \<Rightarrow> thread \<Rightarrow> thread set"
+ dependants :: "'b \<Rightarrow> thread \<Rightarrow> thread set"
text {*
\noindent
@@ -162,12 +162,12 @@
{(Th th, Cs cs) | th cs. waiting wq th cs} \<union> {(Cs cs, Th th) | cs th. holding wq th cs}"
-- {*
\begin{minipage}{0.9\textwidth}
- The following @{text "dependents wq th"} represents the set of threads which are depending on
+ The following @{text "dependants wq th"} represents the set of threads which are depending on
thread @{text "th"} in Resource Allocation Graph @{text "depend wq"}:
\end{minipage}
*}
- cs_dependents_def:
- "dependents (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (depend wq)^+}"
+ cs_dependants_def:
+ "dependants (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (depend wq)^+}"
text {*
@@ -185,18 +185,18 @@
@{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 the {\em current precedence} of a thread is the precedence
- inherited from the maximum of all its dependents, i.e. the threads which are waiting
+ inherited from 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"}.
*}
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> dependents wq th)))"
+ where "cpreced wq s = (\<lambda> th. Max ((\<lambda> th. preced th s) ` ({th} \<union> dependants wq th)))"
(*<*)
lemma
cpreced_def2:
- "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependents wq th})"
+ "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants wq th})"
unfolding cpreced_def image_def
apply(rule eq_reflection)
apply(rule_tac f="Max" in arg_cong)
@@ -268,7 +268,7 @@
lemma cpreced_initial:
"cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"
apply(simp add: cpreced_def)
-apply(simp add: cs_dependents_def cs_depend_def cs_waiting_def cs_holding_def)
+apply(simp add: cs_dependants_def cs_depend_def cs_waiting_def cs_holding_def)
apply(simp add: preced_def)
done
@@ -305,7 +305,7 @@
text {* \noindent
Functions @{text "holding"}, @{text "waiting"}, @{text "depend"} and
- @{text "dependents"} still have the
+ @{text "dependants"} still have the
same meaning, but redefined so that they no longer depend on the
fictitious {\em waiting queue function}
@{text "wq"}, but on system state @{text "s"}.
@@ -317,8 +317,8 @@
"waiting (s::state) \<equiv> waiting (wq_fun (schs s))"
s_depend_abv:
"depend (s::state) \<equiv> depend (wq_fun (schs s))"
- s_dependents_abv:
- "dependents (s::state) \<equiv> dependents (wq_fun (schs s))"
+ s_dependants_abv:
+ "dependants (s::state) \<equiv> dependants (wq_fun (schs s))"
text {*
@@ -339,9 +339,9 @@
by (auto simp:s_depend_abv wq_def cs_depend_def)
lemma
- s_dependents_def:
- "dependents (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}"
- by (auto simp:s_dependents_abv wq_def cs_dependents_def)
+ s_dependants_def:
+ "dependants (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}"
+ by (auto simp:s_dependants_abv wq_def cs_dependants_def)
text {*
The following function @{text "readys"} calculates the set of ready threads. A thread is {\em ready}
Binary file journal.pdf has changed