# HG changeset patch # User zhangx # Date 1455251577 -28800 # Node ID 74fc1eae4605534e45ac3e21938057e3be307c5a # Parent 81c6ede5cd11a78bcb8cdd48793e5d410c8a2855 Commenting of PIPBasics.thy almost completed. The last section needs to be distributed to Correctness.thy and Implementation.thy diff -r 81c6ede5cd11 -r 74fc1eae4605 Implementation.thy --- 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 \ the_thread) ` subtree (tRAG s) x)" + +lemma cp_gen_alt_def: + "cp_gen s = (Max \ (\x. (the_preced s \ 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 "\ x \ A. \ th. x = Th th" + shows "cp_gen s ` A = (cp s \ the_thread) ` A" +proof(rule f_image_eq) + fix a + assume "a \ A" + from assms[rule_format, OF this] + obtain th where eq_a: "a = Th th" by auto + show "cp_gen s a = (cp s \ 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} \ (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 \ {}" 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 \ {}" by (auto simp:subtree_def) + } note this[simp] + have [simp]: "\x\children (tRAG s) x. subtree (tRAG s) x \ {}" + proof - + from False obtain q where "q \ children (tRAG s) x" by blast + moreover have "subtree (tRAG s) q \ {}" by simp + ultimately show ?thesis by blast + qed + have h: "Max ((the_preced s \ the_thread) ` + ({x} \ \(subtree (tRAG s) ` children (tRAG s) x))) = + Max ({the_preced s th} \ cp_gen s ` children (tRAG s) x)" + (is "?L = ?R") + proof - + let "Max (?f ` (?A \ \ (?g ` ?B)))" = ?L + let "Max (_ \ (?h ` ?B))" = ?R + let ?L1 = "?f ` \(?g ` ?B)" + have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)" + proof - + have "?L1 = ?f ` (\ x \ ?B.(?g x))" by simp + also have "... = (\ x \ ?B. ?f ` (?g x))" by auto + finally have "Max ?L1 = Max ..." by simp + also have "... = Max (Max ` (\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 \ ?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} \ + (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 \ the_thread) ` children (tRAG s) (Th th)" + proof(rule cp_gen_over_set) + show " \x\children (tRAG s) (Th th). \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 diff -r 81c6ede5cd11 -r 74fc1eae4605 PIPBasics.thy --- 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' \ (subtree (RAG s) (Th th))})" -proof - - have "Max (the_preced s ` ({th} \ dependants (wq s) th)) = - Max (the_preced s ` {th'. Th th' \ 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' \ (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' \ (subtree (RAG s) (Th th))})" +proof - + have "Max (the_preced s ` ({th} \ dependants (wq s) th)) = + Max (the_preced s ` {th'. Th th' \ 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 \ 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 \ {(Th th, Cs cs)}" and "(Cs cs, Th th'') \ 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 \ 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 \ threads s" shows "cp s th \ 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 ` (\th\readys s. {th'. Th th' \ subtree (RAG s) (Th th)}))" - by (unfold threads_alt_def, simp) + have "?R = + Max (the_preced s ` (\th\readys s. {th'. Th th' \ subtree (RAG s) (Th th)}))" + by (simp add: threads_alt_def) also have "... = Max ((\th\readys s. the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)}))" by (unfold image_UN, simp) @@ -3355,9 +3428,10 @@ {th'. Th th' \ 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 \ (\th. the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)})) ` readys s)" - by (unfold image_comp, simp) + also have "... = + Max ((Max \ (\th. the_preced s ` {th'. Th th' \ 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 \ 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 \ 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) \ (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) \ (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) \ (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) \ (tRAG s)^+} = {}" @@ -4724,9 +4836,17 @@ end +subsection {* A notion @{text detached} and its relation with @{term cntP} + and @{term cntV} *} + definition detached :: "state \ thread \ bool" where "detached s th \ (\(\ cs. holding s th cs)) \ (\(\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 \ 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 \ 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 "\ x \ A. \ th. x = Th th" - shows "cp_gen s ` A = (cp s \ the_thread) ` A" -proof(rule f_image_eq) - fix a - assume "a \ A" - from assms[rule_format, OF this] - obtain th where eq_a: "a = Th th" by auto - show "cp_gen s a = (cp s \ 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} \ (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 \ {}" 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 \ {}" by (auto simp:subtree_def) - } note this[simp] - have [simp]: "\x\children (tRAG s) x. subtree (tRAG s) x \ {}" - proof - - from False obtain q where "q \ children (tRAG s) x" by blast - moreover have "subtree (tRAG s) q \ {}" by simp - ultimately show ?thesis by blast - qed - have h: "Max ((the_preced s \ the_thread) ` - ({x} \ \(subtree (tRAG s) ` children (tRAG s) x))) = - Max ({the_preced s th} \ cp_gen s ` children (tRAG s) x)" - (is "?L = ?R") - proof - - let "Max (?f ` (?A \ \ (?g ` ?B)))" = ?L - let "Max (_ \ (?h ` ?B))" = ?R - let ?L1 = "?f ` \(?g ` ?B)" - have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)" - proof - - have "?L1 = ?f ` (\ x \ ?B.(?g x))" by simp - also have "... = (\ x \ ?B. ?f ` (?g x))" by auto - finally have "Max ?L1 = Max ..." by simp - also have "... = Max (Max ` (\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 \ ?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} \ - (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 \ the_thread) ` children (tRAG s) (Th th)" - proof(rule cp_gen_over_set) - show " \x\children (tRAG s) (Th th). \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 diff -r 81c6ede5cd11 -r 74fc1eae4605 PIPDefs.thy --- 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 \ thread \ 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 \ bool) \ 'a list \ 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 \ thread \ nat" where "cntP s th = count (\ e. \ 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 \ thread \ nat" where "cntV s th = count (\ e. \ cs. e = V th cs) s" +definition cntCS :: "state \ thread \ nat" + where "cntCS s th = card (holdents s th)" + definition "pvD s th = (if (th \ readys s \ th \ 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 \ thread" where "the_thread (Th th) = th" @@ -663,14 +668,6 @@ \ cs. (Th th1, Cs cs) \ RAG s \ (Cs cs, Th th2) \ RAG s}" by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def) -definition "cp_gen s x = - Max ((the_preced s \ the_thread) ` subtree (tRAG s) x)" - -lemma cp_gen_alt_def: - "cp_gen s = (Max \ (\x. (the_preced s \ the_thread) ` subtree (tRAG s) x))" - by (auto simp:cp_gen_def) - - (*<*) end