pip: comparison PrioGDef.thy

equal deleted inserted replaced

-:8679d75b1d76
+:8142e80f5d58
+chapter {* Definitions *}
 (*<*)
 theory PrioGDef
 imports Precedence_ord Moment
 begin
 (*>*)
 -- {* Finished thread is removed: *}
 "threads (Exit thread # s) = (threads s) - {thread}" |
 -- {* Other kind of events does not affect the value of @{text "threads"}: *}
 "threads (e#s) = threads s"
-text {* \noindent
+text {*
-Functions such as @{text "threads"}, which extract information out of system states, are called
+\noindent
-{\em observing functions}. A series of observing functions will be defined in the sequel in order to
+The function @{text "threads"} defined above is one of
-model the protocol.
+the so called {\em observation function}s which forms
-Observing function @{text "priority"} calculates
+the very basis of Paulson's inductive protocol verification method.
-the {\em original priority} of thread @{text "th"} in state @{text "s"}, expressed as
+Each observation function {\em observes} one particular aspect (or attribute)
-: @{text "priority th s" }. The {\em original priority} is the priority
+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
+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"
 where
 -- {* @{text "0"} is assigned to threads which have never been created: *}
 (if thread' = thread then prio else priority thread s)" |
 "priority thread (e#s) = priority thread s"
 text {*
 \noindent
-In the following,
+Observation @{text "last_set th s"} is the last time when the priority of thread @{text "th"} is set,
-@{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.
 *}
 fun last_set :: "thread \<Rightarrow> state \<Rightarrow> nat"
 where
 \end{minipage}
 *}
 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
 @{text "cpreced s th"} gives the {\em current precedence} of thread @{text "th"} under
 state @{text "s"}. The definition of @{text "cpreced"} reflects the basic idea of
 *}
 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:
 "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants wq th})"
 unfolding cpreced_def image_def
 apply(rule eq_reflection)
 apply(rule_tac f="Max" in arg_cong)
 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,
 the following abbreviation "release qs" is the waiting queue after the thread
 holding the resource (which is thread at the head of @{text "qs"}) released
 from common sense that the thread who comes the earliest should take over.
 The intention of this definition is to show that the choice of which thread to take over the
 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
-text {* \noindent
+{\em schedule state}. It is represented as a record consisting of
-The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}
+a function assigning waiting queue to resources
-out of the current system state @{text "s"}.
+(to be used as the @{text "wq"} argument in @{text "holding"}, @{text "waiting"}
-It is the central function to model Priority Inheritance:
+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 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}
 \begin{enumerate}
 \item @{text "ps"} is the schedule state of last moment.
 \end{enumerate}
 \item @{text "ncp"} is new precedence function, it is calculated from the newly updated waiting queue
 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) =
 (let wq = wq_fun (schs s) in
 (|wq_fun = wq, cprec_fun = cpreced wq (Create th prio # s)|))"
 (let wq = wq_fun (schs s) in
 (|wq_fun = wq, cprec_fun = cpreced wq (Exit th # s)|))"
 |  "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
 (|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|))"
 |  "schs (V th cs # s) =
 s_dependants_abv:
 "dependants (s::state) \<equiv> dependants (wq_fun (schs s))"
 text {*
-The following lemma can be proved easily:
+The following lemma can be proved easily, and the meaning is obvious.
 *}
 lemma
 s_holding_def:
 "holding (s::state) th cs \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th = hd (wq_fun (schs s) cs))"
 by (auto simp:s_holding_abv wq_def cs_holding_def)
 definition readys :: "state \<Rightarrow> thread set"
 where "readys s \<equiv> {th . th \<in> threads s \<and> (\<forall> cs. \<not> waiting s th cs)}"
 text {* \noindent
 The following function @{text "runing"} calculates the set of running thread, which is the ready
 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"}.
 *}
 unfolding s_holding_abv
 unfolding wq_def
 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
 -- {*
 A thread can be created if it is not a live thread:
 if it is running and holding that resource:
 \end{minipage}
 *}
 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 {* \noindent
+text {*
-With predicate @{text "step"}, the fact that @{text "s"} is a legal state in
+In Paulson's inductive method, every protocol is defined by such a @{text "step"}
-Priority Inheritance protocol can be expressed as: @{text "vt step s"}, where
+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
+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"
 where
 -- {* Empty list @{text "[]"} is a legal state in any protocol:*}
 vt_nil[intro]: "vt []" |
 -- {*
 \begin{minipage}{0.9\textwidth}
-If @{text "s"} a legal state, and event @{text "e"} is eligible to happen
+If @{text "s"} a legal state of the protocol defined by predicate @{text "step"},
-in state @{text "s"}, then @{text "e#s"} is a legal state as well:
+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 {* \noindent
-The following two functions @{text "the_cs"} and @{text "the_th"} are used to extract
+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 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"
 where "the_cs (Cs cs) = cs"
 text {* \noindent
 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))"
 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"
 where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s"
 (*<*)

changeset 53	8142e80f5d58
parent 49	8679d75b1d76