--- 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"