# HG changeset patch # User zhangx # Date 1454773323 -28800 # Node ID 4b416723a616fa0220c8eb28c6befb82bf4d8c3b # Parent 4782d82c3ae964a173cab374e5fa85ccd80750cb More redundant lemmas are reomved. diff -r 4782d82c3ae9 -r 4b416723a616 PIPBasics.thy --- a/PIPBasics.thy Sat Feb 06 08:35:45 2016 +0800 +++ b/PIPBasics.thy Sat Feb 06 23:42:03 2016 +0800 @@ -2044,221 +2044,241 @@ section {* RAG is acyclic *} -text {* (* ddd *) - The nature of the work is like this: since it starts from a very simple and basic - model, even intuitively very `basic` and `obvious` properties need to derived from scratch. - For instance, the fact - that one thread can not be blocked by two critical resources at the same time - is obvious, because only running threads can make new requests, if one is waiting for - a critical resource and get blocked, it can not make another resource request and get - blocked the second time (because it is not running). - - To derive this fact, one needs to prove by contraction and - reason about time (or @{text "moement"}). The reasoning is based on a generic theorem - named @{text "p_split"}, which is about status changing along the time axis. It says if - a condition @{text "Q"} is @{text "True"} at a state @{text "s"}, - but it was @{text "False"} at the very beginning, then there must exits a moment @{text "t"} - in the history of @{text "s"} (notice that @{text "s"} itself is essentially the history - of events leading to it), such that @{text "Q"} switched - from being @{text "False"} to @{text "True"} and kept being @{text "True"} - till the last moment of @{text "s"}. - - Suppose a thread @{text "th"} is blocked - on @{text "cs1"} and @{text "cs2"} in some state @{text "s"}, - since no thread is blocked at the very beginning, by applying - @{text "p_split"} to these two blocking facts, there exist - two moments @{text "t1"} and @{text "t2"} in @{text "s"}, such that - @{text "th"} got blocked on @{text "cs1"} and @{text "cs2"} - and kept on blocked on them respectively ever since. - - Without lost of generality, we assume @{text "t1"} is earlier than @{text "t2"}. - However, since @{text "th"} was blocked ever since memonent @{text "t1"}, so it was still - in blocked state at moment @{text "t2"} and could not - make any request and get blocked the second time: Contradiction. +subsection {* Uniqueness of waiting *} + +text {* + Uniqueness of waiting is expressed by the following + predicate over system state (or event trace). + It says a thread can only be blocked on one resource. +*} + +definition + "waiting_unique (ss::state) = + (\ th cs1 cs2. waiting ss th cs1 \ + waiting ss th cs2 \ cs1 = cs2)" + +text {* + We are going to show (in the + lemma named @{text waiting_unique}) that + this property holds on any valid trace (or system state). +*} + +text {* + As a first step, we need to understand how + a thread is get blocked. + We show in the following lemmas + (all named @{text "waiting_inv"}) that + @{term P}-operation is the only cause. *} +context valid_trace_create +begin +lemma waiting_inv: + assumes "\ waiting s th' cs'" + and "waiting (e#s) th' cs'" + shows "e = P th' cs'" + using assms + by (unfold s_waiting_def, fold wq_def, simp) +end + +context valid_trace_set +begin +lemma waiting_inv: + assumes "\ waiting s th' cs'" + and "waiting (e#s) th' cs'" + shows "e = P th' cs'" + using assms + by (unfold s_waiting_def, fold wq_def, simp) +end + +context valid_trace_exit +begin +lemma waiting_inv: + assumes "\ waiting s th' cs'" + and "waiting (e#s) th' cs'" + shows "e = P th' cs'" + using assms + by (unfold s_waiting_def, fold wq_def, simp) +end + +context valid_trace_p +begin + +lemma waiting_inv: + assumes "\ waiting s th' cs'" + and "waiting (e#s) th' cs'" + shows "e = P th' cs'" +proof(cases "cs' = cs") + case True + moreover have "th' = th" + proof(rule ccontr) + assume otherwise: "th' \ th" + have "waiting s th' cs'" + proof - + from assms(2)[unfolded True s_waiting_def, + folded wq_def, unfolded wq_es_cs] + have h: "th' \ set (wq s cs @ [th])" + "th' \ hd (wq s cs @ [th])" by auto + from h(1) and otherwise + have "th' \ set (wq s cs)" by auto + hence "wq s cs \ []" by auto + hence "hd (wq s cs @ [th]) = hd (wq s cs)" by auto + with h otherwise + have "waiting s th' cs" + by (unfold s_waiting_def, fold wq_def, auto) + from this[folded True] show ?thesis . + qed + with assms(1) show False by simp + qed + ultimately show ?thesis using is_p by simp +next + case False + hence "wq (e#s) cs' = wq s cs'" by simp + from assms[unfolded s_waiting_def, folded wq_def, + unfolded this] + show ?thesis by simp +qed + +end + +context valid_trace_v_n +begin + +lemma waiting_inv: + assumes "\ waiting s th' cs'" + and "waiting (e#s) th' cs'" + shows "e = P th' cs'" +proof - + from assms(2) + show ?thesis + by (cases rule:waiting_esE, insert assms, auto) +qed + +end + +context valid_trace_v_e +begin + +lemma waiting_inv: + assumes "\ waiting s th' cs'" + and "waiting (e#s) th' cs'" + shows "e = P th' cs'" +proof - + from assms(2) + show ?thesis + by (cases rule:waiting_esE, insert assms, auto) +qed + +end + + +context valid_trace_e +begin + +lemma waiting_inv: + assumes "\ waiting s th cs" + and "waiting (e#s) th cs" + shows "e = P th cs" +proof(cases e) + case (Create th' prio') + then interpret vt: valid_trace_create s e th' prio' + by (unfold_locales, simp) + show ?thesis using vt.waiting_inv[OF assms] by simp +next + case (Exit th') + then interpret vt: valid_trace_exit s e th' + by (unfold_locales, simp) + show ?thesis using vt.waiting_inv[OF assms] by simp +next + case (Set th' prio') + then interpret vt: valid_trace_set s e th' prio' + by (unfold_locales, simp) + show ?thesis using vt.waiting_inv[OF assms] by simp +next + case (P th' cs') + then interpret vt: valid_trace_p s e th' cs' + by (unfold_locales, simp) + show ?thesis using vt.waiting_inv[OF assms] by simp +next + case (V th' cs') + then interpret vt_e: valid_trace_v s e th' cs' + by (unfold_locales, simp) + show ?thesis + proof(cases "vt_e.rest = []") + case True + then interpret vt: valid_trace_v_e s e th' cs' + by (unfold_locales, simp) + show ?thesis using vt.waiting_inv[OF assms] by simp + next + case False + then interpret vt: valid_trace_v_n s e th' cs' + by (unfold_locales, simp) + show ?thesis using vt.waiting_inv[OF assms] by simp + qed +qed + +lemma waiting_unique_kept: + assumes "waiting_unique s" + shows "waiting_unique (e#s)" +proof - + note h = assms[unfolded waiting_unique_def, rule_format] + { fix th cs1 cs2 + assume w1: "waiting (e#s) th cs1" + and w2: "waiting (e#s) th cs2" + have "cs1 = cs2" + proof(rule ccontr) + assume otherwise: "cs1 \ cs2" + show False + proof(cases "waiting s th cs1") + case True + from h[OF this] and otherwise + have "\ waiting s th cs2" by auto + from waiting_inv[OF this w2] + have "e = P th cs2" . + then interpret vt: valid_trace_p s e th cs2 + by (unfold_locales, simp) + from vt.th_not_waiting and True + show ?thesis by simp + next + case False + from waiting_inv[OF this w1] + have "e = P th cs1" . + then interpret vt: valid_trace_p s e th cs1 + by (unfold_locales, simp) + have "wq (e # s) cs2 = wq s cs2" + using otherwise by simp + from w2[unfolded s_waiting_def, folded wq_def, + unfolded this] + have "waiting s th cs2" + by (unfold s_waiting_def, fold wq_def, simp) + thus ?thesis by (simp add: vt.th_not_waiting) + qed + qed + } thus ?thesis by (unfold waiting_unique_def, auto) +qed + +end context valid_trace begin -lemma waiting_unique_pre: (* ddd *) - assumes h11: "thread \ set (wq s cs1)" - and h12: "thread \ hd (wq s cs1)" - assumes h21: "thread \ set (wq s cs2)" - and h22: "thread \ hd (wq s cs2)" - and neq12: "cs1 \ cs2" - shows "False" -proof - - let "?Q" = "\ cs s. thread \ set (wq s cs) \ thread \ hd (wq s cs)" - from h11 and h12 have q1: "?Q cs1 s" by simp - from h21 and h22 have q2: "?Q cs2 s" by simp - have nq1: "\ ?Q cs1 []" by (simp add:wq_def) - have nq2: "\ ?Q cs2 []" by (simp add:wq_def) - from p_split [of "?Q cs1", OF q1 nq1] - obtain t1 where lt1: "t1 < length s" - and np1: "\ ?Q cs1 (moment t1 s)" - and nn1: "(\i'>t1. ?Q cs1 (moment i' s))" by auto - from p_split [of "?Q cs2", OF q2 nq2] - obtain t2 where lt2: "t2 < length s" - and np2: "\ ?Q cs2 (moment t2 s)" - and nn2: "(\i'>t2. ?Q cs2 (moment i' s))" by auto - { fix s cs - assume q: "?Q cs s" - have "thread \ runing s" - proof - assume "thread \ runing s" - hence " \cs. \ (thread \ set (wq_fun (schs s) cs) \ - thread \ hd (wq_fun (schs s) cs))" - by (unfold runing_def s_waiting_def readys_def, auto) - from this[rule_format, of cs] q - show False by (simp add: wq_def) - qed - } note q_not_runing = this - { fix t1 t2 cs1 cs2 - assume lt1: "t1 < length s" - and np1: "\ ?Q cs1 (moment t1 s)" - and nn1: "(\i'>t1. ?Q cs1 (moment i' s))" - and lt2: "t2 < length s" - and np2: "\ ?Q cs2 (moment t2 s)" - and nn2: "(\i'>t2. ?Q cs2 (moment i' s))" - and lt12: "t1 < t2" - let ?t3 = "Suc t2" - interpret ve2: valid_moment_e _ t2 using lt2 - by (unfold_locales, simp) - let ?e = ve2.next_e - have "t2 < ?t3" by simp - from nn2 [rule_format, OF this] and ve2.trace_e - have h1: "thread \ set (wq (?e#moment t2 s) cs2)" and - h2: "thread \ hd (wq (?e#moment t2 s) cs2)" by auto - have ?thesis - proof - - have "thread \ runing (moment t2 s)" - proof(cases "thread \ set (wq (moment t2 s) cs2)") - case True - have "?e = V thread cs2" - proof - - have eq_th: "thread = hd (wq (moment t2 s) cs2)" - using True and np2 by auto - thus ?thesis - using True h2 ve2.vat_moment_e.wq_out_inv by blast - qed - thus ?thesis - using step.cases ve2.vat_moment_e.pip_e by auto - next - case False - hence "?e = P thread cs2" - using h1 ve2.vat_moment_e.wq_in_inv by blast - thus ?thesis - using step.cases ve2.vat_moment_e.pip_e by auto - qed - moreover have "thread \ runing (moment t2 s)" - by (rule q_not_runing[OF nn1[rule_format, OF lt12]]) - ultimately show ?thesis by simp - qed - } note lt_case = this - show ?thesis - proof - - { assume "t1 < t2" - from lt_case[OF lt1 np1 nn1 lt2 np2 nn2 this] - have ?thesis . - } moreover { - assume "t2 < t1" - from lt_case[OF lt2 np2 nn2 lt1 np1 nn1 this] - have ?thesis . - } moreover { - assume eq_12: "t1 = t2" - let ?t3 = "Suc t2" - interpret ve2: valid_moment_e _ t2 using lt2 - by (unfold_locales, simp) - let ?e = ve2.next_e - have "t2 < ?t3" by simp - from nn2 [rule_format, OF this] and ve2.trace_e - have h1: "thread \ set (wq (?e#moment t2 s) cs2)" by auto - have lt_2: "t2 < ?t3" by simp - from nn2 [rule_format, OF this] and ve2.trace_e - have h1: "thread \ set (wq (?e#moment t2 s) cs2)" and - h2: "thread \ hd (wq (?e#moment t2 s) cs2)" by auto - from nn1[rule_format, OF lt_2[folded eq_12], unfolded ve2.trace_e[folded eq_12]] - eq_12[symmetric] - have g1: "thread \ set (wq (?e#moment t1 s) cs1)" and - g2: "thread \ hd (wq (?e#moment t1 s) cs1)" by auto - have "?e = V thread cs2 \ ?e = P thread cs2" - using h1 h2 np2 ve2.vat_moment_e.wq_in_inv - ve2.vat_moment_e.wq_out_inv by blast - moreover have "?e = V thread cs1 \ ?e = P thread cs1" - using eq_12 g1 g2 np1 ve2.vat_moment_e.wq_in_inv - ve2.vat_moment_e.wq_out_inv by blast - ultimately have ?thesis using neq12 by auto - } ultimately show ?thesis using nat_neq_iff by blast - qed -qed - -text {* - This lemma is a simple corrolary of @{text "waiting_unique_pre"}. -*} - -lemma waiting_unique: - assumes "waiting s th cs1" - and "waiting s th cs2" - shows "cs1 = cs2" - using waiting_unique_pre assms - unfolding wq_def s_waiting_def - by auto - -end - -lemma (in valid_trace_v) - preced_es [simp]: "preced th (e#s) = preced th s" - by (unfold is_v preced_def, simp) - -lemma the_preced_v[simp]: "the_preced (V th cs#s) = the_preced s" -proof - fix th' - show "the_preced (V th cs # s) th' = the_preced s th'" - by (unfold the_preced_def preced_def, simp) -qed - - -lemma (in valid_trace_v) - the_preced_es: "the_preced (e#s) = the_preced s" - by (unfold is_v preced_def, simp) - -context valid_trace_p -begin - -lemma not_holding_s_th_cs: "\ holding s th cs" -proof - assume otherwise: "holding s th cs" - from pip_e[unfolded is_p] - show False - proof(cases) - case (thread_P) - moreover have "(Cs cs, Th th) \ RAG s" - using otherwise cs_holding_def - holding_eq th_not_in_wq by auto - ultimately show ?thesis by auto - qed +lemma waiting_unique + [unfolded waiting_unique_def, rule_format]: + shows "waiting_unique s" +proof(induct rule:ind) + case Nil + show ?case + by (unfold waiting_unique_def s_waiting_def, simp) +next + case (Cons s e) + then interpret vt: valid_trace_e s e by simp + show ?case using Cons(2) vt.waiting_unique_kept + by simp qed end - -lemma (in valid_trace_v_n) finite_waiting_set: - "finite {(Th th', Cs cs) |th'. next_th s th cs th'}" - by (simp add: waiting_set_eq) - -lemma (in valid_trace_v_n) finite_holding_set: - "finite {(Cs cs, Th th') |th'. next_th s th cs th'}" - by (simp add: holding_set_eq) - -lemma (in valid_trace_v_e) finite_waiting_set: - "finite {(Th th', Cs cs) |th'. next_th s th cs th'}" - by (simp add: waiting_set_eq) - -lemma (in valid_trace_v_e) finite_holding_set: - "finite {(Cs cs, Th th') |th'. next_th s th cs th'}" - by (simp add: holding_set_eq) - +subsection {* Acyclic keeping *} context valid_trace_v_e begin @@ -2279,7 +2299,7 @@ lemma waiting_taker: "waiting s taker cs" apply (unfold s_waiting_def, fold wq_def, unfold wq_s_cs taker_def) - using eq_wq' th'_in_inv wq'_def by fastforce + using eq_wq' set_wq' th_not_in_rest by auto lemma acylic_RAG_kept: @@ -3260,10 +3280,6 @@ context valid_trace_p begin -lemma ready_th_s: "th \ readys s" - using runing_th_s - by (unfold runing_def, auto) - lemma live_th_es: "th \ threads (e#s)" using live_th_s by (unfold is_p, simp) @@ -3323,6 +3339,20 @@ } ultimately show ?thesis by auto qed +lemma not_holding_s_th_cs: "\ holding s th cs" +proof + assume otherwise: "holding s th cs" + from pip_e[unfolded is_p] + show False + proof(cases) + case (thread_P) + moreover have "(Cs cs, Th th) \ RAG s" + using otherwise cs_holding_def + holding_eq th_not_in_wq by auto + ultimately show ?thesis by auto + qed +qed + lemma cntCS_es_th: "cntCS (e#s) th = cntCS s th + 1" proof - have "card (holdents s th \ {cs}) = card (holdents s th) + 1" @@ -3781,7 +3811,8 @@ unfolded wq_es_cs set_wq', unfolded eq_wq'] . moreover have "\ (th' \ set (th # rest) \ th' \ hd (th # rest))" using n_wait[unfolded True s_waiting_def, folded wq_def, unfolded wq_s_cs] . - ultimately have "th' = taker" by auto + ultimately have "th' = taker" using th_not_in_rest by simp + thm taker_def wq'_def with assms(1) show ?thesis by simp qed @@ -4343,10 +4374,6 @@ using holdents_kept by (unfold cntCS_def, simp) -lemma threads_kept[simp]: - "threads (e#s) = threads s" - by (unfold is_set, simp) - lemma readys_kept1: assumes "th' \ readys (e#s)" shows "th' \ readys s"