--- 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) =
+ (\<forall> th cs1 cs2. waiting ss th cs1 \<longrightarrow>
+ waiting ss th cs2 \<longrightarrow> 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 "\<not> 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 "\<not> 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 "\<not> 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 "\<not> 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' \<noteq> 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' \<in> set (wq s cs @ [th])"
+ "th' \<noteq> hd (wq s cs @ [th])" by auto
+ from h(1) and otherwise
+ have "th' \<in> set (wq s cs)" by auto
+ hence "wq s cs \<noteq> []" 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 "\<not> 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 "\<not> 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 "\<not> 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 \<noteq> cs2"
+ show False
+ proof(cases "waiting s th cs1")
+ case True
+ from h[OF this] and otherwise
+ have "\<not> 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 \<in> set (wq s cs1)"
- and h12: "thread \<noteq> hd (wq s cs1)"
- assumes h21: "thread \<in> set (wq s cs2)"
- and h22: "thread \<noteq> hd (wq s cs2)"
- and neq12: "cs1 \<noteq> cs2"
- shows "False"
-proof -
- let "?Q" = "\<lambda> cs s. thread \<in> set (wq s cs) \<and> thread \<noteq> 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: "\<not> ?Q cs1 []" by (simp add:wq_def)
- have nq2: "\<not> ?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: "\<not> ?Q cs1 (moment t1 s)"
- and nn1: "(\<forall>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: "\<not> ?Q cs2 (moment t2 s)"
- and nn2: "(\<forall>i'>t2. ?Q cs2 (moment i' s))" by auto
- { fix s cs
- assume q: "?Q cs s"
- have "thread \<notin> runing s"
- proof
- assume "thread \<in> runing s"
- hence " \<forall>cs. \<not> (thread \<in> set (wq_fun (schs s) cs) \<and>
- thread \<noteq> 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: "\<not> ?Q cs1 (moment t1 s)"
- and nn1: "(\<forall>i'>t1. ?Q cs1 (moment i' s))"
- and lt2: "t2 < length s"
- and np2: "\<not> ?Q cs2 (moment t2 s)"
- and nn2: "(\<forall>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 \<in> set (wq (?e#moment t2 s) cs2)" and
- h2: "thread \<noteq> hd (wq (?e#moment t2 s) cs2)" by auto
- have ?thesis
- proof -
- have "thread \<in> runing (moment t2 s)"
- proof(cases "thread \<in> 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 \<notin> 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 \<in> 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 \<in> set (wq (?e#moment t2 s) cs2)" and
- h2: "thread \<noteq> 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 \<in> set (wq (?e#moment t1 s) cs1)" and
- g2: "thread \<noteq> hd (wq (?e#moment t1 s) cs1)" by auto
- have "?e = V thread cs2 \<or> ?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 \<or> ?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: "\<not> 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) \<in> 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 \<in> readys s"
- using runing_th_s
- by (unfold runing_def, auto)
-
lemma live_th_es: "th \<in> 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: "\<not> 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) \<in> 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 \<union> {cs}) = card (holdents s th) + 1"
@@ -3781,7 +3811,8 @@
unfolded wq_es_cs set_wq', unfolded eq_wq'] .
moreover have "\<not> (th' \<in> set (th # rest) \<and> th' \<noteq> 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' \<in> readys (e#s)"
shows "th' \<in> readys s"