--- a/CpsG.thy Tue Oct 06 18:52:04 2015 +0800
+++ b/CpsG.thy Sat Oct 17 16:10:33 2015 +0800
@@ -1,8 +1,12 @@
-
+section {*
+ This file contains lemmas used to guide the recalculation of current precedence
+ after every system call (or system operation)
+*}
theory CpsG
imports PrioG Max
begin
+(* obvious lemma *)
lemma not_thread_holdents:
fixes th s
assumes vt: "vt s"
@@ -126,8 +130,7 @@
qed
qed
-
-
+(* obvious lemma *)
lemma next_th_neq:
assumes vt: "vt s"
and nt: "next_th s th cs th'"
@@ -155,6 +158,7 @@
qed
qed
+(* obvious lemma *)
lemma next_th_unique:
assumes nt1: "next_th s th cs th1"
and nt2: "next_th s th cs th2"
@@ -170,8 +174,6 @@
from acyclic_RAG[OF vt] show "acyclic (RAG s)" .
qed
-
-
definition child :: "state \<Rightarrow> (node \<times> node) set"
where "child s \<equiv>
{(Th th', Th th) | th th'. \<exists>cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"
@@ -310,11 +312,15 @@
qed
qed
+text {* (* ??? *)
+*}
lemma child_RAG_eq:
assumes vt: "vt s"
shows "(Th th1, Th th2) \<in> (child s)^+ \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"
by (auto intro: RAG_child[OF vt] child_RAG_p)
+text {* (* ??? *)
+*}
lemma children_no_dep:
fixes s th th1 th2 th3
assumes vt: "vt s"
@@ -348,6 +354,8 @@
qed
qed
+text {* (* ??? *)
+*}
lemma unique_RAG_p:
assumes vt: "vt s"
and dp1: "(n, n1) \<in> (RAG s)^+"
@@ -359,6 +367,8 @@
show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto
qed
+text {* (* ??? *)
+*}
lemma dependants_child_unique:
fixes s th th1 th2 th3
assumes vt: "vt s"
@@ -395,6 +405,8 @@
apply (unfold children_def)
by (metis assms(2) children_def RAG_children eq_RAG)
+text {* (* ??? *)
+*}
lemma dependants_expand:
assumes "vt s"
shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"
@@ -435,6 +447,8 @@
shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"
by auto
+text {* (* ??? *)
+*}
lemma cp_rec:
fixes s th
assumes vt: "vt s"
@@ -902,8 +916,6 @@
qed
-
-
locale step_v_cps =
fixes s' th cs s
defines s_def : "s \<equiv> (V th cs#s')"
--- 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
--- a/PrioGDef.thy Tue Oct 06 18:52:04 2015 +0800
+++ b/PrioGDef.thy Sat Oct 17 16:10:33 2015 +0800
@@ -1,3 +1,4 @@
+chapter {* Definitions *}
(*<*)
theory PrioGDef
imports Precedence_ord Moment
@@ -70,15 +71,28 @@
-- {* Other kind of events does not affect the value of @{text "threads"}: *}
"threads (e#s) = threads s"
+text {*
+ \noindent
+ The function @{text "threads"} defined above is one of
+ the so called {\em observation function}s which forms
+ the very basis of Paulson's inductive protocol verification method.
+ Each observation function {\em observes} one particular aspect (or attribute)
+ of the system. For example, the attribute observed by @{text "threads s"}
+ is the set of threads living in state @{text "s"}.
+ The protocol being modelled
+ The decision made the protocol being modelled is based on the {\em observation}s
+ returned by {\em observation function}s. Since {\observation function}s forms
+ the very basis on which Paulson's inductive method is based, there will be
+ a lot of such observation functions introduced in the following. In fact, any function
+ which takes event list as argument is a {\em observation function}.
+ *}
+
text {* \noindent
- Functions such as @{text "threads"}, which extract information out of system states, are called
- {\em observing functions}. A series of observing functions will be defined in the sequel in order to
- model the protocol.
- Observing function @{text "priority"} calculates
- the {\em original priority} of thread @{text "th"} in state @{text "s"}, expressed as
- : @{text "priority th s" }. The {\em original priority} is the priority
+ Observation @{text "priority th s"} is
+ the {\em original priority} of thread @{text "th"} in state @{text "s"}.
+ The {\em original priority} is the priority
assigned to a thread when it is created or when it is reset by system call
- @{text "Set thread priority"}.
+ (represented by event @{text "Set thread priority"}).
*}
fun priority :: "thread \<Rightarrow> state \<Rightarrow> priority"
@@ -93,8 +107,7 @@
text {*
\noindent
- In the following,
- @{text "last_set th s"} is the last time when the priority of thread @{text "th"} is set,
+ Observation @{text "last_set th s"} is the last time when the priority of thread @{text "th"} is set,
observed from state @{text "s"}.
The time in the system is measured by the number of events happened so far since the very beginning.
*}
@@ -177,17 +190,6 @@
cs_dependants_def:
"dependants (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}"
-text {*
- The data structure used by the operating system for scheduling is referred to as
- {\em schedule state}. It is represented as a record consisting of
- a function assigning waiting queue to resources
- (to be used as the @{text "wq"} argument in @{text "holding"}, @{text "waiting"}
- and @{text "RAG"}, etc) and a function assigning precedence to threads:
- *}
-
-record schedule_state =
- wq_fun :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *}
- cprec_fun :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *}
text {* \noindent
The following
@@ -203,6 +205,15 @@
definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"
where "cpreced wq s = (\<lambda>th. Max ((\<lambda>th'. preced th' s) ` ({th} \<union> dependants wq th)))"
+text {*
+ Notice that the current precedence (@{text "cpreced"}) of one thread @{text "th"} can be boosted
+ (becoming larger than its own precedence) by those threads in
+ the @{text "dependants wq th"}-set. If one thread get boosted, we say
+ it inherits the priority (or, more precisely, the precedence) of
+ its dependants. This is how the word "Inheritance" in
+ Priority Inheritance Protocol comes.
+*}
+
(*<*)
lemma
cpreced_def2:
@@ -213,13 +224,6 @@
by (auto)
(*>*)
-(*
-abbreviation
- "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)"
-
-abbreviation
- "initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0"
-*)
text {* \noindent
Assuming @{text "qs"} be the waiting queue of a critical resource,
@@ -242,16 +246,53 @@
release resource does not affect the correctness of the PIP protocol.
*}
-(* ccc *)
+text {*
+ The data structure used by the operating system for scheduling is referred to as
+ {\em schedule state}. It is represented as a record consisting of
+ a function assigning waiting queue to resources
+ (to be used as the @{text "wq"} argument in @{text "holding"}, @{text "waiting"}
+ and @{text "RAG"}, etc) and a function assigning precedence to threads:
+ *}
+
+record schedule_state =
+ wq_fun :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *}
+ cprec_fun :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *}
text {* \noindent
- The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}
- out of the current system state @{text "s"}.
- It is the central function to model Priority Inheritance:
+ The following two abbreviations (@{text "all_unlocked"} and @{text "initial_cprec"})
+ are used to set the initial values of the @{text "wq_fun"} @{text "cprec_fun"} fields
+ respectively of the @{text "schedule_state"} record by the following function @{text "sch"},
+ which is used to calculate the system's {\em schedule state}.
+
+ Since there is no thread at the very beginning to make request, all critical resources
+ are free (or unlocked). This status is represented by the abbreviation
+ @{text "all_unlocked"}.
+ *}
+abbreviation
+ "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)"
+
+
+text {* \noindent
+ The initial current precedence for a thread can be anything, because there is no thread then.
+ We simply assume every thread has precedence @{text "Prc 0 0"}.
+ *}
+
+abbreviation
+ "initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0"
+
+
+text {* \noindent
+ The following function @{text "schs"} is used to calculate the system's schedule state @{text "schs s"}
+ out of the current system state @{text "s"}. It is the central function to model Priority Inheritance:
*}
fun schs :: "state \<Rightarrow> schedule_state"
where
- "schs [] = (| wq_fun = \<lambda> cs. [], cprec_fun = (\<lambda>_. Prc 0 0) |)" |
+ -- {*
+ \begin{minipage}{0.9\textwidth}
+ Setting the initial value of the @{text "schedule_state"} record (see the explanations above).
+ \end{minipage}
+ *}
+ "schs [] = (| wq_fun = all_unlocked, cprec_fun = initial_cprec |)" |
-- {*
\begin{minipage}{0.9\textwidth}
@@ -276,6 +317,12 @@
function. The RAGency of precedence function on waiting queue function is the reason to
put them in the same record so that they can evolve together.
\end{enumerate}
+
+
+ The calculation of @{text "cprec_fun"} depends on the value of @{text "wq_fun"}.
+ Therefore, in the following cases, @{text "wq_fun"} is always calculated first, in
+ the name of @{text "wq"} (if @{text "wq_fun"} is not changed
+ by the happening event) or @{text "new_wq"} (if the value of @{text "wq_fun"} is changed).
\end{minipage}
*}
"schs (Create th prio # s) =
@@ -287,6 +334,12 @@
| "schs (Set th prio # s) =
(let wq = wq_fun (schs s) in
(|wq_fun = wq, cprec_fun = cpreced wq (Set th prio # s)|))"
+ -- {*
+ \begin{minipage}{0.9\textwidth}
+ Different from the forth coming cases, the @{text "wq_fun"} field of the schedule state
+ is changed. So, the new value is calculated first, in the name of @{text "new_wq"}.
+ \end{minipage}
+ *}
| "schs (P th cs # s) =
(let wq = wq_fun (schs s) in
let new_wq = wq(cs := (wq cs @ [th])) in
@@ -353,7 +406,7 @@
text {*
- The following lemma can be proved easily:
+ The following lemma can be proved easily, and the meaning is obvious.
*}
lemma
s_holding_def:
@@ -383,12 +436,19 @@
text {* \noindent
The following function @{text "runing"} calculates the set of running thread, which is the ready
- thread with the highest precedence.
+ thread with the highest precedence.
*}
definition runing :: "state \<Rightarrow> thread set"
where "runing s \<equiv> {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"
text {* \noindent
+ Notice that the definition of @{text "running"} reflects the preemptive scheduling strategy,
+ because, if the @{text "running"}-thread (the one in @{text "runing"} set)
+ lowered its precedence by resetting its own priority to a lower
+ one, it will lose its status of being the max in @{text "ready"}-set and be superseded.
+*}
+
+text {* \noindent
The following function @{text "holdents s th"} returns the set of resources held by thread
@{text "th"} in state @{text "s"}.
*}
@@ -404,16 +464,20 @@
by (simp)
text {* \noindent
- @{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in
+ Observation @{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in
state @{text "s"}:
*}
definition cntCS :: "state \<Rightarrow> thread \<Rightarrow> nat"
where "cntCS s th = card (holdents s th)"
text {* \noindent
- The fact that event @{text "e"} is eligible to happen next in state @{text "s"}
+ According to the convention of Paulson's inductive method,
+ the decision made by a protocol that event @{text "e"} is eligible to happen next under state @{text "s"}
is expressed as @{text "step s e"}. The predicate @{text "step"} is inductively defined as
- follows:
+ follows (notice how the decision is based on the {\em observation function}s
+ defined above, and also notice how a complicated protocol is modeled by a few simple
+ observations, and how such a kind of simplicity gives rise to improved trust on
+ faithfulness):
*}
inductive step :: "state \<Rightarrow> event \<Rightarrow> bool"
where
@@ -443,13 +507,29 @@
*}
thread_V: "\<lbrakk>thread \<in> runing s; holding s thread cs\<rbrakk> \<Longrightarrow> step s (V thread cs)" |
-- {*
- A thread can adjust its own priority as long as it is current running:
+ \begin{minipage}{0.9\textwidth}
+ A thread can adjust its own priority as long as it is current running.
+ With the resetting of one thread's priority, its precedence may change.
+ If this change lowered the precedence, according to the definition of @{text "running"}
+ function,
+ \end{minipage}
*}
thread_set: "\<lbrakk>thread \<in> runing s\<rbrakk> \<Longrightarrow> step s (Set thread prio)"
+text {*
+ In Paulson's inductive method, every protocol is defined by such a @{text "step"}
+ predicate. For instance, the predicate @{text "step"} given above
+ defines the PIP protocol. So, it can also be called "PIP".
+*}
+
+abbreviation
+ "PIP \<equiv> step"
+
+
text {* \noindent
- With predicate @{text "step"}, the fact that @{text "s"} is a legal state in
- Priority Inheritance protocol can be expressed as: @{text "vt step s"}, where
+ For any protocol defined by a @{text "step"} predicate,
+ the fact that @{text "s"} is a legal state in
+ the protocol is expressed as: @{text "vt step s"}, where
the predicate @{text "vt"} can be defined as the following:
*}
inductive vt :: "state \<Rightarrow> bool"
@@ -458,19 +538,32 @@
vt_nil[intro]: "vt []" |
-- {*
\begin{minipage}{0.9\textwidth}
- If @{text "s"} a legal state, and event @{text "e"} is eligible to happen
- in state @{text "s"}, then @{text "e#s"} is a legal state as well:
+ If @{text "s"} a legal state of the protocol defined by predicate @{text "step"},
+ and event @{text "e"} is allowed to happen under state @{text "s"} by the protocol
+ predicate @{text "step"}, then @{text "e#s"} is a new legal state rendered by the
+ happening of @{text "e"}:
\end{minipage}
*}
vt_cons[intro]: "\<lbrakk>vt s; step s e\<rbrakk> \<Longrightarrow> vt (e#s)"
text {* \noindent
It is easy to see that the definition of @{text "vt"} is generic. It can be applied to
- any step predicate to get the set of legal states.
+ any specific protocol specified by a @{text "step"}-predicate to get the set of
+ legal states of that particular protocol.
*}
+text {*
+ The following are two very basic properties of @{text "vt"}.
+*}
+
+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 {* \noindent
- The following two functions @{text "the_cs"} and @{text "the_th"} are used to extract
+ The following two auxiliary functions @{text "the_cs"} and @{text "the_th"} are used to extract
critical resource and thread respectively out of RAG nodes.
*}
fun the_cs :: "node \<Rightarrow> cs"
@@ -483,27 +576,33 @@
The following predicate @{text "next_th"} describe the next thread to
take over when a critical resource is released. In @{text "next_th s th cs t"},
@{text "th"} is the thread to release, @{text "t"} is the one to take over.
+ Notice how this definition is backed up by the @{text "release"} function and its use
+ in the @{text "V"}-branch of @{text "schs"} function. This @{text "next_th"} function
+ is not needed for the execution of PIP. It is introduced as an auxiliary function
+ to state lemmas. The correctness of this definition will be confirmed by
+ lemmas @{text "step_v_hold_inv"}, @{text " step_v_wait_inv"},
+ @{text "step_v_get_hold"} and @{text "step_v_not_wait"}.
*}
definition next_th:: "state \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> thread \<Rightarrow> bool"
where "next_th s th cs t = (\<exists> rest. wq s cs = th#rest \<and> rest \<noteq> [] \<and>
- t = hd (SOME q. distinct q \<and> set q = set rest))"
+ t = hd (SOME q. distinct q \<and> set q = set rest))"
text {* \noindent
- The function @{text "count Q l"} is used to count the occurrence of situation @{text "Q"}
+ The aux function @{text "count Q l"} is used to count the occurrence of situation @{text "Q"}
in list @{text "l"}:
*}
definition count :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat"
where "count Q l = length (filter Q l)"
text {* \noindent
- The following @{text "cntP s"} returns the number of operation @{text "P"} happened
+ The following observation @{text "cntP s"} returns the number of operation @{text "P"} happened
before reaching state @{text "s"}.
*}
definition cntP :: "state \<Rightarrow> thread \<Rightarrow> nat"
where "cntP s th = count (\<lambda> e. \<exists> cs. e = P th cs) s"
text {* \noindent
- The following @{text "cntV s"} returns the number of operation @{text "V"} happened
+ The following observation @{text "cntV s"} returns the number of operation @{text "V"} happened
before reaching state @{text "s"}.
*}
definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat"