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 (trace) 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"}: *}

  \noindent 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: *}

  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"}: *}

text {*

  The function @{text "threads"} is used to calculate the set of live

  threads (@{text "threads s"}) in state @{text "s"}. *}

  "threads (Create th prio#s) = {th} \<union> threads s" | 

  "threads (Exit th # s) = (threads s) - {th}" | 

  "threads (e # s) = threads s" 

  \noindent The function @{text "threads"} is one of the {\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

  function}. *}

  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 (represented by event @{text "Set thread

  priority"}). *}

  "priority th [] = 0" |

  "priority th (Create th' prio # s) = 

     (if th' = th then prio else priority th s)" |

  "priority th (Set th' prio # s) = 

     (if th' = th then prio else priority th s)" |

  "priority th (e # s) = priority th s"

  \noindent 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. *}

  "last_set th [] = 0" |

  "last_set th ((Create th' prio) # s) = 

       (if (th = th') then length s else last_set th s)" |

  "last_set th ((Set th' prio) # s) = 

       (if (th = th') then length s else last_set th s)" |

  "last_set th (_ # s) = last_set th s"

  \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 the {\em time} the priority was set. The intention

  is to discriminate threads with the same priority by giving threads whose

  priority is assigned earlier higher precedences, because such threads are

  assumed more urgent to finish. *}

  where "preced th s \<equiv> Prc (priority th s) (last_set th s)"

definition preceds :: "thread set \<Rightarrow> state \<Rightarrow> precedence set"

  where "preceds ths s \<equiv> {preced th s | th. th \<in> ths}"

  \noindent A number of important notions in PIP are represented as the

  following 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

  resource, which is slightly different from tradition where all threads in

  the waiting queue are considered as waiting for the resource. *}

text {* 

  \begin{minipage}{0.9\textwidth} This meaning of @{text "wq"} is reflected

  in the following definition of @{text "holding wq th cs"}, where @{text

  "holding wq th cs"} means thread @{text "th"} is holding the critical

  resource @{text "cs"}. This decision is based on @{text "wq"}.

  \end{minipage} *}

text {* 

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

  "waiting_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"

text {* 

  Resource Allocation Graphs (RAG for short) are used extensively in our

  formal analysis. The following type @{text "node"} is used to represent

  the two types of nodes in RAGs. *}

datatype node = 

  Th "thread" -- {* Node for a thread. *}

| Cs "cs"     -- {* Node for a critical resource. *}

text {*

  \begin{minipage}{0.9\textwidth} @{text "RAG wq"} generates RAG (a binary

  relations on @{text "node"}) out of waiting queues of the system

  (represented by the @{text "wq"} argument): \end{minipage} *}

  RAG_raw :: "(cs \<Rightarrow> thread list) => (node * node) set"

where

  "RAG_raw wq \<equiv>

      {(Th th, Cs cs) | th cs. waiting_raw wq th cs} \<union> 

      {(Cs cs, Th th) | cs th. holding_raw wq th cs}"

text {*

  \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"}. Here, "RAGing" means waiting

  directly or indirectly on the critical resource. \end{minipage} *}

  dependants_raw :: "(cs \<Rightarrow> thread list) \<Rightarrow> thread \<Rightarrow> thread set"

where

  "dependants_raw wq th \<equiv> {th' . (Th th', Th th) \<in> (RAG_raw wq)^+}"

  precedence, i.e. @{text "preced th s"}. *}

definition 

  cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"

  where 

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

  @{text "th"} can be boosted (increased) by those threads in the @{text

  "dependants wq th"}-set. If one thread gets boosted, we say it inherits

  the priority (or, more precisely, the precedence) of its dependants. This

  is whrere the word "Inheritance" in Priority Inheritance Protocol comes

  from. *}

lemma cpreced_def2:

  "cpreced wq s th \<equiv> Max ({preced th s} \<union> preceds (dependants_raw wq th) s)"

  unfolding cpreced_def image_def preceds_def

  @{text "qs"}) released the resource: *}

  affect the correctness of the PIP protocol. *}

  etc) and a function assigning precedence to threads: *}

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"}. *}

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.

    Setting the initial value of the @{text "schedule_state"} record 

    (see the explanations above).

fun schs :: "state \<Rightarrow> schedule_state"

  where 

  "schs [] = (| wq_fun = all_unlocked,  cprec_fun = initial_cprec |)" 

| "schs (Create th prio # s) = 

apply(rule ext)

apply(simp add: dependants_raw_def RAG_raw_def waiting_raw_def holding_raw_def)

text {* 

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

  *}

text {* 

  \noindent The following @{text "cp"} is a shorthand for @{text

  "cprec_fun"}. *}

text {* 

  \noindent Functions @{text "holding"}, @{text "waiting"}, @{text "RAG"}

  and @{text "dependants"} still have the same meaning, but redefined so

  that they no longer RAG on the fictitious {\em waiting queue function}

  @{text "wq"}, but on system state @{text "s"}. *}

text {* 

  The following four lemmas relate the @{term wq} and non-@{term wq}

  versions of @{term waiting}, @{term holding}, @{term dependants} and

  @{term cp}. *}

lemma waiting_eq: 

  shows "waiting s th cs = waiting_raw (wq s) th cs"

  by (simp add: s_waiting_abv wq_def)

lemma holding_eq: 

  shows "holding s th cs = holding_raw (wq s) th cs"

  by (simp add: s_holding_abv wq_def)

lemma eq_dependants: 

  shows "dependants_raw (wq s) = dependants s"

  by (simp add: s_dependants_abv wq_def)

lemma cp_eq: 

  shows "cp s th = cpreced (wq s) s th"

unfolding cp_def wq_def

apply(induct s rule: schs.induct)

apply(simp add: Let_def cpreced_initial)

apply(simp add: Let_def)

apply(simp add: Let_def)

apply(simp add: Let_def)

apply(subst (2) schs.simps)

apply(simp add: Let_def)

apply(subst (2) schs.simps)

apply(simp add: Let_def)

done

  The following lemma can be proved easily, and the meaning is obvious. *}

  by (auto simp:s_holding_abv wq_def holding_raw_def)

  by (auto simp:s_waiting_abv wq_def waiting_raw_def)

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

    {(Cs cs, Th th) | cs th. holding_raw (wq s) th cs}"

  by (auto simp:s_RAG_abv wq_def RAG_raw_def)

lemma eq_RAG: 

  "RAG_raw (wq s) = RAG s"

  by (unfold RAG_raw_def s_RAG_def, auto)