1 chapter {* Definitions *}

     2 (*<*)

     3 theory PrioGDef

     4 imports Precedence_ord Moment

     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 

    41 text {* 

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

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

    44   *}

    45 type_synonym state = "event list"

    46 

    47 

    48 text {* 

    49 \noindent

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

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

    52   *}

    53 datatype node = 

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

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

    56 

    57 text {*

    58   \noindent

    59   The following function

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

    61   in state @{text "s"}.

    62   *}

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

    64   where 

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

    66   "threads [] = {}" | 

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

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

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

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

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

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

    73 

    74 text {* 

    75   \noindent

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

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

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

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

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

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

    82   The protocol being modelled 

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

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

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

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

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

    88   *}

    89 

    90 text {* \noindent

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

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

    93   The {\em original priority} is the priority 

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

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

    96 *}

    97 

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

    99   where

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

   101   "priority thread [] = 0" |

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

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

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

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

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

   107 

   108 text {*

   109   \noindent

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

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

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

   113 *}

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

   115   where

   116   "last_set thread [] = 0" |

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

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

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

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

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

   122 

   123 text {*

   124   \noindent 

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

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

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

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

   129   This explains the following definition:

   130   *}

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

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

   133 

   134 

   135 text {*

   136   \noindent

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

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

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

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

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

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

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

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

   145   *}

   146 

   147 consts 

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

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

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

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

   152 

   153 defs (overloaded) 

   154   -- {* 

   155   \begin{minipage}{0.9\textwidth}

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

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

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

   159   \end{minipage}

   160   *}

   161 

   162   cs_holding_def: 

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

   164   -- {* 

   165   \begin{minipage}{0.9\textwidth}

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

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

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

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

   170   \end{minipage}

   171   *}

   172   cs_waiting_def: 

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

   174   -- {* 

   175   \begin{minipage}{0.9\textwidth}

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

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

   178   \end{minipage}

   179   *}

   180   cs_RAG_def: 

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

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

   183   -- {* 

   184   \begin{minipage}{0.9\textwidth}

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

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

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

   188   \end{minipage}

   189   *}

   190   cs_dependants_def: 

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

   192 

   193 

   194 text {* \noindent 

   195   The following

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

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

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

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

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

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

   202   @{text "preced th s"}.

   203   *}

   204 

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

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

   207 

   208 text {*

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

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

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

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

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

   214   Priority Inheritance Protocol comes.

   215 *}

   216 

   217 (*<*)

   218 lemma 

   219   cpreced_def2:

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

   221   unfolding cpreced_def image_def

   222   apply(rule eq_reflection)

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

   224   by (auto)

   225 (*>*)

   226 

   227 

   228 text {* \noindent

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

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

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

   232   the resource:

   233 *}

   234 abbreviation

   235   "release qs \<equiv> case qs of

   236              [] => [] 

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

   238 text {* \noindent

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

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

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

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

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

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

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

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

   247 *}

   248 

   249 text {*

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

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

   252   a function assigning waiting queue to resources 

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

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

   255   *}

   256 

   257 record schedule_state = 

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

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

   260 

   261 text {* \noindent

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

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

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

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

   266 

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

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

   269   @{text "all_unlocked"}. 

   270   *}

   271 abbreviation

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

   273 

   274 

   275 text {* \noindent

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

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

   278   *}

   279 

   280 abbreviation 

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

   282 

   283 

   284 text {* \noindent

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

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

   287   *}

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

   289   where 

   290   -- {*

   291   \begin{minipage}{0.9\textwidth}

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

   293   \end{minipage}

   294   *}

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

   296 

   297   -- {*

   298   \begin{minipage}{0.9\textwidth}

   299   \begin{enumerate}

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

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

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

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

   304   \begin{enumerate}

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

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

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

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

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

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

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

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

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

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

   315   \end{enumerate}

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

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

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

   319   \end{enumerate}

   320   

   321 

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

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

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

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

   326   \end{minipage}

   327      *}

   328    "schs (Create th prio # s) = 

   329        (let wq = wq_fun (schs s) in

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

   331 |  "schs (Exit th # s) = 

   332        (let wq = wq_fun (schs s) in

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

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

   335        (let wq = wq_fun (schs s) in

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

   337    -- {*

   338    \begin{minipage}{0.9\textwidth}

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

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

   341    \end{minipage}   

   342    *}

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

   344        (let wq = wq_fun (schs s) in

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

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

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

   348        (let wq = wq_fun (schs s) in

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

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

   351 

   352 lemma cpreced_initial: 

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

   354 apply(simp add: cpreced_def)

   355 apply(simp add: cs_dependants_def cs_RAG_def cs_waiting_def cs_holding_def)

   356 apply(simp add: preced_def)

   357 done

   358 

   359 lemma sch_old_def:

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

   361                   let pwq = wq_fun ps in 

   362                   let nwq = case e of

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

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

   365                                                       [] \<Rightarrow> [] | 

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

   367                                             in pwq(cs:=nq)                 |

   368                               _ \<Rightarrow> pwq

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

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

   371                  )"

   372 apply(cases e)

   373 apply(simp_all)

   374 done

   375 

   376 

   377 text {* 

   378   \noindent

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

   380   *}

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

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

   383 

   384 text {* \noindent 

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

   386   *}

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

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

   389 

   390 definition "cp_gen s x = Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"

   391 

   392 text {* \noindent

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

   394   @{text "dependants"} still have the 

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

   396   fictitious {\em waiting queue function}

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

   398   *}

   399 defs (overloaded) 

   400   s_holding_abv: 

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

   402   s_waiting_abv: 

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

   404   s_RAG_abv: 

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

   406   s_dependants_abv: 

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

   408 

   409 

   410 text {* 

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

   412   *}

   413 lemma

   414   s_holding_def: 

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

   416   by (auto simp:s_holding_abv wq_def cs_holding_def)

   417 

   418 lemma s_waiting_def: 

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

   420   by (auto simp:s_waiting_abv wq_def cs_waiting_def)

   421 

   422 lemma s_RAG_def: 

   423   "RAG (s::state) =

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

   425   by (auto simp:s_RAG_abv wq_def cs_RAG_def)

   426 

   427 lemma

   428   s_dependants_def: 

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

   430   by (auto simp:s_dependants_abv wq_def cs_dependants_def)

   431 

   432 text {*

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

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

   435   *}

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

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

   438 

   439 text {* \noindent

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

   441   thread with the highest precedence.  

   442   *}

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

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

   445 

   446 text {* \noindent

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

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

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

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

   451 *}

   452 

   453 text {* \noindent

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

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

   456   *}

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

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

   459 

   460 lemma holdents_test: 

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

   462 unfolding holdents_def

   463 unfolding s_RAG_def

   464 unfolding s_holding_abv

   465 unfolding wq_def

   466 by (simp)

   467 

   468 text {* \noindent

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

   470   state @{text "s"}:

   471   *}

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

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

   474 

   475 text {* \noindent

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

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

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

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

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

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

   482   faithfulness):

   483   *}

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

   485   where

   486   -- {* 

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

   488   *}

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

   490   -- {*

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

   492   *}

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

   494   -- {*

   495   \begin{minipage}{0.9\textwidth}

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

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

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

   499   carefully programmed so that deadlock can not happen:

   500   \end{minipage}

   501   *}

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

   503                                                                 step s (P thread cs)" |

   504   -- {*

   505   \begin{minipage}{0.9\textwidth}

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

   507   if it is running and holding that resource:

   508   \end{minipage}

   509   *}

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

   511   -- {*

   512   \begin{minipage}{0.9\textwidth}

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

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

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

   516   function, 

   517   \end{minipage}

   518   *}  

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

   520 

   521 text {*

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

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

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

   525 *}

   526 

   527 abbreviation

   528   "PIP \<equiv> step"

   529 

   530 

   531 text {* \noindent

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

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

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

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

   536   *}

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

   538   where

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

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

   541   -- {* 

   542   \begin{minipage}{0.9\textwidth}

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

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

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

   546   happening of @{text "e"}:

   547   \end{minipage}

   548   *}

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

   550 

   551 text {*  \noindent

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

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

   554   legal states of that particular protocol.

   555   *}

   556 

   557 text {* 

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

   559 *}

   560 

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

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

   563 

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

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

   566 

   567 text {* \noindent

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

   569   critical resource and thread respectively out of RAG nodes.

   570   *}

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

   572   where "the_cs (Cs cs) = cs"

   573 

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

   575   where "the_th (Th th) = th"

   576 

   577 text {* \noindent

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

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

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

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

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

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

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

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

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

   587   *}

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

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

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

   591 

   592 text {* \noindent

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

   594   in list @{text "l"}:

   595   *}

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

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

   598 

   599 text {* \noindent

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

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

   602   *}

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

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

   605 

   606 text {* \noindent

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

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

   609   *}

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

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

   612 (*<*)

   613 

   614 end

   615 (*>*)

   616