--- a/PrioG.thy Tue Oct 06 18:52:04 2015 +0800
+++ b/PrioG.thy Sat Oct 17 16:10:33 2015 +0800
@@ -51,11 +51,12 @@
qed
qed
-lemma step_back_vt: "vt (e#s) \<Longrightarrow> vt s"
- by(ind_cases "vt (e#s)", simp)
-
-lemma step_back_step: "vt (e#s) \<Longrightarrow> step s e"
- by(ind_cases "vt (e#s)", simp)
+text {*
+ The following lemma shows that only the @{text "P"}
+ operation can add new thread into waiting queues.
+ Such kind of lemmas are very obvious, but need to be checked formally.
+ This is a kind of confirmation that our modelling is correct.
+*}
lemma block_pre:
fixes thread cs s
@@ -111,6 +112,13 @@
qed
qed
+text {*
+ The following lemmas is also obvious and shallow. It says
+ that only running thread can request for a critical resource
+ and that the requested resource must be one which is
+ not current held by the thread.
+*}
+
lemma p_pre: "\<lbrakk>vt ((P thread cs)#s)\<rbrakk> \<Longrightarrow>
thread \<in> runing s \<and> (Cs cs, Th thread) \<notin> (RAG s)^+"
apply (ind_cases "vt ((P thread cs)#s)")
@@ -202,6 +210,39 @@
lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"
*)
+text {* (* ??? *)
+ 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 lose 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.
+*}
+
lemma waiting_unique_pre:
fixes cs1 cs2 s thread
assumes vt: "vt s"
@@ -252,6 +293,7 @@
case True
from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
by auto
+ thm abs2
from abs2 [OF vt_e True eq_th h2 h1]
show ?thesis by auto
next
@@ -354,6 +396,10 @@
qed
qed
+text {*
+ This lemma is a simple corrolary of @{text "waiting_unique_pre"}.
+*}
+
lemma waiting_unique:
fixes s cs1 cs2
assumes "vt s"
@@ -365,6 +411,11 @@
by auto
(* not used *)
+text {*
+ Every thread can only be blocked on one critical resource,
+ symmetrically, every critical resource can only be held by one thread.
+ This fact is much more easier according to our definition.
+*}
lemma held_unique:
fixes s::"state"
assumes "holding s th1 cs"
@@ -407,6 +458,7 @@
thus ?thesis by auto
qed
+(* An aux lemma used later *)
lemma unique_minus:
fixes x y z r
assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
@@ -501,6 +553,12 @@
qed
qed
+text {*
+ The following three lemmas show that @{text "RAG"} does not change
+ by the happening of @{text "Set"}, @{text "Create"} and @{text "Exit"}
+ events, respectively.
+*}
+
lemma RAG_set_unchanged: "(RAG (Set th prio # s)) = RAG s"
apply (unfold s_RAG_def s_waiting_def wq_def)
by (simp add:Let_def)
@@ -514,10 +572,17 @@
by (simp add:Let_def)
-
+text {*
+ The following lemmas are used in the proof of
+ lemma @{text "step_RAG_v"}, which characterizes how the @{text "RAG"} is changed
+ by @{text "V"}-events.
+ However, since our model is very concise, such seemingly obvious lemmas need to be derived from scratch,
+ starting from the model definitions.
+*}
lemma step_v_hold_inv[elim_format]:
"\<And>c t. \<lbrakk>vt (V th cs # s);
- \<not> holding (wq s) t c; holding (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> next_th s th cs t \<and> c = cs"
+ \<not> holding (wq s) t c; holding (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow>
+ next_th s th cs t \<and> c = cs"
proof -
fix c t
assume vt: "vt (V th cs # s)"
@@ -564,6 +629,10 @@
qed
qed
+text {*
+ The following @{text "step_v_wait_inv"} is also an obvious lemma, which, however, needs to be
+ derived from scratch, which confirms the correctness of the definition of @{text "next_th"}.
+*}
lemma step_v_wait_inv[elim_format]:
"\<And>t c. \<lbrakk>vt (V th cs # s); \<not> waiting (wq (V th cs # s)) t c; waiting (wq s) t c
\<rbrakk>
@@ -773,6 +842,10 @@
qed
qed
+text {* (* ??? *)
+ The following @{text "step_RAG_v"} lemma charaterizes how @{text "RAG"} is changed
+ with the happening of @{text "V"}-events:
+*}
lemma step_RAG_v:
fixes th::thread
assumes vt:
@@ -790,6 +863,10 @@
apply (erule_tac step_v_not_wait, auto)
done
+text {*
+ The following @{text "step_RAG_p"} lemma charaterizes how @{text "RAG"} is changed
+ with the happening of @{text "P"}-events:
+*}
lemma step_RAG_p:
"vt (P th cs#s) \<Longrightarrow>
RAG (P th cs # s) = (if (wq s cs = []) then RAG s \<union> {(Cs cs, Th th)}
@@ -808,6 +885,12 @@
lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
by (unfold s_RAG_def, auto)
+text {*
+ The following lemma shows that @{text "RAG"} is acyclic.
+ The overall structure is by induction on the formation of @{text "vt s"}
+ and then case analysis on event @{text "e"}, where the non-trivial cases
+ for those for @{text "V"} and @{text "P"} events.
+*}
lemma acyclic_RAG:
fixes s
assumes vt: "vt s"
@@ -1218,6 +1301,12 @@
qed
qed
+text {* \noindent
+ The following lemmas shows that: starting from any node in @{text "RAG"},
+ by chasing out-going edges, it is always possible to reach a node representing a ready
+ thread. In this lemma, it is the @{text "th'"}.
+*}
+
lemma chain_building:
assumes vt: "vt s"
shows "node \<in> Domain (RAG s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (RAG s)^+)"
@@ -1269,6 +1358,9 @@
qed
qed
+text {* \noindent
+ The following is just an instance of @{text "chain_building"}.
+*}
lemma th_chain_to_ready:
fixes s th
assumes vt: "vt s"
@@ -1452,6 +1544,11 @@
ultimately show ?thesis by (simp add:cntCS_def)
qed
+text {* (* ??? *) \noindent
+ The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"}
+ of one particular thread.
+*}
+
lemma cnp_cnv_cncs:
fixes s th
assumes vt: "vt s"
@@ -2294,8 +2391,6 @@
apply (metis insertCI runing_unique)
apply(auto)
done
-
-
lemma create_pre:
assumes stp: "step s e"
@@ -2360,74 +2455,7 @@
assumes "vt s"
and "th \<notin> threads s"
shows "cntP s th = cntV s th"
-proof -
- from assms show ?thesis
- proof(induct)
- case (vt_cons s e)
- have ih: "th \<notin> threads s \<Longrightarrow> cntP s th = cntV s th" by fact
- have not_in: "th \<notin> threads (e # s)" by fact
- have "step s e" by fact
- thus ?case proof(cases)
- case (thread_create thread prio)
- assume eq_e: "e = Create thread prio"
- hence "thread \<in> threads (e#s)" by simp
- with not_in and eq_e have "th \<notin> threads s" by auto
- from ih [OF this] show ?thesis using eq_e
- by (auto simp:cntP_def cntV_def count_def)
- next
- case (thread_exit thread)
- assume eq_e: "e = Exit thread"
- and not_holding: "holdents s thread = {}"
- have vt_s: "vt s" by fact
- from finite_holding[OF vt_s] have "finite (holdents s thread)" .
- with not_holding have "cntCS s thread = 0" by (unfold cntCS_def, auto)
- moreover have "thread \<in> readys s" using thread_exit by (auto simp:runing_def)
- moreover note cnp_cnv_cncs[OF vt_s, of thread]
- ultimately have eq_thread: "cntP s thread = cntV s thread" by auto
- show ?thesis
- proof(cases "th = thread")
- case True
- with eq_thread eq_e show ?thesis
- by (auto simp:cntP_def cntV_def count_def)
- next
- case False
- with not_in and eq_e have "th \<notin> threads s" by simp
- from ih[OF this] and eq_e show ?thesis
- by (auto simp:cntP_def cntV_def count_def)
- qed
- next
- case (thread_P thread cs)
- assume eq_e: "e = P thread cs"
- have "thread \<in> runing s" by fact
- with not_in eq_e have neq_th: "thread \<noteq> th"
- by (auto simp:runing_def readys_def)
- from not_in eq_e have "th \<notin> threads s" by simp
- from ih[OF this] and neq_th and eq_e show ?thesis
- by (auto simp:cntP_def cntV_def count_def)
- next
- case (thread_V thread cs)
- assume eq_e: "e = V thread cs"
- have "thread \<in> runing s" by fact
- with not_in eq_e have neq_th: "thread \<noteq> th"
- by (auto simp:runing_def readys_def)
- from not_in eq_e have "th \<notin> threads s" by simp
- from ih[OF this] and neq_th and eq_e show ?thesis
- by (auto simp:cntP_def cntV_def count_def)
- next
- case (thread_set thread prio)
- assume eq_e: "e = Set thread prio"
- and "thread \<in> runing s"
- hence "thread \<in> threads (e#s)"
- by (simp add:runing_def readys_def)
- with not_in and eq_e have "th \<notin> threads s" by auto
- from ih [OF this] show ?thesis using eq_e
- by (auto simp:cntP_def cntV_def count_def)
- qed
- next
- case vt_nil
- show ?case by (auto simp:cntP_def cntV_def count_def)
- qed
-qed
+ by (simp add: assms(1) assms(2) cnp_cnv_cncs not_thread_cncs)
lemma eq_RAG:
"RAG (wq s) = RAG s"
@@ -2764,6 +2792,10 @@
qed
qed
+text {* (* ccc *) \noindent
+ Since the current precedence of the threads in ready queue will always be boosted,
+ there must be one inside it has the maximum precedence of the whole system.
+*}
lemma max_cp_readys_threads:
assumes vt: "vt s"
shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
@@ -2880,4 +2912,9 @@
shows "(detached s th) = (cntP s th = cntV s th)"
by (insert vt, auto intro:detached_intro detached_elim)
+text {*
+ The lemmas in this .thy file are all obvious lemmas, however, they still needs to be derived
+ from the concise and miniature model of PIP given in PrioGDef.thy.
+*}
+
end