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