pip: comparison PrioGDef.thy

equal deleted inserted replaced

-:2e6c8d530216
+:c0f14399c12f
 imports Precedence_ord Moment
 begin
 (*>*)
 text {*
-In this section, the formal model of Priority Inheritance is presented.
+In this section, the formal model of  Priority Inheritance Protocol (PIP) is presented.
 The model is based on Paulson's inductive protocol verification method, where
 the state of the system is modelled as a list of events happened so far with the latest
 event put at the head.
+*}
+text {*
 To define events, the identifiers of {\em threads},
 {\em priority} and {\em critical resources } (abbreviated as @{text "cs"})
 need to be represented. All three are represetned using standard
 Isabelle/HOL type @{typ "nat"}:
 *}
 type_synonym priority = nat  -- {* Type for priorities. *}
 type_synonym cs = nat -- {* Type for critical sections (or critical resources). *}
 text {*
 \noindent
-Every event in the system corresponds to a system call, the formats of which are
+The abstraction of Priority Inheritance Protocol (PIP) is set at the system call level.
+Every system call is represented as an event. The format of events is defined
 defined as follows:
 *}
 datatype event =
 Create thread priority | -- {* Thread @{text "thread"} is created with priority @{text "priority"}. *}
 Exit thread | -- {* Thread @{text "thread"} finishing its execution. *}
 P thread cs | -- {* Thread @{text "thread"} requesting critical resource @{text "cs"}. *}
 V thread cs | -- {* Thread @{text "thread"}  releasing critical resource @{text "cs"}. *}
 Set thread priority -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *}
+text {*
+As mentioned earlier, in Paulson's inductive method, the states of system are represented as lists of events,
+which is defined by the following type @{text "state"}:
+*}
+type_synonym state = "event list"
 text {*
 \noindent
 Resource Allocation Graph (RAG for short) is used extensively in our formal analysis.
 The following type @{text "node"} is used to represent nodes in RAG.
 *}
 datatype node =
 Th "thread" | -- {* Node for thread. *}
 Cs "cs" -- {* Node for critical resource. *}
-text {*
-In Paulson's inductive method, the states of system are represented as lists of events,
-which is defined by the following type @{text "state"}:
-*}
-type_synonym state = "event list"
 text {*
 \noindent
 The following function
 @{text "threads"} is used to calculate the set of live threads (@{text "threads s"})
 "threads (Create thread prio#s) = {thread} \<union> threads s" |
 -- {* 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
 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
 "priority thread (e#s) = priority thread s"
 text {*
 \noindent
 In the following,
-@{text "last_set th s"} is the time when thread @{text "th"} is created,
+@{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
 "last_set thread (_#s) = last_set thread s"
 text {*
 \noindent
 The {\em precedence} is a notion derived from {\em priority}, where the {\em precedence} of
-a thread is the combination of its {\em original priority} and {\em birth time}. The intention is
+a thread is the combination of its {\em original priority} and {\em time} the priority is set.
-to discriminate threads with the same priority by giving threads whose priority
+The intention is to discriminate threads with the same priority by giving threads whose priority
 is assigned earlier higher precedences, becasue such threads are more urgent to finish.
 This explains the following definition:
 *}
 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
 where "preced thread s \<equiv> Prc (priority thread s) (last_set thread s)"
 text {*
 \noindent
-A number of important notions are defined here:
+A number of important notions in PIP are represented as functions defined
+in terms of the waiting queues of the system, where the waiting queues
+, as a whole, is represented by the @{text "wq"} argument of every notion function.
+The @{text "wq"} argument is itself a functions which
+maps every critical resource @{text "cs"} to the list of threads which are holding or waiting for it.
+The thread at the head of this list is designated as the thread which is current
+holding the resrouce, which is slightly different from tradition where
+all threads in the waiting queue are considered as waiting for the resource.
 *}
 consts
 holding :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"
 waiting :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"
 RAG :: "'b \<Rightarrow> (node \<times> node) set"
 dependants :: "'b \<Rightarrow> thread \<Rightarrow> thread set"
-text {*
-\noindent
-In the definition of the following several functions, it is supposed that
-the waiting queue of every critical resource is given by a waiting queue
-function @{text "wq"}, which servers as arguments of these functions.
-*}
 defs (overloaded)
 -- {*
 \begin{minipage}{0.9\textwidth}
-We define that the thread which is at the head of waiting queue of resource @{text "cs"}
+This meaning of @{text "wq"} is reflected in the following definition of @{text "holding wq th cs"},
-is holding the resource. This definition is slightly different from tradition where
+where @{text "holding wq th cs"} means thread @{text "th"} is holding the critical
-all threads in the waiting queue are considered as waiting for the resource.
+resource @{text "cs"}. This decision is based on @{text "wq"}.
-This notion is reflected in the definition of @{text "holding wq th cs"} as follows:
+\end{minipage}
-\end{minipage}
+*}
-*}
 cs_holding_def:
 "holding wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread = hd (wq cs))"
 -- {*
 \begin{minipage}{0.9\textwidth}
 In accordance with the definition of @{text "holding wq th cs"},
 *}
 cs_waiting_def:
 "waiting wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"
 -- {*
 \begin{minipage}{0.9\textwidth}
-@{text "RAG wq"} represents the Resource Allocation Graph of the system under the waiting
+@{text "RAG wq"} generates RAG (a binary relations on @{text "node"})
-queue function @{text "wq"}.
+out of waiting queues of the system (represented by the @{text "wq"} argument):
 \end{minipage}
 *}
 cs_RAG_def:
 "RAG (wq::cs \<Rightarrow> thread list) \<equiv>
 {(Th th, Cs cs) | th cs. waiting wq th cs} \<union> {(Cs cs, Th th) | cs th. holding wq th cs}"
 -- {*
 \begin{minipage}{0.9\textwidth}
 The following @{text "dependants wq th"} represents the set of threads which are RAGing on
-thread @{text "th"} in Resource Allocation Graph @{text "RAG wq"}:
+thread @{text "th"} in Resource Allocation Graph @{text "RAG wq"}.
+Here, "RAGing" means waiting directly or indirectly on the critical resource.
 \end{minipage}
 *}
 cs_dependants_def:
 "dependants (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}"
+(* I stop here for the moment 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 and a function assigning precedence to

changeset 48	c0f14399c12f
parent 35	92f61f6a0fe7
child 49	8679d75b1d76