pip: comparison PIPBasics.thy

equal deleted inserted replaced

-:524bd3caa6b6
+:f7b33c633b96
 theory PIPBasics
 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"
 proof
 also from assms have "... = ?L"
 by (subst Max.insert, simp+)
 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"
 using assms
 proof(induct s)
 thus ?thesis by simp
 qed
 thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)
 qed
+lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
+by (unfold s_RAG_def, auto)
+lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
+by  (unfold s_waiting_def cs_waiting_def wq_def, auto)
+lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs"
+by (unfold s_holding_def wq_def cs_holding_def, simp)
+lemma runing_ready:
+shows "runing s \<subseteq> readys s"
+unfolding runing_def readys_def
+by auto
+lemma readys_threads:
+shows "readys s \<subseteq> threads s"
+unfolding readys_def
+by auto
+lemma wq_v_neq [simp]:
+"cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'"
+by (auto simp:wq_def Let_def cp_def split:list.splits)
+lemma runing_head:
+assumes "th \<in> runing s"
+and "th \<in> set (wq_fun (schs s) cs)"
+shows "th = hd (wq_fun (schs s) cs)"
+using assms
+by (simp add:runing_def readys_def s_waiting_def wq_def)
+lemma runing_wqE:
+assumes "th \<in> runing s"
+and "th \<in> set (wq s cs)"
+obtains rest where "wq s cs = th#rest"
+proof -
+from assms(2) obtain th' rest where eq_wq: "wq s cs = th'#rest"
+by (meson list.set_cases)
+have "th' = th"
+proof(rule ccontr)
+assume "th' \<noteq> th"
+hence "th \<noteq> hd (wq s cs)" using eq_wq by auto
+with assms(2)
+have "waiting s th cs"
+by (unfold s_waiting_def, fold wq_def, auto)
+with assms show False
+by (unfold runing_def readys_def, auto)
+qed
+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 +
 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
-locale valid_trace_v_e = valid_trace_v +
-assumes rest_nil: "rest = []"
+text {*
+The following @{text "taker"} is the thread to
-locale valid_trace_set= valid_trace_e +
+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"
 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
 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"
+text {*
-by (unfold s_RAG_def, auto)
+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)
-lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
-by  (unfold s_waiting_def cs_waiting_def wq_def, auto)
-lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs"
-by (unfold s_holding_def wq_def cs_holding_def, simp)
-lemma runing_ready:
-shows "runing s \<subseteq> readys s"
-unfolding runing_def readys_def
-by auto
-lemma readys_threads:
-shows "readys s \<subseteq> threads s"
-unfolding readys_def
-by auto
-lemma wq_v_neq [simp]:
-"cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'"
-by (auto simp:wq_def Let_def cp_def split:list.splits)
-lemma runing_head:
-assumes "th \<in> runing s"
-and "th \<in> set (wq_fun (schs s) cs)"
-shows "th = hd (wq_fun (schs s) cs)"
-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)"
-obtains rest where "wq s cs = th#rest"
-proof -
-from assms(2) obtain th' rest where eq_wq: "wq s cs = th'#rest"
-by (meson list.set_cases)
-have "th' = th"
-proof(rule ccontr)
-assume "th' \<noteq> th"
-hence "th \<noteq> hd (wq s cs)" using eq_wq by auto
-with assms(2)
-have "waiting s th cs"
-by (unfold s_waiting_def, fold wq_def, auto)
-with assms show False
-by (unfold runing_def readys_def, auto)
-qed
-with eq_wq that show ?thesis by metis
-qed
-end
 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)
 lemma wq_distinct_kept:
 end
 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)
 lemma wq_distinct_kept:
 assumes "distinct (wq s cs')"
 shows "distinct (wq (e#s) cs')"
 using assms by simp
 end
-context valid_trace_p
+context valid_trace_p (* ccc *)
 begin
 lemma wq_neq_simp [simp]:
 assumes "cs' \<noteq> cs"
 shows "wq (e#s) cs' = wq s cs'"
 end
 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)
 lemma wq_distinct_kept:
 end
 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"
 using assms
 by (induct, 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)
-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)"
 shows "e = V thread cs"
 proof(cases e)
 next
 fix x
 assume " distinct x \<and> set x = set rest"
 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)
 lemma next_th_taker:
 by (simp add: cs_holding_def holding_eq)
 qed
 end
-locale valid_trace_p_h = valid_trace_p +
-assumes we: "wq s cs = []"
+context valid_trace_p_w
-locale valid_trace_p_w = valid_trace_p +
-assumes wne: "wq s cs \<noteq> []"
 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)
 lemma wq_es_cs': "wq (e#s) cs = holder#waiters@[th]"
 by (simp add: finite_subtree_threads)
 next
 show "preced th s \<in> the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}"
 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)"
 proof(unfold cp_alt_def, rule Max_f_mono)
 by (unfold is_create, simp)
 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
 qed
 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
 qed
 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
 qed
 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
 qed
 proof -
 { fix cs'
 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
 lemma cntCS_kept [simp]:
 assumes "th' \<noteq> th"
 { fix cs'
 assume wait: "waiting s th' cs'"
 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)
 qed
 proof -
 { fix cs'
 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
 by (unfold readys_def, auto)
 qed
 qed
 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
 show False by simp
 qed
 proof -
 { fix cs'
 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
 lemma cntCS_kept [simp]:
 assumes "th' \<noteq> th"
 { fix cs'
 assume wait: "waiting s th' cs'"
 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)
 qed
 proof -
 { fix cs'
 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
 by (unfold readys_def, auto)
 qed
 proof -
 { fix cs'
 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
 lemma cntCS_kept [simp]:
 shows "cntCS (e#s) th' = cntCS s th'" (is "?L = ?R")
 { fix cs'
 assume wait: "waiting s th' cs'"
 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
 ultimately show ?thesis
 by (unfold readys_def, auto)
 proof -
 { fix cs'
 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
 by (unfold readys_def, auto)
 qed

changeset 99	f7b33c633b96
parent 93	524bd3caa6b6
child 100	3d2b59f15f26