--- a/Implementation.thy Tue Feb 09 22:30:43 2016 +0800
+++ b/Implementation.thy Fri Feb 12 12:32:57 2016 +0800
@@ -7,6 +7,113 @@
after every system call (or system operation)
*}
+section {* Recursive calculation of @{term "cp"} *}
+
+definition "cp_gen s x =
+ Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"
+
+lemma cp_gen_alt_def:
+ "cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))"
+ by (auto simp:cp_gen_def)
+
+lemma cp_gen_def_cond:
+ assumes "x = Th th"
+ shows "cp s th = cp_gen s (Th th)"
+by (unfold cp_alt_def1 cp_gen_def, simp)
+
+lemma cp_gen_over_set:
+ assumes "\<forall> x \<in> A. \<exists> th. x = Th th"
+ shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A"
+proof(rule f_image_eq)
+ fix a
+ assume "a \<in> A"
+ from assms[rule_format, OF this]
+ obtain th where eq_a: "a = Th th" by auto
+ show "cp_gen s a = (cp s \<circ> the_thread) a"
+ by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp)
+qed
+
+
+context valid_trace
+begin
+(* ddd *)
+lemma cp_gen_rec:
+ assumes "x = Th th"
+ shows "cp_gen s x = Max ({the_preced s th} \<union> (cp_gen s) ` children (tRAG s) x)"
+proof(cases "children (tRAG s) x = {}")
+ case True
+ show ?thesis
+ by (unfold True cp_gen_def subtree_children, simp add:assms)
+next
+ case False
+ hence [simp]: "children (tRAG s) x \<noteq> {}" by auto
+ note fsbttRAGs.finite_subtree[simp]
+ have [simp]: "finite (children (tRAG s) x)"
+ by (intro rev_finite_subset[OF fsbttRAGs.finite_subtree],
+ rule children_subtree)
+ { fix r x
+ have "subtree r x \<noteq> {}" by (auto simp:subtree_def)
+ } note this[simp]
+ have [simp]: "\<exists>x\<in>children (tRAG s) x. subtree (tRAG s) x \<noteq> {}"
+ proof -
+ from False obtain q where "q \<in> children (tRAG s) x" by blast
+ moreover have "subtree (tRAG s) q \<noteq> {}" by simp
+ ultimately show ?thesis by blast
+ qed
+ have h: "Max ((the_preced s \<circ> the_thread) `
+ ({x} \<union> \<Union>(subtree (tRAG s) ` children (tRAG s) x))) =
+ Max ({the_preced s th} \<union> cp_gen s ` children (tRAG s) x)"
+ (is "?L = ?R")
+ proof -
+ let "Max (?f ` (?A \<union> \<Union> (?g ` ?B)))" = ?L
+ let "Max (_ \<union> (?h ` ?B))" = ?R
+ let ?L1 = "?f ` \<Union>(?g ` ?B)"
+ have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)"
+ proof -
+ have "?L1 = ?f ` (\<Union> x \<in> ?B.(?g x))" by simp
+ also have "... = (\<Union> x \<in> ?B. ?f ` (?g x))" by auto
+ finally have "Max ?L1 = Max ..." by simp
+ also have "... = Max (Max ` (\<lambda>x. ?f ` subtree (tRAG s) x) ` ?B)"
+ by (subst Max_UNION, simp+)
+ also have "... = Max (cp_gen s ` children (tRAG s) x)"
+ by (unfold image_comp cp_gen_alt_def, simp)
+ finally show ?thesis .
+ qed
+ show ?thesis
+ proof -
+ have "?L = Max (?f ` ?A \<union> ?L1)" by simp
+ also have "... = max (the_preced s (the_thread x)) (Max ?L1)"
+ by (subst Max_Un, simp+)
+ also have "... = max (?f x) (Max (?h ` ?B))"
+ by (unfold eq_Max_L1, simp)
+ also have "... =?R"
+ by (rule max_Max_eq, (simp)+, unfold assms, simp)
+ finally show ?thesis .
+ qed
+ qed thus ?thesis
+ by (fold h subtree_children, unfold cp_gen_def, simp)
+qed
+
+lemma cp_rec:
+ "cp s th = Max ({the_preced s th} \<union>
+ (cp s o the_thread) ` children (tRAG s) (Th th))"
+proof -
+ have "Th th = Th th" by simp
+ note h = cp_gen_def_cond[OF this] cp_gen_rec[OF this]
+ show ?thesis
+ proof -
+ have "cp_gen s ` children (tRAG s) (Th th) =
+ (cp s \<circ> the_thread) ` children (tRAG s) (Th th)"
+ proof(rule cp_gen_over_set)
+ show " \<forall>x\<in>children (tRAG s) (Th th). \<exists>th. x = Th th"
+ by (unfold tRAG_alt_def, auto simp:children_def)
+ qed
+ thus ?thesis by (subst (1) h(1), unfold h(2), simp)
+ qed
+qed
+
+end
+
text {* (* ddd *)
One beauty of our modelling is that we follow the definitional extension tradition of HOL.
The benefit of such a concise and miniature model is that large number of intuitively
--- a/PIPBasics.thy Tue Feb 09 22:30:43 2016 +0800
+++ b/PIPBasics.thy Fri Feb 12 12:32:57 2016 +0800
@@ -167,28 +167,6 @@
done
text {*
- The following lemmas is an alternative definition of @{term cp},
- which is based on the notion of subtrees in @{term RAG} and
- is handy to use once the abstract theory of {\em relational graph}
- (and specifically {\em relational tree} and {\em relational forest})
- are in place.
-*}
-lemma cp_alt_def:
- "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 (wq 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_def s_RAG_def subtree_def)
- thus ?thesis by simp
- qed
- thus ?thesis by (unfold cp_eq cpreced_def, fold the_preced_def, simp)
-qed
-
-text {*
The following @{text "children_RAG_alt_def"} relates
@{term children} in @{term RAG} to the notion of @{term holding}.
It is a technical lemmas used to prove the two following lemmas.
@@ -593,6 +571,40 @@
{th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")
by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)
+text {*
+ The following lemmas is an alternative definition of @{term cp},
+ which is based on the notion of subtrees in @{term RAG} and
+ is handy to use once the abstract theory of {\em relational graph}
+ (and specifically {\em relational tree} and {\em relational forest})
+ are in place.
+*}
+lemma cp_alt_def:
+ "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 (wq 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_def s_RAG_def subtree_def)
+ thus ?thesis by simp
+ qed
+ thus ?thesis by (unfold cp_eq cpreced_def, fold the_preced_def, simp)
+qed
+
+text {*
+ The following is another definition of @{term cp}.
+*}
+lemma cp_alt_def1:
+ "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"
+proof -
+ have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =
+ ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"
+ by auto
+ thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)
+qed
+
lemma RAG_tRAG_transfer:
assumes "RAG s' = RAG s \<union> {(Th th, Cs cs)}"
and "(Cs cs, Th th'') \<in> RAG s"
@@ -931,6 +943,19 @@
ultimately show ?thesis by simp
qed
qed
+
+text {*
+ The following two lemmas are fundamental, because they assure
+ that the numbers of both living and ready threads are finite.
+*}
+
+lemma finite_threads:
+ shows "finite (threads s)"
+ using vt by (induct) (auto elim: step.cases)
+
+lemma finite_readys: "finite (readys s)"
+ using finite_threads readys_threads rev_finite_subset by blast
+
end
text {*
@@ -965,7 +990,7 @@
section {* Waiting queues are distinct *}
text {*
- This section proofs that every waiting queue in the system
+ This section proves that every waiting queue in the system
is distinct, given in lemma @{text wq_distinct}.
The proof is split into the locales for events (or operations),
@@ -1478,19 +1503,29 @@
end
-section {* The change of @{term RAG} *}
+section {* The formation of @{term RAG} *}
text {*
The whole of PIP resides on the understanding of the formation
- of @{term RAG}. In this section, we are going to investigate how
- @{term RAG} is changed with the execution of every event (or operation).
- The effect of every event on @{text RAG} is derived in its respective
+ of @{term RAG}. We are going to show that @{term RAG}
+ forms a finite branching forest. The formalization is divided
+ into a series of subsections.
+*}
+
+subsection {* The change of @{term RAG} with each step of execution *}
+
+text {*
+ The very essence to prove that @{term RAG} has a certain property is to
+ show that this property is preserved as an invariant by the execution
+ of the system, and the basis for such kind of invariant proofs is to
+ show how @{term RAG} is changed with the execution of every execution step
+ (or event, or system operation). In this subsection,
+ the effect of every event on @{text RAG} is derived in its respective
locale named @{text "RAG_es"} with all lemmas before auxiliary.
- The derivation of these @{text "RAG_es"}s forms the very basis
- to show the well-formedness of @{term RAG},
+ These derived @{text "RAG_es"}s constitute the foundation
+ to show the various well-formed properties of @{term RAG},
for example, @{term RAG} is finite, acyclic, and single-valued, etc.
-
*}
text {*
@@ -2270,7 +2305,7 @@
end
-section {* RAG is finite *}
+subsection {* RAG is finite *}
context valid_trace_v
begin
@@ -2338,8 +2373,6 @@
qed
end
-section {* RAG is acyclic *}
-
subsection {* Uniqueness of waiting *}
text {*
@@ -2721,6 +2754,9 @@
end
+
+subsection {* RAG is acyclic *}
+
context valid_trace
begin
@@ -2793,7 +2829,7 @@
end
-section {* RAG is single-valued *}
+subsection {* RAG is single-valued *}
text {*
The proof that @{term RAG} is single-valued makes use of
@@ -2813,7 +2849,7 @@
end
-section {* RAG is well-founded *}
+subsection {* RAG is well-founded *}
text {*
In this section, it is proved that both @{term RAG} and
@@ -2844,7 +2880,7 @@
end
-section {* RAG forms a finite-branching forest (or tree) *}
+subsection {* RAG forms a finite-branching forest (or tree) *}
text {*
With all the well-formedness proofs about @{term RAG} in place,
@@ -2876,8 +2912,7 @@
qed
qed
-
-section {* Derived properties for sub-graphs of RAG *}
+subsection {* Derived properties for sub-graphs of RAG *}
context valid_trace
begin
@@ -2952,16 +2987,20 @@
section {* Chain to readys *}
text {*
- In this section, a more complete view of @{term RAG} and @{term threads}
- are given.
+ In this section, based on the just derived
+ properties about the shape of @{term RAG},
+ a more complete view of the relationship
+ between threads is established.
*}
context valid_trace
begin
text {*
- The first lemma is technical, which says out of any node in the domain
- of @{term RAG}, there is a path leading to a ready thread.
+ The first lemma is technical, which says out of any node
+ in the domain of @{term RAG},
+ (no matter whether it is thread node or resource node)
+ there is a path leading to a ready thread.
*}
lemma chain_building:
@@ -3276,18 +3315,26 @@
end
-(* ccc *)
section {* Relating @{term cp} and @{term the_preced} and @{term preced} *}
+text {*
+ @{term cp} of a thread is defined to be the maximum of
+ the @{term preced}-values (precedences) of all threads in
+ its subtree given by @{term RAG}. Therefore, there exits
+ a relationship between @{term cp} and @{term preced} (and
+ also its variation @{term "the_preced"}) to be explored,
+ and this is the target of this section.
+*}
+
context valid_trace
begin
-lemma finite_threads:
- shows "finite (threads s)"
- using vt by (induct) (auto elim: step.cases)
-
-lemma finite_readys: "finite (readys s)"
- using finite_threads readys_threads rev_finite_subset by blast
+text {*
+ Since @{term cp} is the maximum of all @{term preced}s in its subtree,
+ which includes itself, it is not difficult to show
+ that the one thread's precedence is less or equal to its
+ @{text cp}-value:
+*}
lemma le_cp:
shows "preced th s \<le> cp s th"
@@ -3299,6 +3346,13 @@
by (simp add: subtree_def the_preced_def)
qed
+text {*
+ Since @{term cp} is the maximum precedence of its subtree,
+ and the subtree is only a subset of the set of all threads,
+ it can be shown that @{text cp} is less or equal to the maximum of
+ all threads:
+*}
+
lemma cp_le:
assumes th_in: "th \<in> threads s"
shows "cp s th \<le> Max (the_preced s ` threads s)"
@@ -3314,6 +3368,21 @@
node.inject(1) rtranclD subsetI subtree_def trancl_domain)
qed
+text {*
+ Since the @{term cp}-value of each individual thread is less or equal to the
+ maximum precedence value of all threads (shown in lemma @{thm cp_le}),
+ it is easy to derive further that maximum @{term "cp"}-value of
+ all threads is also less or equal to the latter.
+
+ On the other hand, since the precedence value of each individual
+ thread is less of equal to its own @{term cp}-value (shown in lemma @{thm le_cp}),
+ it is easy to show that the maximum of the former is less or equal to the
+ maximum of the latter.
+
+ By combining these two perspectives, we get the following equality
+ between the two maximums:
+*}
+
lemma max_cp_eq:
shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)"
(is "?L = ?R")
@@ -3334,17 +3403,21 @@
qed
text {* (* ddd *) \noindent
- Since the current precedence of the threads in ready queue will always be boosted,
- there must be one inside it has the maximum precedence of the whole system.
+ According to @{thm threads_alt_def} and @{thm readys_subtree_disjoint} ,
+ the set of @{term threads} can be partitioned into subtrees of the
+ threads in @{term readys}, and also because @{term cp}-value of a thread is
+ the maximum precedence of its own subtree, by applying
+ the absorbing property of @{term Max} (lemma @{thm Max_UNION})
+ over the union of subtrees, the following equation can be derived:
*}
-lemma max_cp_readys_threads:
- shows "Max (cp s ` readys s) = Max (cp s ` threads s)" (is "?L = ?R")
+
+lemma max_cp_readys_max_preced:
+ shows "Max (cp s ` readys s) = Max (the_preced s ` threads s)" (is "?L = ?R")
proof(cases "readys s = {}")
case False
- have "?R = Max (the_preced s ` threads s)" by (unfold max_cp_eq, simp)
- also have "... =
- Max (the_preced s ` (\<Union>th\<in>readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)}))"
- by (unfold threads_alt_def, simp)
+ have "?R =
+ Max (the_preced s ` (\<Union>th\<in>readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)}))"
+ by (simp add: threads_alt_def)
also have "... =
Max ((\<Union>th\<in>readys s. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}))"
by (unfold image_UN, simp)
@@ -3355,9 +3428,10 @@
{th'. Th th' \<in> subtree (RAG s) (Th x)}) ` readys s. finite M"
using finite_subtree_threads by auto
qed (auto simp:False subtree_def finite_readys)
- also have "... =
- Max ((Max \<circ> (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})) ` readys s)"
- by (unfold image_comp, simp)
+ also have "... =
+ Max ((Max \<circ> (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})) `
+ readys s)"
+ by (simp add: image_comp)
also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)")
proof -
have "(?f ` ?A) = (?g ` ?A)"
@@ -3372,10 +3446,36 @@
finally show ?thesis by simp
qed (auto simp:threads_alt_def)
+text {*
+ The following lemma is simply a corollary of @{thm max_cp_readys_max_preced}
+ and @{thm max_cp_eq}:
+*}
+lemma max_cp_readys_threads:
+ shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
+ using max_cp_readys_max_preced max_cp_eq by auto
+
end
+
section {* Relating @{term cntP}, @{term cntV}, @{term cntCS} and @{term pvD} *}
+text {*
+ As explained in the section where @{term "cntP"},
+ @{term "cntV"} and @{term "cntCS"} are defined,
+ we need to establish a equation (in lemma @{text "cnp_cnv_cncs"})
+ so that the last can be calculated out of the first two.
+
+ While the calculation of @{term "cntV"} and @{term "cntCS"}
+ are relatively simple, the calculation of @{term "cntCS"} and
+ @{term "pvD"} are complicated, because their definitions
+ involve a number of other functions such as @{term holdents}, @{term readys},
+ and @{term threads}. To prove @{text "cnp_cnv_cncs"},
+ we need to investigate how the values of these functions
+ are changed with the execution of each kind of system operation.
+ Following conventions, such investigation are divided into
+ locales corresponding to system operations.
+*}
+
context valid_trace_p_w
begin
@@ -4633,6 +4733,10 @@
context valid_trace
begin
+text {*
+ The following two lemmas are purely technical, which says
+ a non-living thread can not hold any resource.
+*}
lemma not_thread_holdents:
assumes not_in: "th \<notin> threads s"
shows "holdents s th = {}"
@@ -4654,6 +4758,14 @@
using not_thread_holdents[OF assms]
by (simp add:cntCS_def)
+text {*
+ Starting from the following @{text cnp_cnv_eq}, all
+ lemmas in this section concern the meaning of
+ condition @{prop "cntP s th = cntV s th"}, i.e.
+ when the numbers of resource requesting and resource releasing
+ are equal.
+*}
+
lemma cnp_cnv_eq:
assumes "th \<notin> threads s"
shows "cntP s th = cntV s th"
@@ -4699,6 +4811,11 @@
show False by simp
qed
+lemma count_eq_RAG_plus_Th:
+ assumes "cntP s th = cntV s th"
+ shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}"
+ using count_eq_RAG_plus[OF assms] by auto
+
lemma eq_pv_dependants:
assumes eq_pv: "cntP s th = cntV s th"
shows "dependants s th = {}"
@@ -4712,11 +4829,6 @@
shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
using assms eq_pv_dependants dependants_alt_def eq_dependants by auto
-lemma count_eq_RAG_plus_Th:
- assumes "cntP s th = cntV s th"
- shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}"
- using count_eq_RAG_plus[OF assms] by auto
-
lemma count_eq_tRAG_plus_Th:
assumes "cntP s th = cntV s th"
shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
@@ -4724,9 +4836,17 @@
end
+subsection {* A notion @{text detached} and its relation with @{term cntP}
+ and @{term cntV} *}
+
definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool"
where "detached s th \<equiv> (\<not>(\<exists> cs. holding s th cs)) \<and> (\<not>(\<exists>cs. waiting s th cs))"
+text {*
+ The following lemma shows that a thread is detached means
+ it is isolated from @{term RAG}:
+*}
+
lemma detached_test:
shows "detached s th = (Th th \<notin> Field (RAG s))"
apply(simp add: detached_def Field_def)
@@ -4799,114 +4919,6 @@
end
-section {* Recursive definition of @{term "cp"} *}
-
-lemma cp_alt_def1:
- "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"
-proof -
- have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =
- ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"
- by auto
- thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)
-qed
-
-lemma cp_gen_def_cond:
- assumes "x = Th th"
- shows "cp s th = cp_gen s (Th th)"
-by (unfold cp_alt_def1 cp_gen_def, simp)
-
-lemma cp_gen_over_set:
- assumes "\<forall> x \<in> A. \<exists> th. x = Th th"
- shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A"
-proof(rule f_image_eq)
- fix a
- assume "a \<in> A"
- from assms[rule_format, OF this]
- obtain th where eq_a: "a = Th th" by auto
- show "cp_gen s a = (cp s \<circ> the_thread) a"
- by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp)
-qed
-
-
-context valid_trace
-begin
-(* ddd *)
-lemma cp_gen_rec:
- assumes "x = Th th"
- shows "cp_gen s x = Max ({the_preced s th} \<union> (cp_gen s) ` children (tRAG s) x)"
-proof(cases "children (tRAG s) x = {}")
- case True
- show ?thesis
- by (unfold True cp_gen_def subtree_children, simp add:assms)
-next
- case False
- hence [simp]: "children (tRAG s) x \<noteq> {}" by auto
- note fsbttRAGs.finite_subtree[simp]
- have [simp]: "finite (children (tRAG s) x)"
- by (intro rev_finite_subset[OF fsbttRAGs.finite_subtree],
- rule children_subtree)
- { fix r x
- have "subtree r x \<noteq> {}" by (auto simp:subtree_def)
- } note this[simp]
- have [simp]: "\<exists>x\<in>children (tRAG s) x. subtree (tRAG s) x \<noteq> {}"
- proof -
- from False obtain q where "q \<in> children (tRAG s) x" by blast
- moreover have "subtree (tRAG s) q \<noteq> {}" by simp
- ultimately show ?thesis by blast
- qed
- have h: "Max ((the_preced s \<circ> the_thread) `
- ({x} \<union> \<Union>(subtree (tRAG s) ` children (tRAG s) x))) =
- Max ({the_preced s th} \<union> cp_gen s ` children (tRAG s) x)"
- (is "?L = ?R")
- proof -
- let "Max (?f ` (?A \<union> \<Union> (?g ` ?B)))" = ?L
- let "Max (_ \<union> (?h ` ?B))" = ?R
- let ?L1 = "?f ` \<Union>(?g ` ?B)"
- have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)"
- proof -
- have "?L1 = ?f ` (\<Union> x \<in> ?B.(?g x))" by simp
- also have "... = (\<Union> x \<in> ?B. ?f ` (?g x))" by auto
- finally have "Max ?L1 = Max ..." by simp
- also have "... = Max (Max ` (\<lambda>x. ?f ` subtree (tRAG s) x) ` ?B)"
- by (subst Max_UNION, simp+)
- also have "... = Max (cp_gen s ` children (tRAG s) x)"
- by (unfold image_comp cp_gen_alt_def, simp)
- finally show ?thesis .
- qed
- show ?thesis
- proof -
- have "?L = Max (?f ` ?A \<union> ?L1)" by simp
- also have "... = max (the_preced s (the_thread x)) (Max ?L1)"
- by (subst Max_Un, simp+)
- also have "... = max (?f x) (Max (?h ` ?B))"
- by (unfold eq_Max_L1, simp)
- also have "... =?R"
- by (rule max_Max_eq, (simp)+, unfold assms, simp)
- finally show ?thesis .
- qed
- qed thus ?thesis
- by (fold h subtree_children, unfold cp_gen_def, simp)
-qed
-
-lemma cp_rec:
- "cp s th = Max ({the_preced s th} \<union>
- (cp s o the_thread) ` children (tRAG s) (Th th))"
-proof -
- have "Th th = Th th" by simp
- note h = cp_gen_def_cond[OF this] cp_gen_rec[OF this]
- show ?thesis
- proof -
- have "cp_gen s ` children (tRAG s) (Th th) =
- (cp s \<circ> the_thread) ` children (tRAG s) (Th th)"
- proof(rule cp_gen_over_set)
- show " \<forall>x\<in>children (tRAG s) (Th th). \<exists>th. x = Th th"
- by (unfold tRAG_alt_def, auto simp:children_def)
- qed
- thus ?thesis by (subst (1) h(1), unfold h(2), simp)
- qed
-qed
-end
-
section {* Other properties useful in Implementation.thy or Correctness.thy *}
context valid_trace_e
--- a/PIPDefs.thy Tue Feb 09 22:30:43 2016 +0800
+++ b/PIPDefs.thy Fri Feb 12 12:32:57 2016 +0800
@@ -483,13 +483,6 @@
by (simp)
text {* \noindent
- Observation @{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in
- state @{text "s"}:
- *}
-definition cntCS :: "state \<Rightarrow> thread \<Rightarrow> nat"
- where "cntCS s th = card (holdents s th)"
-
-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
@@ -613,27 +606,39 @@
definition count :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat"
where "count Q l = length (filter Q l)"
-text {* \noindent
- The following observation @{text "cntP s"} returns the number of operation @{text "P"} happened
- before reaching state @{text "s"}.
- *}
+text {*
+ The operation @{term P} is used by a thread to request for resources, while
+ @{term V} is used to release. Therefore, the number of resources
+ held by a thread roughly equals to the number of @{term P} it made minus
+ the number of @{term V}. The equality is rough because the @{term P}-operation
+ might be blocked and fail to give back the holding of the requested resource.
+ In the following, @{text "cntP"} and @{text "cntV"} are the number of @{term P}
+ and @{term "V"} respectively, while @{term cntCS} is the number
+ resources held by a thread and @{text "pvD"} is introduced to account for
+ the above mentioned situation when @{term P} is blocked, so that
+ a equation between @{text cntP}, @{text "cntV"}, @{text "cntCS"} can be established
+ (in the lemma named @{text "valid_trace.cnp_cnv_cncs"}).
+
+ Such a equation, once established, is very handy, because the number of resources
+ held by a thread can be calculated by counting the number of @{term P} and @{text V},
+ which is relatively easy.
+*}
+
definition cntP :: "state \<Rightarrow> thread \<Rightarrow> nat"
where "cntP s th = count (\<lambda> e. \<exists> cs. e = P th cs) s"
-text {* \noindent
- The following observation @{text "cntV s"} returns the number of operation @{text "V"} happened
- before reaching state @{text "s"}.
- *}
definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat"
where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s"
+definition cntCS :: "state \<Rightarrow> thread \<Rightarrow> nat"
+ where "cntCS s th = card (holdents s th)"
+
definition "pvD s th = (if (th \<in> readys s \<or> th \<notin> threads s) then 0 else (1::nat))"
text {* @{text "the_preced"} is also the same as @{text "preced"}, the only
difference is the order of arguemts. *}
definition "the_preced s th = preced th s"
-
text {* @{term "the_thread"} extracts thread out of RAG node. *}
fun the_thread :: "node \<Rightarrow> thread" where
"the_thread (Th th) = th"
@@ -663,14 +668,6 @@
\<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}"
by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)
-definition "cp_gen s x =
- Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"
-
-lemma cp_gen_alt_def:
- "cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))"
- by (auto simp:cp_gen_def)
-
-
(*<*)
end