1 chapter {* Definitions *}

     2 (*<*)

     3 theory PIPDefs

     4 imports Precedence_ord Moment RTree Max

     5 begin

     6 (*>*)

     7 

     8 text {*

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

    10   The model is based on Paulson's inductive protocol verification method, where 

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

    12   event put at the head. 

    13 *}

    14 

    15 text {*

    16   To define events, the identifiers of {\em threads},

    17   {\em priority} and {\em critical resources } (abbreviated as @{text "cs"}) 

    18   need to be represented. All three are represetned using standard 

    19   Isabelle/HOL type @{typ "nat"}:

    20 *}

    21 

    22 type_synonym thread = nat -- {* Type for thread identifiers. *}

    23 type_synonym priority = nat  -- {* Type for priorities. *}

    24 type_synonym cs = nat -- {* Type for critical sections (or critical resources). *}

    25 

    26 text {*

    27   \noindent

    28   The abstraction of Priority Inheritance Protocol (PIP) is set at the system call level.

    29   Every system call is represented as an event. The format of events is defined 

    30   defined as follows:

    31   *}

    32 

    33 datatype event = 

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

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

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

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

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

    39 

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

    41   "actor (Create th pty) = th" |

    42   "actor (Exit th) = th" |

    43   "actor (P th cs) = th" |

    44   "actor (V th cs) = th" |

    45   "actor (Set th pty) = th"

    46 

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

    48   "isCreate (Create th pty) = True" |

    49   "isCreate _ = False"

    50 

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

    52   "isP (P th cs) = True" |

    53   "isP _ = False"

    54 

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

    56   "isV (V th cs) = True" |

    57   "isV _ = False"

    58 

    59 text {* 

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

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

    62   *}

    63 type_synonym state = "event list"

    64 

    65 

    66 text {* 

    67 \noindent

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

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

    70   *}

    71 datatype node = 

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

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

    74 

    75 text {*

    76   \noindent

    77   The following function

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

    79   in state @{text "s"}.

    80   *}

    81 fun threads :: "state \<Rightarrow> thread set"

    82   where 

    83   -- {* At the start of the system, the set of threads is empty: *}

    84   "threads [] = {}" | 

    85   -- {* New thread is added to the @{text "threads"}: *}

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

    87   -- {* Finished thread is removed: *}

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

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

    90   "threads (e#s) = threads s" 

    91 

    92 text {* 

    93   \noindent

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

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

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

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

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

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

   100   The protocol being modelled 

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

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

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

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

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

   106   *}

   107 

   108 text {* \noindent

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

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

   111   The {\em original priority} is the priority 

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

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

   114 *}

   115 

   116 fun priority :: "thread \<Rightarrow> state \<Rightarrow> priority"

   117   where

   118   -- {* @{text "0"} is assigned to threads which have never been created: *}

   119   "priority thread [] = 0" |

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

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

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

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

   124   "priority thread (e#s) = priority thread s"

   125 

   126 text {*

   127   \noindent

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

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

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

   131 *}

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

   133   where

   134   "last_set thread [] = 0" |

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

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

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

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

   139   "last_set thread (_#s) = last_set thread s"

   140 

   141 text {*

   142   \noindent 

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

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

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

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

   147   This explains the following definition:

   148   *}

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

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

   151 

   152 

   153 text {*

   154   \noindent

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

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

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

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

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

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

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

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

   163   *}

   164 

   165 consts 

   166   holding :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool" 

   167   waiting :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"

   168   RAG :: "'b \<Rightarrow> (node \<times> node) set"

   169   dependants :: "'b \<Rightarrow> thread \<Rightarrow> thread set"

   170 

   171 defs (overloaded) 

   172   -- {* 

   173   \begin{minipage}{0.9\textwidth}

   174   This meaning of @{text "wq"} is reflected in the following definition of @{text "holding wq th cs"},

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

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

   177   \end{minipage}

   178   *}

   179 

   180   cs_holding_def: 

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

   182   -- {* 

   183   \begin{minipage}{0.9\textwidth}

   184   In accordance with the definition of @{text "holding wq th cs"}, 

   185   a thread @{text "th"} is considered waiting for @{text "cs"} if 

   186   it is in the {\em waiting queue} of critical resource @{text "cs"}, but not at the head.

   187   This is reflected in the definition of @{text "waiting wq th cs"} as follows:

   188   \end{minipage}

   189   *}

   190   cs_waiting_def: 

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

   192   -- {* 

   193   \begin{minipage}{0.9\textwidth}

   194   @{text "RAG wq"} generates RAG (a binary relations on @{text "node"})

   195   out of waiting queues of the system (represented by the @{text "wq"} argument):

   196   \end{minipage}

   197   *}

   198   cs_RAG_def: 

   199   "RAG (wq::cs \<Rightarrow> thread list) \<equiv>

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

   201   -- {* 

   202   \begin{minipage}{0.9\textwidth}

   203   The following @{text "dependants wq th"} represents the set of threads which are RAGing on

   204   thread @{text "th"} in Resource Allocation Graph @{text "RAG wq"}. 

   205   Here, "RAGing" means waiting directly or indirectly on the critical resource. 

   206   \end{minipage}

   207   *}

   208   cs_dependants_def: 

   209   "dependants (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}"

   210 

   211 

   212 text {* \noindent 

   213   The following

   214   @{text "cpreced s th"} gives the {\em current precedence} of thread @{text "th"} under

   215   state @{text "s"}. The definition of @{text "cpreced"} reflects the basic idea of 

   216   Priority Inheritance that the {\em current precedence} of a thread is the precedence 

   217   inherited from the maximum of all its dependants, i.e. the threads which are waiting 

   218   directly or indirectly waiting for some resources from it. If no such thread exits, 

   219   @{text "th"}'s {\em current precedence} equals its original precedence, i.e. 

   220   @{text "preced th s"}.

   221   *}

   222 

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

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

   225 

   226 text {*

   227   Notice that the current precedence (@{text "cpreced"}) of one thread @{text "th"} can be boosted 

   228   (becoming larger than its own precedence) by those threads in 

   229   the @{text "dependants wq th"}-set. If one thread get boosted, we say 

   230   it inherits the priority (or, more precisely, the precedence) of 

   231   its dependants. This is how the word "Inheritance" in 

   232   Priority Inheritance Protocol comes.

   233 *}

   234 

   235 (*<*)

   236 lemma 

   237   cpreced_def2:

   238   "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants wq th})"

   239   unfolding cpreced_def image_def

   240   apply(rule eq_reflection)

   241   apply(rule_tac f="Max" in arg_cong)

   242   by (auto)

   243 (*>*)

   244 

   245 

   246 text {* \noindent

   247   Assuming @{text "qs"} be the waiting queue of a critical resource, 

   248   the following abbreviation "release qs" is the waiting queue after the thread 

   249   holding the resource (which is thread at the head of @{text "qs"}) released

   250   the resource:

   251 *}

   252 abbreviation

   253   "release qs \<equiv> case qs of

   254              [] => [] 

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

   256 text {* \noindent

   257   It can be seen from the definition that the thread at the head of @{text "qs"} is removed

   258   from the return value, and the value @{term "q"} is an reordering of @{text "qs'"}, the 

   259   tail of @{text "qs"}. Through this reordering, one of the waiting threads (those in @{text "qs'"} }

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

   261   Therefore, this thread is the one who takes over the resource. This is a little better different 

   262   from common sense that the thread who comes the earliest should take over.  

   263   The intention of this definition is to show that the choice of which thread to take over the 

   264   release resource does not affect the correctness of the PIP protocol. 

   265 *}

   266 

   267 text {*

   268   The data structure used by the operating system for scheduling is referred to as 

   269   {\em schedule state}. It is represented as a record consisting of 

   270   a function assigning waiting queue to resources 

   271   (to be used as the @{text "wq"} argument in @{text "holding"}, @{text "waiting"} 

   272   and  @{text "RAG"}, etc) and a function assigning precedence to threads:

   273   *}

   274 

   275 record schedule_state = 

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

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

   278 

   279 text {* \noindent

   280   The following two abbreviations (@{text "all_unlocked"} and @{text "initial_cprec"}) 

   281   are used to set the initial values of the @{text "wq_fun"} @{text "cprec_fun"} fields 

   282   respectively of the @{text "schedule_state"} record by the following function @{text "sch"},

   283   which is used to calculate the system's {\em schedule state}.

   284 

   285   Since there is no thread at the very beginning to make request, all critical resources 

   286   are free (or unlocked). This status is represented by the abbreviation

   287   @{text "all_unlocked"}. 

   288   *}

   289 abbreviation

   290   "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)"

   291 

   292 

   293 text {* \noindent

   294   The initial current precedence for a thread can be anything, because there is no thread then. 

   295   We simply assume every thread has precedence @{text "Prc 0 0"}.

   296   *}

   297 

   298 abbreviation 

   299   "initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0"

   300 

   301 

   302 text {* \noindent

   303   The following function @{text "schs"} is used to calculate the system's schedule state @{text "schs s"}

   304   out of the current system state @{text "s"}. It is the central function to model Priority Inheritance:

   305   *}

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

   307   where 

   308   -- {*

   309   \begin{minipage}{0.9\textwidth}

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

   311   \end{minipage}

   312   *}

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

   314 

   315   -- {*

   316   \begin{minipage}{0.9\textwidth}

   317   \begin{enumerate}

   318   \item @{text "ps"} is the schedule state of last moment.

   319   \item @{text "pwq"} is the waiting queue function of last moment.

   320   \item @{text "pcp"} is the precedence function of last moment (NOT USED). 

   321   \item @{text "nwq"} is the new waiting queue function. It is calculated using a @{text "case"} statement:

   322   \begin{enumerate}

   323       \item If the happening event is @{text "P thread cs"}, @{text "thread"} is added to 

   324             the end of @{text "cs"}'s waiting queue.

   325       \item If the happening event is @{text "V thread cs"} and @{text "s"} is a legal state,

   326             @{text "th'"} must equal to @{text "thread"}, 

   327             because @{text "thread"} is the one currently holding @{text "cs"}. 

   328             The case @{text "[] \<Longrightarrow> []"} may never be executed in a legal state.

   329             the @{text "(SOME q. distinct q \<and> set q = set qs)"} is used to choose arbitrarily one 

   330             thread in waiting to take over the released resource @{text "cs"}. In our representation,

   331             this amounts to rearrange elements in waiting queue, so that one of them is put at the head.

   332       \item For other happening event, the schedule state just does not change.

   333   \end{enumerate}

   334   \item @{text "ncp"} is new precedence function, it is calculated from the newly updated waiting queue 

   335         function. The RAGency of precedence function on waiting queue function is the reason to 

   336         put them in the same record so that they can evolve together.

   337   \end{enumerate}

   338   

   339 

   340   The calculation of @{text "cprec_fun"} depends on the value of @{text "wq_fun"}. 

   341   Therefore, in the following cases, @{text "wq_fun"} is always calculated first, in 

   342   the name of @{text "wq"} (if  @{text "wq_fun"} is not changed

   343   by the happening event) or @{text "new_wq"} (if the value of @{text "wq_fun"} is changed).

   344   \end{minipage}

   345      *}

   346    "schs (Create th prio # s) = 

   347        (let wq = wq_fun (schs s) in

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

   349 |  "schs (Exit th # s) = 

   350        (let wq = wq_fun (schs s) in

   351           (|wq_fun = wq, cprec_fun = cpreced wq (Exit th # s)|))"

   352 |  "schs (Set th prio # s) = 

   353        (let wq = wq_fun (schs s) in

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

   355    -- {*

   356    \begin{minipage}{0.9\textwidth}

   357       Different from the forth coming cases, the @{text "wq_fun"} field of the schedule state 

   358       is changed. So, the new value is calculated first, in the name of @{text "new_wq"}.

   359    \end{minipage}   

   360    *}

   361 |  "schs (P th cs # s) = 

   362        (let wq = wq_fun (schs s) in

   363         let new_wq = wq(cs := (wq cs @ [th])) in

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

   365 |  "schs (V th cs # s) = 

   366        (let wq = wq_fun (schs s) in

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

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

   369 

   370 lemma cpreced_initial: 

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

   372 apply(simp add: cpreced_def)

   373 apply(simp add: cs_dependants_def cs_RAG_def cs_waiting_def cs_holding_def)

   374 apply(simp add: preced_def)

   375 done

   376 

   377 lemma sch_old_def:

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

   379                   let pwq = wq_fun ps in 

   380                   let nwq = case e of

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

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

   383                                                       [] \<Rightarrow> [] | 

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

   385                                             in pwq(cs:=nq)                 |

   386                               _ \<Rightarrow> pwq

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

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

   389                  )"

   390 apply(cases e)

   391 apply(simp_all)

   392 done

   393 

   394 

   395 text {* 

   396   \noindent

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

   398   *}

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

   400   where "wq s = wq_fun (schs s)"

   401 

   402 text {* \noindent 

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

   404   *}

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

   406   where "cp s \<equiv> cprec_fun (schs s)"

   407 

   408 text {* \noindent

   409   Functions @{text "holding"}, @{text "waiting"}, @{text "RAG"} and 

   410   @{text "dependants"} still have the 

   411   same meaning, but redefined so that they no longer RAG on the 

   412   fictitious {\em waiting queue function}

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

   414   *}

   415 defs (overloaded) 

   416   s_holding_abv: 

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

   418   s_waiting_abv: 

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

   420   s_RAG_abv: 

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

   422   s_dependants_abv: 

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

   424 

   425 

   426 text {* 

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

   428   *}

   429 lemma

   430   s_holding_def: 

   431   "holding (s::state) th cs \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th = hd (wq_fun (schs s) cs))"

   432   by (auto simp:s_holding_abv wq_def cs_holding_def)

   433 

   434 lemma s_waiting_def: 

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

   436   by (auto simp:s_waiting_abv wq_def cs_waiting_def)

   437 

   438 lemma s_RAG_def: 

   439   "RAG (s::state) =

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

   441   by (auto simp:s_RAG_abv wq_def cs_RAG_def)

   442 

   443 lemma

   444   s_dependants_def: 

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

   446   by (auto simp:s_dependants_abv wq_def cs_dependants_def)

   447 

   448 text {*

   449   The following function @{text "readys"} calculates the set of ready threads. A thread is {\em ready} 

   450   for running if it is a live thread and it is not waiting for any critical resource.

   451   *}

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

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

   454 

   455 text {* \noindent

   456   The following function @{text "runing"} calculates the set of running thread, which is the ready 

   457   thread with the highest precedence.  

   458   *}

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

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

   461 

   462 text {* \noindent

   463   Notice that the definition of @{text "running"} reflects the preemptive scheduling strategy,  

   464   because, if the @{text "running"}-thread (the one in @{text "runing"} set) 

   465   lowered its precedence by resetting its own priority to a lower

   466   one, it will lose its status of being the max in @{text "ready"}-set and be superseded.

   467 *}

   468 

   469 text {* \noindent

   470   The following function @{text "holdents s th"} returns the set of resources held by thread 

   471   @{text "th"} in state @{text "s"}.

   472   *}

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

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

   475 

   476 lemma holdents_test: 

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

   478 unfolding holdents_def

   479 unfolding s_RAG_def

   480 unfolding s_holding_abv

   481 unfolding wq_def

   482 by (simp)

   483 

   484 text {* \noindent

   485   Observation @{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in

   486   state @{text "s"}:

   487   *}

   488 definition cntCS :: "state \<Rightarrow> thread \<Rightarrow> nat"

   489   where "cntCS s th = card (holdents s th)"

   490 

   491 text {* \noindent

   492   According to the convention of Paulson's inductive method,

   493   the decision made by a protocol that event @{text "e"} is eligible to happen next under state @{text "s"} 

   494   is expressed as @{text "step s e"}. The predicate @{text "step"} is inductively defined as 

   495   follows (notice how the decision is based on the {\em observation function}s 

   496   defined above, and also notice how a complicated protocol is modeled by a few simple 

   497   observations, and how such a kind of simplicity gives rise to improved trust on

   498   faithfulness):

   499   *}

   500 inductive step :: "state \<Rightarrow> event \<Rightarrow> bool"

   501   where

   502   -- {* 

   503   A thread can be created if it is not a live thread:

   504   *}

   505   thread_create: "\<lbrakk>thread \<notin> threads s\<rbrakk> \<Longrightarrow> step s (Create thread prio)" |

   506   -- {*

   507   A thread can exit if it no longer hold any resource:

   508   *}

   509   thread_exit: "\<lbrakk>thread \<in> runing s; holdents s thread = {}\<rbrakk> \<Longrightarrow> step s (Exit thread)" |

   510   -- {*

   511   \begin{minipage}{0.9\textwidth}

   512   A thread can request for an critical resource @{text "cs"}, if it is running and 

   513   the request does not form a loop in the current RAG. The latter condition 

   514   is set up to avoid deadlock. The condition also reflects our assumption all threads are 

   515   carefully programmed so that deadlock can not happen:

   516   \end{minipage}

   517   *}

   518   thread_P: "\<lbrakk>thread \<in> runing s;  (Cs cs, Th thread)  \<notin> (RAG s)^+\<rbrakk> \<Longrightarrow> 

   519                                                                 step s (P thread cs)" |

   520   -- {*

   521   \begin{minipage}{0.9\textwidth}

   522   A thread can release a critical resource @{text "cs"} 

   523   if it is running and holding that resource:

   524   \end{minipage}

   525   *}

   526   thread_V: "\<lbrakk>thread \<in> runing s;  holding s thread cs\<rbrakk> \<Longrightarrow> step s (V thread cs)" |

   527   -- {*

   528   \begin{minipage}{0.9\textwidth}

   529   A thread can adjust its own priority as long as it is current running. 

   530   With the resetting of one thread's priority, its precedence may change. 

   531   If this change lowered the precedence, according to the definition of @{text "running"}

   532   function, 

   533   \end{minipage}

   534   *}  

   535   thread_set: "\<lbrakk>thread \<in> runing s\<rbrakk> \<Longrightarrow> step s (Set thread prio)"

   536 

   537 text {*

   538   In Paulson's inductive method, every protocol is defined by such a @{text "step"}

   539   predicate. For instance, the predicate @{text "step"} given above 

   540   defines the PIP protocol. So, it can also be called "PIP".

   541 *}

   542 

   543 abbreviation

   544   "PIP \<equiv> step"

   545 

   546 

   547 text {* \noindent

   548   For any protocol defined by a @{text "step"} predicate, 

   549   the fact that @{text "s"} is a legal state in 

   550   the protocol is expressed as: @{text "vt step s"}, where

   551   the predicate @{text "vt"} can be defined as the following:

   552   *}

   553 inductive vt :: "state \<Rightarrow> bool"

   554   where

   555   -- {* Empty list @{text "[]"} is a legal state in any protocol:*}

   556   vt_nil[intro]: "vt []" |

   557   -- {* 

   558   \begin{minipage}{0.9\textwidth}

   559   If @{text "s"} a legal state of the protocol defined by predicate @{text "step"}, 

   560   and event @{text "e"} is allowed to happen under state @{text "s"} by the protocol 

   561   predicate @{text "step"}, then @{text "e#s"} is a new legal state rendered by the 

   562   happening of @{text "e"}:

   563   \end{minipage}

   564   *}

   565   vt_cons[intro]: "\<lbrakk>vt s; step s e\<rbrakk> \<Longrightarrow> vt (e#s)"

   566 

   567 text {*  \noindent

   568   It is easy to see that the definition of @{text "vt"} is generic. It can be applied to 

   569   any specific protocol specified by a @{text "step"}-predicate to get the set of

   570   legal states of that particular protocol.

   571   *}

   572 

   573 text {* 

   574   The following are two very basic properties of @{text "vt"}.

   575 *}

   576 

   577 lemma step_back_vt: "vt (e#s) \<Longrightarrow> vt s"

   578   by(ind_cases "vt (e#s)", simp)

   579 

   580 lemma step_back_step: "vt (e#s) \<Longrightarrow> step s e"

   581   by(ind_cases "vt (e#s)", simp)

   582 

   583 text {* \noindent

   584   The following two auxiliary functions @{text "the_cs"} and @{text "the_th"} are used to extract

   585   critical resource and thread respectively out of RAG nodes.

   586   *}

   587 fun the_cs :: "node \<Rightarrow> cs"

   588   where "the_cs (Cs cs) = cs"

   589 

   590 fun the_th :: "node \<Rightarrow> thread"

   591   where "the_th (Th th) = th"

   592 

   593 text {* \noindent

   594   The following predicate @{text "next_th"} describe the next thread to 

   595   take over when a critical resource is released. In @{text "next_th s th cs t"}, 

   596   @{text "th"} is the thread to release, @{text "t"} is the one to take over.

   597   Notice how this definition is backed up by the @{text "release"} function and its use 

   598   in the @{text "V"}-branch of @{text "schs"} function. This @{text "next_th"} function

   599   is not needed for the execution of PIP. It is introduced as an auxiliary function 

   600   to state lemmas. The correctness of this definition will be confirmed by 

   601   lemmas @{text "step_v_hold_inv"}, @{text " step_v_wait_inv"}, 

   602   @{text "step_v_get_hold"} and @{text "step_v_not_wait"}.

   603   *}

   604 definition next_th:: "state \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> thread \<Rightarrow> bool"

   605   where "next_th s th cs t = (\<exists> rest. wq s cs = th#rest \<and> rest \<noteq> [] \<and> 

   606                                      t = hd (SOME q. distinct q \<and> set q = set rest))"

   607 

   608 text {* \noindent

   609   The aux function @{text "count Q l"} is used to count the occurrence of situation @{text "Q"}

   610   in list @{text "l"}:

   611   *}

   612 definition count :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat"

   613   where "count Q l = length (filter Q l)"

   614 

   615 text {* \noindent

   616   The following observation @{text "cntP s"} returns the number of operation @{text "P"} happened 

   617   before reaching state @{text "s"}.

   618   *}

   619 definition cntP :: "state \<Rightarrow> thread \<Rightarrow> nat"

   620   where "cntP s th = count (\<lambda> e. \<exists> cs. e = P th cs) s"

   621 

   622 text {* \noindent

   623   The following observation @{text "cntV s"} returns the number of operation @{text "V"} happened 

   624   before reaching state @{text "s"}.

   625   *}

   626 definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat"

   627   where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s"

   628 

   629 text {* @{text "the_preced"} is also the same as @{text "preced"}, the only

   630        difference is the order of arguemts. *}

   631 definition "the_preced s th = preced th s"

   632 

   633 text {* @{term "the_thread"} extracts thread out of RAG node. *}

   634 fun the_thread :: "node \<Rightarrow> thread" where

   635    "the_thread (Th th) = th"

   636 

   637 text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *}

   638 definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}"

   639 

   640 text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *}

   641 definition "hRAG (s::state) =  {(Cs cs, Th th) | th cs. holding s th cs}"

   642 

   643 text {* 

   644   The following @{text "tRAG"} is the thread-graph derived from @{term "RAG"}.

   645   It characterizes the dependency between threads when calculating current

   646   precedences. It is defined as the composition of the above two sub-graphs, 

   647   names @{term "wRAG"} and @{term "hRAG"}.

   648  *}

   649 definition "tRAG s = wRAG s O hRAG s"

   650 

   651 text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *}

   652 lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)"

   653   by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv 

   654              s_holding_abv cs_RAG_def, auto)

   655 

   656 definition "cp_gen s x =

   657                   Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"

   658 

   659 (*<*)

   660 

   661 end

   662 (*>*)

   663