10   In this section, the formal model of  Priority Inheritance Protocol (PIP) is presented. 

    10   In this section, the formal model of Priority Inheritance Protocol (PIP) is presented. 

    12   the state of the system is modelled as a list of events happened so far with the latest 

    12   the state of the system is modelled as a list of events (trace) happened so far with the 

    13   event put at the head. 

    13   latest event put at the head. 

    35   Create thread priority | -- {* Thread @{text "thread"} is created with priority @{text "priority"}. *}

    35   Create thread priority   -- {* Thread @{text "thread"} is created with priority @{text "priority"}. *}

    36   Exit thread | -- {* Thread @{text "thread"} finishing its execution. *}

    36 | Exit thread              -- {* Thread @{text "thread"} finishing its execution. *}

    37   P thread cs | -- {* Thread @{text "thread"} requesting critical resource @{text "cs"}. *}

    37 | P thread cs              -- {* Thread @{text "thread"} requesting critical resource @{text "cs"}. *}

    38   V thread cs | -- {* Thread @{text "thread"}  releasing critical resource @{text "cs"}. *}

    38 | V thread cs              -- {* Thread @{text "thread"} releasing critical resource @{text "cs"}. *}

    39   Set thread priority -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *}

    39 | Set thread priority      -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *}

    63   As mentioned earlier, in Paulson's inductive method, the states of system are represented as lists of events,

    64   As mentioned earlier, in Paulson's inductive method, the states of system are represented as lists 

    64   which is defined by the following type @{text "state"}:

    65   of events, which is defined by the following type @{text "state"}: *}

    65   *}

    66 

    70 \noindent

    71   Resource Allocation Graphs (RAG for short) are used extensively in our formal analysis. 

    71   Resource Allocation Graph (RAG for short) is used extensively in our formal analysis. 

    72   The following type @{text "node"} is used to represent the two types of nodes in RAGs. *}

    72   The following type @{text "node"} is used to represent nodes in RAG.

    73   *}

    75    Th "thread" | -- {* Node for thread. *}

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

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

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

    77 

    76 

    78 text {*

    77 text {*

    79   \noindent

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

    80   The following function

    79   in state @{text "s"}. *}

    81   @{text "threads"} is used to calculate the set of live threads (@{text "threads s"})

    80 

    82   in state @{text "s"}.

    83   *}

    96   \noindent

    93 

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

    94   \noindent The function @{text "threads"} defined above is one of the

    98   the so called {\em observation function}s which forms 

    95   so called {\em observation function}s which forms the very basis of

    99   the very basis of Paulson's inductive protocol verification method.

    96   Paulson's inductive protocol verification method.  Each observation

   100   Each observation function {\em observes} one particular aspect (or attribute)

    97   function {\em observes} one particular aspect (or attribute) of the

   101   of the system. For example, the attribute observed by  @{text "threads s"}

    98   system. For example, the attribute observed by @{text "threads s"}

   102   is the set of threads living in state @{text "s"}. 

    99   is the set of threads living in state @{text "s"}.  The protocol

   103   The protocol being modelled 

   100   being modelled The decision made the protocol being modelled is

   104   The decision made the protocol being modelled is based on the {\em observation}s

   101   based on the {\em observation}s returned by {\em observation

   105   returned by {\em observation function}s. Since {\observation function}s forms 

   102   function}s. Since {\observation function}s forms the very basis on

   106   the very basis on which Paulson's inductive method is based, there will be 

   103   which Paulson's inductive method is based, there will be a lot of

   107   a lot of such observation functions introduced in the following. In fact, any function 

   104   such observation functions introduced in the following. In fact, any

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

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

   109   *}

   106   function}.  *}

   110 

   107 

   111 text {* \noindent

   108 text {* 

   112   Observation @{text "priority th s"} is

   109 

   113   the {\em original priority} of thread @{text "th"} in state @{text "s"}. 

   110   \noindent Observation @{text "priority th s"} is the {\em original

   114   The {\em original priority} is the priority 

   111   priority} of thread @{text "th"} in state @{text "s"}.  The {\em

   115   assigned to a thread when it is created or when it is reset by system call 

   112   original priority} is the priority assigned to a thread when it is

   116   (represented by event @{text "Set thread priority"}).

   113   created or when it is reset by system call (represented by event

   117 *}

   114   @{text "Set thread priority"}).  *}

   130   \noindent

   127 

   131   Observation @{text "last_set th s"} is the last time when the priority of thread @{text "th"} is set, 

   128   \noindent Observation @{text "last_set th s"} is the last time when

   132   observed from state @{text "s"}.

   129   the priority of thread @{text "th"} is set, observed from state

   133   The time in the system is measured by the number of events happened so far since the very beginning.

   130   @{text "s"}.  The time in the system is measured by the number of

   134 *}

   131   events happened so far since the very beginning.  *}

   132 

   145   \noindent 

   143 

   146   The {\em precedence} is a notion derived from {\em priority}, where the {\em precedence} of 

   144   \noindent The {\em precedence} is a notion derived from {\em

   147   a thread is the combination of its {\em original priority} and {\em time} the priority is set. 

   145   priority}, where the {\em precedence} of a thread is the combination

   148   The intention is to discriminate threads with the same priority by giving threads whose priority

   146   of its {\em original priority} and {\em time} the priority is set.

   149   is assigned earlier higher precedences, becasue such threads are more urgent to finish. 

   147   The intention is to discriminate threads with the same priority by

   150   This explains the following definition:

   148   giving threads whose priority is assigned earlier higher

   151   *}

   149   precedences, becasue such threads are more urgent to finish.  This

   150   explains the following definition: *}

   151 

   157   \noindent

   157 

   158   A number of important notions in PIP are represented as the following functions, 

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

   159   defined in terms of the waiting queues of the system, where the waiting queues 

   159   the following functions, defined in terms of the waiting queues of

   160   , as a whole, is represented by the @{text "wq"} argument of every notion function.

   160   the system, where the waiting queues , as a whole, is represented by

   161   The @{text "wq"} argument is itself a functions which maps every critical resource 

   161   the @{text "wq"} argument of every notion function.  The @{text

   162   @{text "cs"} to the list of threads which are holding or waiting for it. 

   162   "wq"} argument is itself a functions which maps every critical

   163   The thread at the head of this list is designated as the thread which is current 

   163   resource @{text "cs"} to the list of threads which are holding or

   164   holding the resrouce, which is slightly different from tradition where

   164   waiting for it.  The thread at the head of this list is designated

   165   all threads in the waiting queue are considered as waiting for the resource.

   165   as the thread which is current holding the resrouce, which is

   166   *}

   166   slightly different from tradition where all threads in the waiting

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

   176 definition 

   177 -- {* 

   177   -- {*