# HG changeset patch # User zhangx # Date 1454674272 -28800 # Node ID 4e59c0ce1511d5bd20da93dc97bdb5c63ede1a2e # Parent b769f43deb30c5cac8d637af5dee0b09c827c482 wq_in_inv and wq_out_inv are removed, a number of loop holes need to be filled. diff -r b769f43deb30 -r 4e59c0ce1511 CpsG.thy --- a/CpsG.thy Thu Feb 04 14:45:30 2016 +0800 +++ b/CpsG.thy Fri Feb 05 20:11:12 2016 +0800 @@ -1,4 +1,4 @@ -theory PIPBasics +theory CpsG imports PIPDefs begin diff -r b769f43deb30 -r 4e59c0ce1511 PIPBasics.thy --- a/PIPBasics.thy Thu Feb 04 14:45:30 2016 +0800 +++ b/PIPBasics.thy Fri Feb 05 20:11:12 2016 +0800 @@ -322,8 +322,9 @@ text {* The following lemmas are the simplification rules for @{term count}, @{term cntP}, @{term cntV}. - It is a major technical in this development to use - the counter of @{term "P"} and @{term "V"} (* ccc *) + It is part of the scheme to use the counting + of @{term "P"} and @{term "V"} operations to reason about + the number of resources occupied by one thread. *} lemma count_rec1 [simp]: @@ -374,6 +375,12 @@ using assms by (unfold cntV_def, cases e, simp+) +text {* + The following two lemmas show that only @{term P} + and @{term V} operation can change the value + of @{term cntP} and @{term cntV}, which is true + obviously. +*} lemma cntP_diff_inv: assumes "cntP (e#s) th \ cntP s th" shows "isP e \ actor e = th" @@ -394,8 +401,6 @@ insert assms V, auto simp:cntV_def) qed (insert assms, auto simp:cntV_def) -(* ccc *) - section {* Locales used to investigate the execution of PIP *} text {* @@ -689,14 +694,23 @@ using vt_moment[of "Suc i", unfolded trace_e] by (unfold_locales, simp) -section {* Distinctiveness of waiting queues *} - -lemma (in valid_trace) finite_threads: - shows "finite (threads s)" - using vt by (induct) (auto elim: step.cases) - -lemma (in valid_trace) finite_readys [simp]: "finite (readys s)" - using finite_threads readys_threads rev_finite_subset by blast +section {* Waiting queues are distinct *} + +text {* + This section proofs 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), + all contain a lemma named @{text "wq_distinct_kept"} to show that + the distinctiveness is preserved by the respective operation. All lemmas + before are to facilitate the proof of @{text "wq_distinct_kept"}. + + The proof also demonstrates the common pattern to prove + invariant properties over valid traces, i.e. to spread the + invariant proof into locales and to assemble the results of all + locales to complete the final proof. + +*} context valid_trace_create begin @@ -760,7 +774,7 @@ with cs_th_RAG show ?thesis by auto qed qed - + lemma wq_es_cs: "wq (e#s) cs = wq s cs @ [th]" by (unfold is_p wq_def, auto simp:Let_def) @@ -834,6 +848,13 @@ context valid_trace begin +text {* + The proof of @{text "wq_distinct"} shows how the results + proved in the foregoing locales are assembled in + a overall structure of induction and case analysis + to get the final conclusion. This scheme will be + used repeatedly in the following. +*} lemma wq_distinct: "distinct (wq s cs)" proof(induct rule:ind) case (Cons s e) @@ -869,99 +890,96 @@ section {* Waiting queues and threads *} -context valid_trace_e +text {* + This section shows that all threads withing waiting queues are + in the @{term threads}-set. In other words, @{term threads} covers + all the threads in waiting queue. + + The proof follows the same pattern as @{thm valid_trace.wq_distinct}. + The desired property is shown to be kept by all operations (or events) + in their respective locales, and finally the main lemmas is + derived by assembling the invariant keeping results of the locales. +*} + +context valid_trace_create begin -lemma wq_out_inv: - assumes s_in: "thread \ set (wq s cs)" - and s_hd: "thread = hd (wq s cs)" - and s_i: "thread \ hd (wq (e#s) cs)" - shows "e = V thread cs" -proof(cases e) --- {* There are only two non-trivial cases: *} - case (V th cs1) - show ?thesis - proof(cases "cs1 = cs") - case True - have "PIP s (V th cs)" using pip_e[unfolded V[unfolded True]] . - thus ?thesis - proof(cases) - case (thread_V) - moreover have "th = thread" using thread_V(2) s_hd - by (unfold s_holding_def wq_def, simp) - ultimately show ?thesis using V True by simp - qed - qed (insert assms V, auto simp:wq_def Let_def split:if_splits) -next - case (P th cs1) - show ?thesis - proof(cases "cs1 = cs") - case True - with P have "wq (e#s) cs = wq_fun (schs s) cs @ [th]" - by (auto simp:wq_def Let_def split:if_splits) - with s_i s_hd s_in have False - by (metis empty_iff hd_append2 list.set(1) wq_def) - thus ?thesis by simp - qed (insert assms P, auto simp:wq_def Let_def split:if_splits) -qed (insert assms, auto simp:wq_def Let_def split:if_splits) - -lemma wq_in_inv: - assumes s_ni: "thread \ set (wq s cs)" - and s_i: "thread \ set (wq (e#s) cs)" - shows "e = P thread cs" -proof(cases e) - -- {* This is the only non-trivial case: *} - case (V th cs1) - have False - proof(cases "cs1 = cs") - case True - show ?thesis - proof(cases "(wq s cs1)") - case (Cons w_hd w_tl) - have "set (wq (e#s) cs) \ set (wq s cs)" - proof - - have "(wq (e#s) cs) = (SOME q. distinct q \ set q = set w_tl)" - using Cons V by (auto simp:wq_def Let_def True split:if_splits) - moreover have "set ... \ set (wq s cs)" - proof(rule someI2) - show "distinct w_tl \ set w_tl = set w_tl" - by (metis distinct.simps(2) local.Cons wq_distinct) - qed (insert Cons True, auto) - ultimately show ?thesis by simp - qed - with assms show ?thesis by auto - qed (insert assms V True, auto simp:wq_def Let_def split:if_splits) - qed (insert assms V, auto simp:wq_def Let_def split:if_splits) - thus ?thesis by auto -qed (insert assms, auto simp:wq_def Let_def split:if_splits) - -end - -lemma (in valid_trace_create) +lemma th_not_in_threads: "th \ threads s" proof - from pip_e[unfolded is_create] show ?thesis by (cases, simp) qed -lemma (in valid_trace_create) +lemma threads_es [simp]: "threads (e#s) = threads s \ {th}" by (unfold is_create, simp) -lemma (in valid_trace_exit) - threads_es [simp]: "threads (e#s) = threads s - {th}" +lemma wq_threads_kept: + assumes "\ th' cs'. th' \ set (wq s cs') \ th' \ threads s" + and "th' \ set (wq (e#s) cs')" + shows "th' \ threads (e#s)" +proof - + have "th' \ threads s" + proof - + from assms(2)[unfolded wq_kept] + have "th' \ set (wq s cs')" . + from assms(1)[OF this] show ?thesis . + qed + with threads_es show ?thesis by simp +qed + +end + +context valid_trace_exit +begin + +lemma threads_es [simp]: "threads (e#s) = threads s - {th}" by (unfold is_exit, simp) -lemma (in valid_trace_p) - threads_es [simp]: "threads (e#s) = threads s" - by (unfold is_p, simp) - -lemma (in valid_trace_v) +lemma + th_not_in_wq: "th \ set (wq s cs)" +proof - + from pip_e[unfolded is_exit] + show ?thesis + by (cases, unfold holdents_def s_holding_def, fold wq_def, + auto elim!:runing_wqE) +qed + +lemma wq_threads_kept: + assumes "\ th' cs'. th' \ set (wq s cs') \ th' \ threads s" + and "th' \ set (wq (e#s) cs')" + shows "th' \ threads (e#s)" +proof - + have "th' \ threads s" + proof - + from assms(2)[unfolded wq_kept] + have "th' \ set (wq s cs')" . + from assms(1)[OF this] show ?thesis . + qed + moreover have "th' \ th" + proof + assume otherwise: "th' = th" + from assms(2)[unfolded wq_kept] + have "th' \ set (wq s cs')" . + with th_not_in_wq[folded otherwise] + show False by simp + qed + ultimately show ?thesis + by (unfold threads_es, simp) +qed + +end + +context valid_trace_v +begin + +lemma threads_es [simp]: "threads (e#s) = threads s" by (unfold is_v, simp) -lemma (in valid_trace_v) - th_not_in_rest[simp]: "th \ set rest" +lemma + th_not_in_rest: "th \ set rest" proof assume otherwise: "th \ set rest" have "distinct (wq s cs)" by (simp add: wq_distinct) @@ -969,10 +987,10 @@ show False by auto qed -lemma (in valid_trace_v) distinct_rest: "distinct rest" +lemma distinct_rest: "distinct rest" by (simp add: distinct_tl rest_def wq_distinct) -lemma (in valid_trace_v) +lemma set_wq_es_cs [simp]: "set (wq (e#s) cs) = set (wq s cs) - {th}" proof(unfold wq_es_cs wq'_def, rule someI2) show "distinct rest \ set rest = set rest" @@ -981,23 +999,117 @@ fix x assume "distinct x \ set x = set rest" thus "set x = set (wq s cs) - {th}" - by (unfold wq_s_cs, simp) + by (unfold wq_s_cs, simp add:th_not_in_rest) +qed + +lemma wq_threads_kept: + assumes "\ th' cs'. th' \ set (wq s cs') \ th' \ threads s" + and "th' \ set (wq (e#s) cs')" + shows "th' \ threads (e#s)" +proof(cases "cs' = cs") + case True + have " th' \ threads s" + proof - + from assms(2)[unfolded True set_wq_es_cs] + have "th' \ set (wq s cs) - {th}" . + hence "th' \ set (wq s cs)" by simp + from assms(1)[OF this] + show ?thesis . + qed + with threads_es show ?thesis by simp +next + case False + have "th' \ threads s" + proof - + from wq_neq_simp[OF False] + have "wq (e # s) cs' = wq s cs'" . + from assms(2)[unfolded this] + have "th' \ set (wq s cs')" . + from assms(1)[OF this] + show ?thesis . + qed + with threads_es show ?thesis by simp qed - -lemma (in valid_trace_exit) - th_not_in_wq: "th \ set (wq s cs)" +end + +context valid_trace_p +begin + +lemma threads_es [simp]: "threads (e#s) = threads s" + by (unfold is_p, simp) + +lemma ready_th_s: "th \ readys s" + using runing_th_s + by (unfold runing_def, auto) + +lemma live_th_s: "th \ threads s" + using readys_threads ready_th_s by auto + +lemma wq_threads_kept: + assumes "\ th' cs'. th' \ set (wq s cs') \ th' \ threads s" + and "th' \ set (wq (e#s) cs')" + shows "th' \ threads (e#s)" +proof(cases "cs' = cs") + case True + from assms(2)[unfolded True wq_es_cs] + have "th' \ set (wq s cs) \ th' = th" by auto + thus ?thesis + proof + assume "th' \ set (wq s cs)" + from assms(1)[OF this] have "th' \ threads s" . + with threads_es + show ?thesis by simp + next + assume "th' = th" + with live_th_s have "th' \ threads s" by simp + with threads_es show ?thesis by simp + qed +next + case False + have "th' \ threads s" + proof - + from wq_neq_simp[OF False] + have "wq (e # s) cs' = wq s cs'" . + from assms(2)[unfolded this] + have "th' \ set (wq s cs')" . + from assms(1)[OF this] + show ?thesis . + qed + with threads_es show ?thesis by simp +qed + +end + +context valid_trace_set +begin + +lemma threads_kept[simp]: + "threads (e#s) = threads s" + by (unfold is_set, simp) + +lemma wq_threads_kept: + assumes "\ th' cs'. th' \ set (wq s cs') \ th' \ threads s" + and "th' \ set (wq (e#s) cs')" + shows "th' \ threads (e#s)" proof - - from pip_e[unfolded is_exit] - show ?thesis - by (cases, unfold holdents_def s_holding_def, fold wq_def, - auto elim!:runing_wqE) + have "th' \ threads s" + using assms(1)[OF assms(2)[unfolded wq_kept]] . + with threads_kept show ?thesis by simp qed +end + +text {* + The is the main lemma of this section, which is derived + by induction, case analysis on event @{text e} and + assembling the @{text "wq_threads_kept"}-results of + all possible cases of @{text "e"}. +*} lemma (in valid_trace) wq_threads: assumes "th \ set (wq s cs)" shows "th \ threads s" using assms -proof(induct rule:ind) +proof(induct arbitrary:th cs rule:ind) case (Nil) thus ?case by (auto simp:wq_def) next @@ -1008,42 +1120,41 @@ case (Create th' prio') interpret vt: valid_trace_create s e th' prio' using Create by (unfold_locales, simp) - show ?thesis - using Cons.hyps(2) Cons.prems by auto + show ?thesis using vt.wq_threads_kept Cons by auto next case (Exit th') interpret vt: valid_trace_exit s e th' using Exit by (unfold_locales, simp) - show ?thesis - using Cons.hyps(2) Cons.prems vt.th_not_in_wq by auto + show ?thesis using vt.wq_threads_kept Cons by auto next case (P th' cs') interpret vt: valid_trace_p s e th' cs' using P by (unfold_locales, simp) - show ?thesis - using Cons.hyps(2) Cons.prems readys_threads - runing_ready vt.is_p vt.runing_th_s vt_e.wq_in_inv - by fastforce + show ?thesis using vt.wq_threads_kept Cons by auto next case (V th' cs') interpret vt: valid_trace_v s e th' cs' using V by (unfold_locales, simp) - show ?thesis using Cons - using vt.is_v vt.threads_es vt_e.wq_in_inv by blast + show ?thesis using vt.wq_threads_kept Cons by auto next case (Set th' prio) interpret vt: valid_trace_set s e th' prio using Set by (unfold_locales, simp) - show ?thesis using Cons.hyps(2) Cons.prems vt.is_set - by (auto simp:wq_def Let_def) + show ?thesis using vt.wq_threads_kept Cons by auto qed qed -section {* RAG and threads *} +subsection {* RAG and threads *} context valid_trace begin +text {* + As corollaries of @{thm wq_threads}, it is shown in this subsection + that the fields (including both domain + and range) of @{term RAG} are covered by @{term threads}. +*} + lemma dm_RAG_threads: assumes in_dom: "(Th th) \ Domain (RAG s)" shows "th \ threads s" @@ -1669,8 +1780,8 @@ assumes "waiting (e#s) th' cs'" obtains "waiting s th' cs'" using assms - by (metis cs_waiting_def event.distinct(15) is_p list.sel(1) - set_ConsD waiting_eq we wq_es_cs' wq_neq_simp wq_out_inv) + by (metis empty_iff list.sel(1) list.set(1) s_waiting_def + set_ConsD wq_def wq_es_cs' wq_neq_simp) lemma holding_esE: assumes "holding (e#s) th' cs'" @@ -1771,9 +1882,7 @@ next case True with assms show ?thesis - using event.inject(3) holder_def is_p s_holding_def s_waiting_def that - waiting_es_th_cs wq_def wq_es_cs' wq_in_inv - by(force) + using s_holding_def that wq_def wq_es_cs' wq_s_cs by auto qed lemma waiting_esE: @@ -1870,7 +1979,7 @@ end -section {* Finiteness of RAG *} +section {* RAG is finite *} context valid_trace begin @@ -2952,6 +3061,9 @@ by (simp add: subtree_def the_preced_def) qed +lemma finite_threads: + shows "finite (threads s)" + using vt by (induct) (auto elim: step.cases) lemma cp_le: assumes th_in: "th \ threads s" @@ -3016,6 +3128,8 @@ } ultimately show ?thesis by auto qed +lemma finite_readys: "finite (readys s)" + using finite_threads readys_threads rev_finite_subset by blast text {* (* ccc *) \noindent Since the current precedence of the threads in ready queue will always be boosted, @@ -3038,7 +3152,7 @@ show "\M\(\x. the_preced s ` {th'. Th th' \ subtree (RAG s) (Th x)}) ` readys s. finite M" using finite_subtree_threads by auto - qed (auto simp:False subtree_def) + 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) @@ -3132,9 +3246,6 @@ using runing_th_s by (unfold runing_def, auto) -lemma live_th_s: "th \ threads s" - using readys_threads ready_th_s by auto - lemma live_th_es: "th \ threads (e#s)" using live_th_s by (unfold is_p, simp)