(*<*)

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 \<equiv> 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 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 "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 = 

    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 

  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 :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"

  where "cpreced wq s = (\<lambda> th. Max ((\<lambda> th. preced th s) ` ({th} \<union> dependents wq th)))"

(*<*)

lemma 

  cpreced_def2:

  "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependents 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"

abbreviation

  "release qs \<equiv> case qs of

             [] => [] 

          |  (_#qs) => (SOME q. distinct q \<and> set q = set qs)"

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 [] = (| wq_fun = \<lambda> cs. [],  cprec_fun = (\<lambda>_. Prc 0 0) |)" |

  -- {*

  \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 (NOT USED). 

  \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 (Create th prio # s) = 

       (let wq = wq_fun (schs s) in

          (|wq_fun = wq, cprec_fun = cpreced wq (Create th prio # s)|))"

|  "schs (Exit th # 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)|))"

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

       (let wq = wq_fun (schs s) in

        let new_wq = wq(cs := release (wq cs)) in

          (|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))"

lemma cpreced_initial: 

  "cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"

apply(simp add: cpreced_def)

apply(simp add: cs_dependents_def cs_depend_def cs_waiting_def cs_holding_def)

apply(simp add: preced_def)

done

lemma sch_old_def:

  "schs (e#s) = (let ps = schs s in 

                  let pwq = wq_fun ps in 

                  let nwq = case e of

                             P th cs \<Rightarrow>  pwq(cs:=(pwq cs @ [th])) |

                             V th cs \<Rightarrow> let nq = case (pwq cs) of

                                                      [] \<Rightarrow> [] | 

                                                      (_#qs) \<Rightarrow> (SOME q. distinct q \<and> set q = set qs)

                                            in pwq(cs:=nq)                 |

                              _ \<Rightarrow> pwq

                  in let ncp = cpreced nwq (e#s) in 

                     \<lparr>wq_fun = nwq, cprec_fun = ncp\<rparr>

                 )"

apply(cases e)

apply(simp_all)

done

text {* 

  \noindent

  The following @{text "wq"} is a shorthand for @{text "wq_fun"}. 

  *}

definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list" 

  where "wq s = wq_fun (schs s)"

text {* \noindent 

  The following @{text "cp"} is a shorthand for @{text "cprec_fun"}. 

  *}

definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"

  where "cp s \<equiv> cprec_fun (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_abv: 

  "holding (s::state) \<equiv> holding (wq_fun (schs s))"

  s_waiting_abv: 

  "waiting (s::state) \<equiv> waiting (wq_fun (schs s))"

  s_depend_abv: 

  "depend (s::state) \<equiv> depend (wq_fun (schs s))"

  s_dependents_abv: 

  "dependents (s::state) \<equiv> dependents (wq_fun (schs s))"

text {* 

  The following lemma can be proved easily:

  *}

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)

lemma s_waiting_def: 

  "waiting (s::state) th cs \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th \<noteq> hd (wq_fun (schs s) cs))"

  by (auto simp:s_waiting_abv wq_def cs_waiting_def)

lemma s_depend_def: 

  "depend (s::state) =

    {(Th th, Cs cs) | th cs. waiting (wq s) th cs} \<union> {(Cs cs, Th th) | cs th. holding (wq s) th cs}"

  by (auto simp:s_depend_abv wq_def cs_depend_def)

lemma

  s_dependents_def: 

  "dependents (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}"

  by (auto simp:s_dependents_abv wq_def cs_dependents_def)

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

  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 \<equiv> {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> 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

  in state @{text "s"}, then @{text "e#s"} is a legal state as well:

  \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.

  *}

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

(*>*)