(*<*)

theory PIPDefs

begin

(*>*)

chapter {* Definitions *}

text {*

  In this chapter, the formal model of the 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.

  *}

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 represented 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 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 the

  system are represented as lists of events, which is defined by the

  following type @{text "state"}: *}

type_synonym state = "event list"

text {*

  The 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 th prio#s) = {th} \<union> threads s" | 

  -- {* Finished thread is removed: *}

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

  -- {* Other kind of events does not affect the value of @{text "threads"}: *}

  "threads (e # s) = threads s" 

text {* 

  \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 being live 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 {* 

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

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

text {*

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

fun last_set :: "thread \<Rightarrow> state \<Rightarrow> nat"

  where

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

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

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

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

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

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

text {*

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

definition

  "holding_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread = hd (wq cs))"

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

definition

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

definition

  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 {*

definition

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

definition 

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

  where 

definition 

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

  where 

  "cpreceds wq s ths \<equiv> {cpreced wq s th | th. th \<in> ths}"

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 the resource: *}

abbreviation

  "release qs \<equiv> case qs of

             [] => [] 

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

text {* 

  \noindent It can be seen from the definition that the thread at the head

  of @{text "qs"} is removed from the return value, and the value @{term

  "q"} is an reordering of @{text "qs'"}, the tail of @{text "qs"}. Through

  this reordering, one of the waiting threads (those in @{text "qs'"} } is

  chosen nondeterministically to be the head of the new queue @{text "q"}.

  Therefore, this thread is the one who takes over the resource. This is a

  little better different 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. *}

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

  \begin{minipage}{0.9\textwidth}

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

    (see the explanations above).

  \end{minipage}

  *}

  -- {*

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

     *}

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

  where 

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

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

   -- {*

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

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

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 "RAG"}

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

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

definition 

  s_holding_abv: 

  "holding (s::state) \<equiv> holding_raw (wq s)"

definition

  s_waiting_abv: 

  "waiting (s::state) \<equiv> waiting_raw (wq s)"

definition

  s_RAG_abv: 

  "RAG (s::state) \<equiv> RAG_raw (wq s)"

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

text {* 

  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 s cs) \<and> th = hd (wq s cs))"

  by(simp add: s_holding_abv holding_raw_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 waiting_raw_def)

lemma s_RAG_def: 

  "RAG (s::state) =

    {(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)

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 "running"} calculates the set of

  running thread, which is the ready thread with the highest precedence. *}

definition running :: "state \<Rightarrow> thread set"

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

definition holdents :: "state \<Rightarrow> thread \<Rightarrow> cs set" 

  where "holdents s th \<equiv> {cs . holding s th cs}"

lemma holdents_test: 

  "holdents s th = {cs . (Cs cs, Th th) \<in> RAG s}"

unfolding holdents_def

unfolding s_RAG_def

unfolding s_holding_abv

unfolding wq_def

by (simp)

text {* 

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