(*<*)

theory PIPDefs

imports Precedence_ord Moment RTree Max

begin

(*>*)

chapter {* Definitions *}

text {*

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

fun actor :: "event \<Rightarrow> thread" where

  "actor (Create th pty) = th" |

  "actor (Exit th) = th" |

  "actor (P th cs) = th" |

  "actor (V th cs) = th" |

  "actor (Set th pty) = th"

fun isCreate :: "event \<Rightarrow> bool" where

  "isCreate (Create th pty) = True" |

  "isCreate _ = False"

fun isP :: "event \<Rightarrow> bool" where

  "isP (P th cs) = True" |

  "isP _ = False"

fun isV :: "event \<Rightarrow> bool" where

  "isV (V th cs) = True" |

  "isV _ = False"

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

  \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

  The function @{text "threads"} defined above is one of 

  the so called {\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 such observation functions introduced in the following. In fact, any function 

  which takes event list as argument is a {\em observation function}.

  *}

text {* \noindent

  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 thread [] = 0" |

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

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

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

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

  "priority thread (e#s) = priority thread 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 thread [] = 0" |

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

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

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

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

  "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 time} the priority is set. 

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

  -- {* 

  \begin{minipage}{0.9\textwidth}

  \end{minipage}

  *}

  -- {* 

  \begin{minipage}{0.9\textwidth}

  *}

  -- {* 

  \begin{minipage}{0.9\textwidth}

  \end{minipage}

  *}

  cs_dependants_def: 

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

text {*

  Priority Inheritance Protocol comes.

*}

(*<*)

lemma 

  cpreced_def2:

  unfolding cpreced_def image_def

  apply(rule eq_reflection)

  apply(rule_tac f="Max" in arg_cong)

  by (auto)

(*>*)

*}

abbreviation

  "release qs \<equiv> case qs of

             [] => [] 

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

*}

text {*

  *}

record schedule_state = 

    wq_fun :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *}

    cprec_fun :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *}

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:

  *}

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

  where 

  -- {*

  \begin{minipage}{0.9\textwidth}

    Setting the initial value of the @{text "schedule_state"} record (see the explanations above).

  \end{minipage}

  *}

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

  -- {*

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

     *}

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

apply(simp add: cpreced_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 "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"}.

  *}

  s_holding_abv: 

  s_waiting_abv: 

  s_RAG_abv: 

  s_dependants_abv: 

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

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

lemma s_RAG_def: 

  "RAG (s::state) =

lemma

  s_dependants_def: 

  by (auto simp:s_dependants_abv wq_def cs_dependants_def)

text {*

  *}

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

  where "readys s \<equiv> {th . th \<in> threads s \<and> (\<forall> cs. \<not> waiting s th cs)}"

  *}

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

  where "runing s \<equiv> {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"