--- a/PIPBasics.thy Fri Jan 29 11:01:13 2016 +0800
+++ b/PIPBasics.thy Sun Jan 31 18:15:13 2016 +0800
@@ -2,6 +2,8 @@
imports PIPDefs
begin
+section {* Generic aulxiliary lemmas *}
+
lemma f_image_eq:
assumes h: "\<And> a. a \<in> A \<Longrightarrow> f a = g a"
shows "f ` A = g ` A"
@@ -84,6 +86,8 @@
finally show ?thesis by simp
qed
+section {* Lemmas do not depend on trace validity *}
+
lemma birth_time_lt:
assumes "s \<noteq> []"
shows "last_set th s < length s"
@@ -152,116 +156,9 @@
thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)
qed
-(* ccc *)
-
-
-locale valid_trace =
- fixes s
- assumes vt : "vt s"
-
-locale valid_trace_e = valid_trace +
- fixes e
- assumes vt_e: "vt (e#s)"
-begin
-
-lemma pip_e: "PIP s e"
- using vt_e by (cases, simp)
-
-end
-
-locale valid_trace_create = valid_trace_e +
- fixes th prio
- assumes is_create: "e = Create th prio"
-
-locale valid_trace_exit = valid_trace_e +
- fixes th
- assumes is_exit: "e = Exit th"
-
-locale valid_trace_p = valid_trace_e +
- fixes th cs
- assumes is_p: "e = P th cs"
-
-locale valid_trace_v = valid_trace_e +
- fixes th cs
- assumes is_v: "e = V th cs"
-begin
- definition "rest = tl (wq s cs)"
- definition "wq' = (SOME q. distinct q \<and> set q = set rest)"
-end
-
-locale valid_trace_v_n = valid_trace_v +
- assumes rest_nnl: "rest \<noteq> []"
-
-locale valid_trace_v_e = valid_trace_v +
- assumes rest_nil: "rest = []"
-
-locale valid_trace_set= valid_trace_e +
- fixes th prio
- assumes is_set: "e = Set th prio"
-
-context valid_trace
-begin
-
-lemma ind [consumes 0, case_names Nil Cons, induct type]:
- assumes "PP []"
- and "(\<And>s e. valid_trace_e s e \<Longrightarrow>
- PP s \<Longrightarrow> PIP s e \<Longrightarrow> PP (e # s))"
- shows "PP s"
-proof(induct rule:vt.induct[OF vt, case_names Init Step])
- case Init
- from assms(1) show ?case .
-next
- case (Step s e)
- show ?case
- proof(rule assms(2))
- show "valid_trace_e s e" using Step by (unfold_locales, auto)
- next
- show "PP s" using Step by simp
- next
- show "PIP s e" using Step by simp
- qed
-qed
-
-lemma vt_moment: "\<And> t. vt (moment t s)"
-proof(induct rule:ind)
- case Nil
- thus ?case by (simp add:vt_nil)
-next
- case (Cons s e t)
- show ?case
- proof(cases "t \<ge> length (e#s)")
- case True
- from True have "moment t (e#s) = e#s" by simp
- thus ?thesis using Cons
- by (simp add:valid_trace_def valid_trace_e_def, auto)
- next
- case False
- from Cons have "vt (moment t s)" by simp
- moreover have "moment t (e#s) = moment t s"
- proof -
- from False have "t \<le> length s" by simp
- from moment_app [OF this, of "[e]"]
- show ?thesis by simp
- qed
- ultimately show ?thesis by simp
- qed
-qed
-
-lemma finite_threads:
- shows "finite (threads s)"
-using vt by (induct) (auto elim: step.cases)
-
-end
-
lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
by (unfold s_RAG_def, auto)
-locale valid_moment = valid_trace +
- fixes i :: nat
-
-sublocale valid_moment < vat_moment: valid_trace "(moment i s)"
- by (unfold_locales, insert vt_moment, auto)
-
lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
by (unfold s_waiting_def cs_waiting_def wq_def, auto)
@@ -289,9 +186,6 @@
using assms
by (simp add:runing_def readys_def s_waiting_def wq_def)
-context valid_trace
-begin
-
lemma runing_wqE:
assumes "th \<in> runing s"
and "th \<in> set (wq s cs)"
@@ -312,12 +206,287 @@
with eq_wq that show ?thesis by metis
qed
+(* ccc *)
+
+section {* Locales used to investigate the execution of PIP *}
+
+text {*
+ The following locale @{text valid_trace} is used to constrain the
+ trace to be valid. All properties hold for valid traces are
+ derived under this locale.
+*}
+locale valid_trace =
+ fixes s
+ assumes vt : "vt s"
+
+text {*
+ The following locale @{text valid_trace_e} describes
+ the valid extension of a valid trace. The event @{text "e"}
+ represents an event in the system, which corresponds
+ to a one step operation of the PIP protocol.
+ It is required that @{text "e"} is an event eligible to happen
+ under state @{text "s"}, which is already required to be valid
+ by the parent locale @{text "valid_trace"}.
+
+ This locale is used to investigate one step execution of PIP,
+ properties concerning the effects of @{text "e"}'s execution,
+ for example, how the values of observation functions are changed,
+ or how desirable properties are kept invariant, are derived
+ under this locale. The state before execution is @{text "s"}, while
+ the state after execution is @{text "e#s"}. Therefore, the lemmas
+ derived usually relate observations on @{text "e#s"} to those
+ on @{text "s"}.
+*}
+
+locale valid_trace_e = valid_trace +
+ fixes e
+ assumes vt_e: "vt (e#s)"
+begin
+
+text {*
+ The following lemma shows that @{text "e"} must be a
+ eligible event (or a valid step) to be taken under
+ the state represented by @{text "s"}.
+*}
+lemma pip_e: "PIP s e"
+ using vt_e by (cases, simp)
+
end
+text {*
+ Because @{term "e#s"} is also a valid trace, properties
+ derived for valid trace @{term s} also hold on @{term "e#s"}.
+*}
+sublocale valid_trace_e < vat_es!: valid_trace "e#s"
+ using vt_e
+ by (unfold_locales, simp)
+
+text {*
+ For each specific event (or operation), there is a sublocale
+ further constraining that the event @{text e} to be that
+ particular event.
+
+ For example, the following
+ locale @{text "valid_trace_create"} is the sublocale for
+ event @{term "Create"}:
+*}
+locale valid_trace_create = valid_trace_e +
+ fixes th prio
+ assumes is_create: "e = Create th prio"
+
+locale valid_trace_exit = valid_trace_e +
+ fixes th
+ assumes is_exit: "e = Exit th"
+
+locale valid_trace_p = valid_trace_e +
+ fixes th cs
+ assumes is_p: "e = P th cs"
+
+text {*
+ locale @{text "valid_trace_p"} is divided further into two
+ sublocales, namely, @{text "valid_trace_p_h"}
+ and @{text "valid_trace_p_w"}.
+*}
+
+text {*
+ The following two sublocales @{text "valid_trace_p_h"}
+ and @{text "valid_trace_p_w"} represent two complementary
+ cases under @{text "valid_trace_p"}, where
+ @{text "valid_trace_p_h"} further constraints that
+ @{text "wq s cs = []"}, which means the waiting queue of
+ the requested resource @{text "cs"} is empty, in which
+ case, the requesting thread @{text "th"}
+ will take hold of @{text "cs"}.
+
+ Opposite to @{text "valid_trace_p_h"},
+ @{text "valid_trace_p_w"} constraints that
+ @{text "wq s cs \<noteq> []"}, which means the waiting queue of
+ the requested resource @{text "cs"} is nonempty, in which
+ case, the requesting thread @{text "th"} will be blocked
+ on @{text "cs"}:
+
+ Peculiar properties will be derived under respective
+ locales.
+*}
+
+locale valid_trace_p_h = valid_trace_p +
+ assumes we: "wq s cs = []"
+
+locale valid_trace_p_w = valid_trace_p +
+ assumes wne: "wq s cs \<noteq> []"
+begin
+
+text {*
+ The following @{text "holder"} designates
+ the holder of @{text "cs"} before the @{text "P"}-operation.
+*}
+definition "holder = hd (wq s cs)"
+
+text {*
+ The following @{text "waiters"} designates
+ the list of threads waiting for @{text "cs"}
+ before the @{text "P"}-operation.
+*}
+definition "waiters = tl (wq s cs)"
+end
+
+text {*
+ @{text "valid_trace_v"} is set for the @{term V}-operation.
+*}
+locale valid_trace_v = valid_trace_e +
+ fixes th cs
+ assumes is_v: "e = V th cs"
+begin
+ -- {* The following @{text "rest"} is the tail of
+ waiting queue of the resource @{text "cs"}
+ to be released by this @{text "V"}-operation.
+ *}
+ definition "rest = tl (wq s cs)"
+
+ text {*
+ The following @{text "wq'"} is the waiting
+ queue of @{term "cs"}
+ after the @{text "V"}-operation, which
+ is simply a reordering of @{term "rest"}.
+
+ The effect of this reordering needs to be
+ understood by two cases:
+ \begin{enumerate}
+ \item When @{text "rest = []"},
+ the reordering gives rise to an empty list as well,
+ which means there is no thread holding or waiting
+ for resource @{term "cs"}, therefore, it is free.
+
+ \item When @{text "rest \<noteq> []"}, the effect of
+ this reordering is to arbitrarily
+ switch one thread in @{term "rest"} to the
+ head, which, by definition take over the hold
+ of @{term "cs"} and is designated by @{text "taker"}
+ in the following sublocale @{text "valid_trace_v_n"}.
+ *}
+ definition "wq' = (SOME q. distinct q \<and> set q = set rest)"
+
+ text {*
+ The following @{text "rest'"} is the tail of the
+ waiting queue after the @{text "V"}-operation.
+ It plays only auxiliary role to ease reasoning.
+ *}
+ definition "rest' = tl wq'"
+
+end
+
+text {*
+ In the following, @{text "valid_trace_v"} is also
+ divided into two
+ sublocales: when @{text "rest"} is empty (represented
+ by @{text "valid_trace_v_e"}), which means, there is no thread waiting
+ for @{text "cs"}, therefore, after the @{text "V"}-operation,
+ it will become free; otherwise (represented
+ by @{text "valid_trace_v_n"}), one thread
+ will be picked from those in @{text "rest"} to take
+ over @{text "cs"}.
+*}
+
+locale valid_trace_v_e = valid_trace_v +
+ assumes rest_nil: "rest = []"
+
+locale valid_trace_v_n = valid_trace_v +
+ assumes rest_nnl: "rest \<noteq> []"
+begin
+
+text {*
+ The following @{text "taker"} is the thread to
+ take over @{text "cs"}.
+*}
+ definition "taker = hd wq'"
+
+end
+
+
+locale valid_trace_set = valid_trace_e +
+ fixes th prio
+ assumes is_set: "e = Set th prio"
+
+context valid_trace
+begin
+
+text {*
+ Induction rule introduced to easy the
+ derivation of properties for valid trace @{term "s"}.
+ One more premises, namely @{term "valid_trace_e s e"}
+ is added, so that an interpretation of
+ @{text "valid_trace_e"} can be instantiated
+ so that all properties derived so far becomes
+ available in the proof of induction step.
+
+ You will see its use in the proofs that follows.
+*}
+lemma ind [consumes 0, case_names Nil Cons, induct type]:
+ assumes "PP []"
+ and "(\<And>s e. valid_trace_e s e \<Longrightarrow>
+ PP s \<Longrightarrow> PIP s e \<Longrightarrow> PP (e # s))"
+ shows "PP s"
+proof(induct rule:vt.induct[OF vt, case_names Init Step])
+ case Init
+ from assms(1) show ?case .
+next
+ case (Step s e)
+ show ?case
+ proof(rule assms(2))
+ show "valid_trace_e s e" using Step by (unfold_locales, auto)
+ next
+ show "PP s" using Step by simp
+ next
+ show "PIP s e" using Step by simp
+ qed
+qed
+
+text {*
+ The following lemma says that if @{text "s"} is a valid state, so
+ is its any postfix. Where @{term "monent t s"} is the postfix of
+ @{term "s"} with length @{term "t"}.
+*}
+lemma vt_moment: "\<And> t. vt (moment t s)"
+proof(induct rule:ind)
+ case Nil
+ thus ?case by (simp add:vt_nil)
+next
+ case (Cons s e t)
+ show ?case
+ proof(cases "t \<ge> length (e#s)")
+ case True
+ from True have "moment t (e#s) = e#s" by simp
+ thus ?thesis using Cons
+ by (simp add:valid_trace_def valid_trace_e_def, auto)
+ next
+ case False
+ from Cons have "vt (moment t s)" by simp
+ moreover have "moment t (e#s) = moment t s"
+ proof -
+ from False have "t \<le> length s" by simp
+ from moment_app [OF this, of "[e]"]
+ show ?thesis by simp
+ qed
+ ultimately show ?thesis by simp
+ qed
+qed
+end
+
+text {*
+ The following locale @{text "valid_moment"} is to inherit the properties
+ derived on any valid state to the prefix of it, with length @{text "i"}.
+*}
+locale valid_moment = valid_trace +
+ fixes i :: nat
+
+sublocale valid_moment < vat_moment: valid_trace "(moment i s)"
+ by (unfold_locales, insert vt_moment, auto)
+
+
context valid_trace_create
begin
-lemma wq_neq_simp [simp]:
+lemma wq_kept [simp]:
shows "wq (e#s) cs' = wq s cs'"
using assms unfolding is_create wq_def
by (auto simp:Let_def)
@@ -331,7 +500,7 @@
context valid_trace_exit
begin
-lemma wq_neq_simp [simp]:
+lemma wq_kept [simp]:
shows "wq (e#s) cs' = wq s cs'"
using assms unfolding is_exit wq_def
by (auto simp:Let_def)
@@ -342,7 +511,7 @@
using assms by simp
end
-context valid_trace_p
+context valid_trace_p (* ccc *)
begin
lemma wq_neq_simp [simp]:
@@ -482,7 +651,7 @@
context valid_trace_set
begin
-lemma wq_neq_simp [simp]:
+lemma wq_kept [simp]:
shows "wq (e#s) cs' = wq s cs'"
using assms unfolding is_set wq_def
by (auto simp:Let_def)
@@ -496,7 +665,7 @@
context valid_trace
begin
-lemma actor_inv:
+lemma actor_inv: (* ccc *)
assumes "PIP s e"
and "\<not> isCreate e"
shows "actor e \<in> runing s"
@@ -586,7 +755,7 @@
thus ?thesis by auto
qed (insert assms, auto simp:wq_def Let_def split:if_splits)
-lemma wq_out_inv:
+lemma wq_out_inv: (* ccc *)
assumes s_in: "thread \<in> set (wq s cs)"
and s_hd: "thread = hd (wq s cs)"
and s_i: "thread \<noteq> hd (wq (e#s) cs)"
@@ -996,10 +1165,6 @@
thus "x \<noteq> []" using rest_nnl by auto
qed
-definition "taker = hd wq'"
-
-definition "rest' = tl wq'"
-
lemma eq_wq': "wq' = taker # rest'"
by (simp add: neq_wq' rest'_def taker_def)
@@ -1605,17 +1770,10 @@
end
-locale valid_trace_p_h = valid_trace_p +
- assumes we: "wq s cs = []"
-
-locale valid_trace_p_w = valid_trace_p +
- assumes wne: "wq s cs \<noteq> []"
+
+context valid_trace_p_w
begin
-definition "holder = hd (wq s cs)"
-definition "waiters = tl (wq s cs)"
-definition "waiters' = waiters @ [th]"
-
lemma wq_s_cs: "wq s cs = holder#waiters"
by (simp add: holder_def waiters_def wne)
@@ -2235,6 +2393,11 @@
by (simp add: subtree_def the_preced_def)
qed
+
+lemma (in valid_trace) finite_threads:
+ shows "finite (threads s)"
+using vt by (induct) (auto elim: step.cases)
+
lemma cp_le:
assumes th_in: "th \<in> threads s"
shows "cp s th \<le> Max (the_preced s ` threads s)"
@@ -3212,7 +3375,7 @@
lemma not_waiting_th_s [simp]: "\<not> waiting s th cs'"
proof
assume "waiting s th cs'"
- from this[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
+ from this[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
have "th \<in> set (wq s cs')" by auto
from wq_threads[OF this] have "th \<in> threads s" .
with th_not_live_s show False by simp
@@ -3221,7 +3384,7 @@
lemma not_holding_th_s [simp]: "\<not> holding s th cs'"
proof
assume "holding s th cs'"
- from this[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp]
+ from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept]
have "th \<in> set (wq s cs')" by auto
from wq_threads[OF this] have "th \<in> threads s" .
with th_not_live_s show False by simp
@@ -3230,7 +3393,7 @@
lemma not_waiting_th_es [simp]: "\<not> waiting (e#s) th cs'"
proof
assume "waiting (e # s) th cs'"
- from this[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
+ from this[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
have "th \<in> set (wq s cs')" by auto
from wq_threads[OF this] have "th \<in> threads s" .
with th_not_live_s show False by simp
@@ -3239,7 +3402,7 @@
lemma not_holding_th_es [simp]: "\<not> holding (e#s) th cs'"
proof
assume "holding (e # s) th cs'"
- from this[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp]
+ from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept]
have "th \<in> set (wq s cs')" by auto
from wq_threads[OF this] have "th \<in> threads s" .
with th_not_live_s show False by simp
@@ -3274,13 +3437,13 @@
assume h: "cs' \<in> ?L"
hence "cs' \<in> ?R"
by (unfold holdents_def s_holding_def, fold wq_def,
- unfold wq_neq_simp, auto)
+ unfold wq_kept, auto)
} moreover {
fix cs'
assume h: "cs' \<in> ?R"
hence "cs' \<in> ?L"
by (unfold holdents_def s_holding_def, fold wq_def,
- unfold wq_neq_simp, auto)
+ unfold wq_kept, auto)
} ultimately show ?thesis by auto
qed
@@ -3300,7 +3463,7 @@
have n_wait: "\<not> waiting (e#s) th' cs'"
using assms by (auto simp:readys_def)
from wait[unfolded s_waiting_def, folded wq_def]
- n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
+ n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
have False by auto
} thus ?thesis using assms
by (unfold readys_def, auto)
@@ -3315,7 +3478,7 @@
assume wait: "waiting (e#s) th' cs'"
have n_wait: "\<not> waiting s th' cs'"
using assms(2) by (auto simp:readys_def)
- from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
+ from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
n_wait[unfolded s_waiting_def, folded wq_def]
have False by auto
} with assms show ?thesis
@@ -3388,7 +3551,7 @@
lemma not_holding_th_es [simp]: "\<not> holding (e#s) th cs'"
proof
assume "holding (e # s) th cs'"
- from this[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp]
+ from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept]
have "holding s th cs'"
by (unfold s_holding_def, fold wq_def, auto)
with not_holding_th_s
@@ -3421,13 +3584,13 @@
assume h: "cs' \<in> ?L"
hence "cs' \<in> ?R"
by (unfold holdents_def s_holding_def, fold wq_def,
- unfold wq_neq_simp, auto)
+ unfold wq_kept, auto)
} moreover {
fix cs'
assume h: "cs' \<in> ?R"
hence "cs' \<in> ?L"
by (unfold holdents_def s_holding_def, fold wq_def,
- unfold wq_neq_simp, auto)
+ unfold wq_kept, auto)
} ultimately show ?thesis by auto
qed
@@ -3447,7 +3610,7 @@
have n_wait: "\<not> waiting (e#s) th' cs'"
using assms by (auto simp:readys_def)
from wait[unfolded s_waiting_def, folded wq_def]
- n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
+ n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
have False by auto
} thus ?thesis using assms
by (unfold readys_def, auto)
@@ -3462,7 +3625,7 @@
assume wait: "waiting (e#s) th' cs'"
have n_wait: "\<not> waiting s th' cs'"
using assms(2) by (auto simp:readys_def)
- from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
+ from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
n_wait[unfolded s_waiting_def, folded wq_def]
have False by auto
} with assms show ?thesis
@@ -3526,13 +3689,13 @@
assume h: "cs' \<in> ?L"
hence "cs' \<in> ?R"
by (unfold holdents_def s_holding_def, fold wq_def,
- unfold wq_neq_simp, auto)
+ unfold wq_kept, auto)
} moreover {
fix cs'
assume h: "cs' \<in> ?R"
hence "cs' \<in> ?L"
by (unfold holdents_def s_holding_def, fold wq_def,
- unfold wq_neq_simp, auto)
+ unfold wq_kept, auto)
} ultimately show ?thesis by auto
qed
@@ -3554,7 +3717,7 @@
have n_wait: "\<not> waiting (e#s) th' cs'"
using assms by (auto simp:readys_def)
from wait[unfolded s_waiting_def, folded wq_def]
- n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
+ n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
have False by auto
} moreover have "th' \<in> threads s"
using assms[unfolded readys_def] by auto
@@ -3570,7 +3733,7 @@
assume wait: "waiting (e#s) th' cs'"
have n_wait: "\<not> waiting s th' cs'"
using assms by (auto simp:readys_def)
- from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
+ from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
n_wait[unfolded s_waiting_def, folded wq_def]
have False by auto
} with assms show ?thesis