diff -r 12e9aa68d5db -r 4190df6f4488 prio/PrioGDef.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/prio/PrioGDef.thy	Tue Jan 24 00:20:09 2012 +0000
@@ -0,0 +1,401 @@
+(*<*)
+theory PrioGDef
+imports Precedence_ord Moment
+begin
+(*>*)
+
+text {*
+  In this section, the formal model of Priority Inheritance 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. 
+
+  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 thread = nat -- {* Type for thread identifiers. *}
+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
+  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 {* 
+\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"})
+  in state @{text "s"}.
+  *}
+fun threads :: "state \<Rightarrow> thread set"
+  where 
+  -- {* At the start of the system, the set of threads is empty: *}
+  "threads [] = {}" | 
+  -- {* New thread is added to the @{text "threads"}: *}
+  "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 "original_priority"} calculates 
+  the {\em original priority} of thread @{text "th"} in state @{text "s"}, expressed as
+  : @{text "original_priority th 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"}.
+*}
+
+fun original_priority :: "thread \<Rightarrow> state \<Rightarrow> priority"
+  where
+  -- {* @{text "0"} is assigned to threads which have never been created: *}
+  "original_priority thread [] = 0" |
+  "original_priority thread (Create thread' prio#s) = 
+     (if thread' = thread then prio else original_priority thread s)" |
+  "original_priority thread (Set thread' prio#s) = 
+     (if thread' = thread then prio else original_priority thread s)" |
+  "original_priority thread (e#s) = original_priority thread s"
+
+text {*
+  \noindent
+  In the following,
+  @{text "birthtime th s"} is the time when thread @{text "th"} is created, 
+  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 birthtime :: "thread \<Rightarrow> state \<Rightarrow> nat"
+  where
+  "birthtime thread [] = 0" |
+  "birthtime thread ((Create thread' prio)#s) = 
+       (if (thread = thread') then length s else birthtime thread s)" |
+  "birthtime thread ((Set thread' prio)#s) = 
+       (if (thread = thread') then length s else birthtime thread s)" |
+  "birthtime thread (e#s) = birthtime 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
+  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 = Prc (original_priority thread s) (birthtime thread s)"
+
+
+text {*
+  \noindent
+  A number of important notions are defined here:
+  *}
+
+consts 
+  holding :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool" 
+  waiting :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"
+  depend :: "'b \<Rightarrow> (node \<times> node) set"
+  dependents :: "'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"}
+  is holding the resource. This definition is slightly different from tradition where
+  all threads in the waiting queue are considered as waiting for the resource.
+  This notion is reflected in the definition of @{text "holding wq th cs"} as follows:
+  \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"}, 
+  a thread @{text "th"} is considered waiting for @{text "cs"} if 
+  it is in the {\em waiting queue} of critical resource @{text "cs"}, but not at the head.
+  This is reflected in the definition of @{text "waiting wq th cs"} as follows:
+  \end{minipage}
+  *}
+  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 "depend wq"} represents the Resource Allocation Graph of the system under the waiting 
+  queue function @{text "wq"}.
+  \end{minipage}
+  *}
+  cs_depend_def: 
+  "depend (wq::cs \<Rightarrow> thread list) \<equiv>
+      {(Th t, Cs c) | t c. waiting wq t c} \<union> {(Cs c, Th t) | c t. holding wq t c}"
+  -- {* 
+  \begin{minipage}{0.9\textwidth}
+  The following @{text "dependents wq th"} represents the set of threads which are depending on
+  thread @{text "th"} in Resource Allocation Graph @{text "depend wq"}:
+  \end{minipage}
+  *}
+  cs_dependents_def: 
+  "dependents (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (depend 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 and a function assigning precedence to 
+  threads:
+  *}
+record schedule_state = 
+    waiting_queue :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *}
+    cur_preced :: "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 
+  Priority Inheritance that the {\em current precedence} of a thread is the precedence 
+  inherited from the maximum of all its dependents, i.e. the threads which are waiting 
+  directly or indirectly waiting for some resources from it. If no such thread exits, 
+  @{text "th"}'s {\em current precedence} equals its original precedence, i.e. 
+  @{text "preced th s"}.
+  *}
+definition cpreced :: "state \<Rightarrow> (cs \<Rightarrow> thread list) \<Rightarrow> thread \<Rightarrow> precedence"
+  where "cpreced s wq = (\<lambda> th. Max ((\<lambda> th. preced th s) ` ({th} \<union> dependents wq th)))"
+
+text {* \noindent
+  The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}.
+  It is the key function to model Priority Inheritance:
+  *}
+fun schs :: "state \<Rightarrow> schedule_state"
+  where "schs [] = \<lparr>waiting_queue = \<lambda> cs. [],  cur_preced = cpreced [] (\<lambda> cs. [])\<rparr>" |
+  -- {*
+  \begin{minipage}{0.9\textwidth}
+  \begin{enumerate}
+  \item @{text "ps"} is the schedule state of last moment.
+  \item @{text "pwq"} is the waiting queue function of last moment.
+  \item @{text "pcp"} is the precedence function of last moment. 
+  \item @{text "nwq"} is the new waiting queue function. It is calculated using a @{text "case"} statement:
+  \begin{enumerate}
+      \item If the happening event is @{text "P thread cs"}, @{text "thread"} is added to 
+            the end of @{text "cs"}'s waiting queue.
+      \item If the happening event is @{text "V thread cs"} and @{text "s"} is a legal state,
+            @{text "th'"} must equal to @{text "thread"}, 
+            because @{text "thread"} is the one currently holding @{text "cs"}. 
+            The case @{text "[] \<Longrightarrow> []"} may never be executed in a legal state.
+            the @{text "(SOME q. distinct q \<and> set q = set qs)"} is used to choose arbitrarily one 
+            thread in waiting to take over the released resource @{text "cs"}. In our representation,
+            this amounts to rearrange elements in waiting queue, so that one of them is put at the head.
+      \item For other happening event, the schedule state just does not change.
+  \end{enumerate}
+  \item @{text "ncp"} is new precedence function, it is calculated from the newly updated waiting queue 
+        function. The dependency 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}
+  \end{minipage}
+     *}
+   "schs (e#s) = (let ps = schs s in 
+                  let pwq = waiting_queue ps in 
+                  let pcp = cur_preced ps in
+                  let nwq = case e of
+                             P thread cs \<Rightarrow>  pwq(cs:=(pwq cs @ [thread])) |
+                             V thread cs \<Rightarrow> let nq = case (pwq cs) of
+                                                      [] \<Rightarrow> [] | 
+                                                      (th'#qs) \<Rightarrow> (SOME q. distinct q \<and> set q = set qs)
+                                            in pwq(cs:=nq)                 |
+                              _ \<Rightarrow> pwq
+                  in let ncp = cpreced (e#s) nwq in 
+                     \<lparr>waiting_queue = nwq, cur_preced = ncp\<rparr>
+                 )"
+
+text {* 
+  \noindent
+  The following @{text "wq"} is a shorthand for @{text "waiting_queue"}. 
+  *}
+definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list" 
+  where "wq s = waiting_queue (schs s)"
+
+text {* \noindent 
+  The following @{text "cp"} is a shorthand for @{text "cur_preced"}. 
+  *}
+definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"
+  where "cp s = cur_preced (schs s)"
+
+text {* \noindent
+  Functions @{text "holding"}, @{text "waiting"}, @{text "depend"} and 
+  @{text "dependents"} still have the 
+  same meaning, but redefined so that they no longer depend on the 
+  fictitious {\em waiting queue function}
+  @{text "wq"}, but on system state @{text "s"}.
+  *}
+defs (overloaded) 
+  s_holding_def: 
+  "holding (s::state) thread cs \<equiv> (thread \<in> set (wq s cs) \<and> thread = hd (wq s cs))"
+  s_waiting_def: 
+  "waiting (s::state) thread cs \<equiv> (thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs))"
+  s_depend_def: 
+  "depend (s::state) \<equiv> 
+    {(Th t, Cs c) | t c. waiting (wq s) t c} \<union> {(Cs c, Th t) | c t. holding (wq s) t c}"
+  s_dependents_def: 
+  "dependents (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}"
+
+text {*
+  The following function @{text "readys"} calculates the set of ready threads. A thread is {\em ready} 
+  for running if it is a live thread and it is not waiting for any critical resource.
+  *}
+definition readys :: "state \<Rightarrow> thread set"
+  where "readys s = {thread . thread \<in> threads s \<and> (\<forall> cs. \<not> waiting s thread 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 = {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"
+
+text {* \noindent
+  The following function @{text "holdents s th"} returns the set of resources held by thread 
+  @{text "th"} in state @{text "s"}.
+  *}
+definition holdents :: "state \<Rightarrow> thread \<Rightarrow> cs set"
+  where "holdents s th = {cs . (Cs cs, Th th) \<in> depend s}"
+
+text {* \noindent
+  @{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"} 
+  is expressed as @{text "step s e"}. The predicate @{text "step"} is inductively defined as 
+  follows:
+  *}
+inductive step :: "state \<Rightarrow> event \<Rightarrow> bool"
+  where
+  -- {* 
+  A thread can be created if it is not a live thread:
+  *}
+  thread_create: "\<lbrakk>thread \<notin> threads s\<rbrakk> \<Longrightarrow> step s (Create thread prio)" |
+  -- {*
+  A thread can exit if it no longer hold any resource:
+  *}
+  thread_exit: "\<lbrakk>thread \<in> runing s; holdents s thread = {}\<rbrakk> \<Longrightarrow> step s (Exit thread)" |
+  -- {*
+  \begin{minipage}{0.9\textwidth}
+  A thread can request for an critical resource @{text "cs"}, if it is running and 
+  the request does not form a loop in the current RAG. The latter condition 
+  is set up to avoid deadlock. The condition also reflects our assumption all threads are 
+  carefully programmed so that deadlock can not happen:
+  \end{minipage}
+  *}
+  thread_P: "\<lbrakk>thread \<in> runing s;  (Cs cs, Th thread)  \<notin> (depend s)^+\<rbrakk> \<Longrightarrow> 
+                                                                step s (P thread cs)" |
+  -- {*
+  \begin{minipage}{0.9\textwidth}
+  A thread can release a critical resource @{text "cs"} 
+  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:
+  *}  
+  thread_set: "\<lbrakk>thread \<in> runing s\<rbrakk> \<Longrightarrow> step s (Set thread prio)"
+
+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
+  the predicate @{text "vt"} can be defined as the following:
+  *}
+inductive vt :: "(state \<Rightarrow> event \<Rightarrow> bool) \<Rightarrow> state \<Rightarrow> bool"
+ for cs -- {* @{text "cs"} is an argument representing any step predicate. *}
+  where
+  -- {* Empty list @{text "[]"} is a legal state in any protocol:*}
+  vt_nil[intro]: "vt cs []" |
+  -- {* 
+  \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:
+  \end{minipage}
+  *}
+  vt_cons[intro]: "\<lbrakk>vt cs s; cs s e\<rbrakk> \<Longrightarrow> vt cs (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.
+  *}
+
+text {* \noindent
+  The following two 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"
+
+fun the_th :: "node \<Rightarrow> thread"
+  where "the_th (Th th) = th"
+
+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.
+  *}
+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"}
+  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 
+  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 
+  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"
+(*<*)
+end
+(*>*)
+