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

    10 

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

    11   In this section, the formal model of Priority Inheritance Protocol (PIP)

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

    12   is presented. The model is based on Paulson's inductive protocol

    13   latest event put at the head. 

    13   verification method, where the state of the system is modelled as a list

    14 *}

    14   of events (trace) happened so far with the latest event put at the head.

    15 

    15   *}

    16 text {*

    16 

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

    17 text {*

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

    18 

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

    19   To define events, the identifiers of {\em threads}, {\em priority} and

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

    20   {\em critical resources } (abbreviated as @{text "cs"}) need to be

    21 *}

    21   represented. All three are represetned using standard Isabelle/HOL type

    22   @{typ "nat"}: *}

    28   \noindent

    29 

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

    30   \noindent The abstraction of Priority Inheritance Protocol (PIP) is set at

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

    31   the system call level. Every system call is represented as an event. The

    31   defined as follows:

    32   format of events is defined defined as follows: *}

    32   *}

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

    64   

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

    65   As mentioned earlier, in Paulson's inductive method, the states of system

    66   are represented as lists of events, which is defined by the following type

    67   @{text "state"}: *}

    70 text {* 

    72 text {*

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

    73 

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

    74   The function @{text "threads"} is used to calculate the set of live

    73 datatype node = 

    75   threads (@{text "threads s"}) in state @{text "s"}. *}

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

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

    76 

    77 text {*

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

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

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

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

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

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

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

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

    91 

    87 

    92 text {* 

    88 text {* 

    93 

    89 

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

    90   \noindent The function @{text "threads"} is one of the {\em observation

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

    91   function}s which forms the very basis of Paulson's inductive protocol

    96   Paulson's inductive protocol verification method.  Each observation

    92   verification method. Each observation function {\em observes} one

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

    93   particular aspect (or attribute) of the system. For example, the attribute

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

    94   observed by @{text "threads s"} is the set of threads living in state

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

    95   @{text "s"}. The protocol being modelled The decision made the protocol

   100   being modelled The decision made the protocol being modelled is

    96   being modelled is based on the {\em observation}s returned by {\em

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

    97   observation function}s. Since {\observation function}s forms the very

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

    98   basis on which Paulson's inductive method is based, there will be a lot of

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

   106   function}.  *}

   101   function}. *}

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

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

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

   107   priority} is the priority assigned to a thread when it is created or when

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

   108   it is reset by system call (represented by event @{text "Set thread

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

   109   priority"}). *}

   119   "priority thread [] = 0" |

   114   "priority th [] = 0" |

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

   115   "priority th (Create th' prio # s) = 

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

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

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

   117   "priority th (Set th' prio # s) = 

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

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

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

   119   "priority th (e # s) = priority th s"

   125 

   120 

   126 text {*

   121 text {*

   127 

   122 

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

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

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

   124   priority of thread @{text "th"} is set, observed from state @{text "s"}.

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

   125   The time in the system is measured by the number of events happened so far

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

   126   since the very beginning. *}

   135   "last_set thread [] = 0" |

   130   "last_set th [] = 0" |

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

   131   "last_set th ((Create th' prio) # s) = 

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

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

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

   133   "last_set th ((Set th' prio) # s) = 

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

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

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

   135   "last_set th (_ # s) = last_set th s"

   141 

   136 

   142 text {*

   137 text {*

   143 

   138 

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

   139   \noindent The {\em precedence} is a notion derived from {\em priority},

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

   140   where the {\em precedence} of a thread is the combination of its {\em

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

   141   original priority} and the {\em time} the priority was set. The intention

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

   142   is to discriminate threads with the same priority by giving threads whose

   148   giving threads whose priority is assigned earlier higher

   143   priority is assigned earlier higher precedences, because such threads are

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

   144   assumed more urgent to finish. *}

   150   explains the following definition: *}

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

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

   154 

   148 

   155 

   149 definition preceds :: "thread set \<Rightarrow> state \<Rightarrow> precedence set"

   156 text {*

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

   157 

   151 

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

   152 text {*

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

   153 

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

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

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

   155   following functions, defined in terms of the waiting queues of the system,

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

   156   where the waiting queues, as a whole, is represented by the @{text "wq"}

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

   157   argument of every notion function. The @{text "wq"} argument is itself a

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

   158   functions which maps every critical resource @{text "cs"} to the list of

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

   159   threads which are holding or waiting for it. The thread at the head of

   166   slightly different from tradition where all threads in the waiting

   160   this list is designated as the thread which is current holding the

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

   161   resource, which is slightly different from tradition where all threads in

   168 

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

   169 (*

   163 

   170 consts 

   164 text {* 

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

   165 

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

   166   \begin{minipage}{0.9\textwidth} This meaning of @{text "wq"} is reflected

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

   167   in the following definition of @{text "holding wq th cs"}, where @{text

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

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

   175 *)

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

   176 

   170   \end{minipage} *}

   177 -- {* 

   178   \begin{minipage}{0.9\textwidth}

   179   This meaning of @{text "wq"} is reflected in the following definition of

   180   @{text "holding wq th cs"}, where @{text "holding wq th cs"} means thread

   181   @{text "th"} is holding the critical resource @{text "cs"}. This decision

   182   is based on @{text "wq"}.

   183   \end{minipage}

   184   *}

   206   -- {* 

   204   RAG_raw :: "(cs \<Rightarrow> thread list) => (node * node) set"

   207   \begin{minipage}{0.9\textwidth}

   205 where

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

   206   "RAG_raw wq \<equiv>

   209   of waiting queues of the system (represented by the @{text "wq"}

   207       {(Th th, Cs cs) | th cs. waiting_raw wq th cs} \<union> 

   210   argument): \end{minipage}

   208       {(Cs cs, Th th) | cs th. holding_raw wq th cs}"

   211   *}

   209 

   212 

   210 text {*

   213   cs_RAG_raw: 

   211  

   214   "RAG_raw (wq::cs \<Rightarrow> thread list) \<equiv>

   212   \begin{minipage}{0.9\textwidth} The following @{text "dependants wq th"}

   215       {(Th th, Cs cs) | th cs. waiting_raw wq th cs} \<union> {(Cs cs, Th th) | cs th. holding_raw wq th cs}"

   213   represents the set of threads which are RAGing on thread @{text "th"} in

   214   Resource Allocation Graph @{text "RAG wq"}. Here, "RAGing" means waiting

   215   directly or indirectly on the critical resource. \end{minipage} *}

   218   -- {* 

   218   dependants_raw :: "(cs \<Rightarrow> thread list) \<Rightarrow> thread \<Rightarrow> thread set"

   219   \begin{minipage}{0.9\textwidth}

   219 where

   220   The following @{text "dependants wq th"} represents the set of threads

   220   "dependants_raw wq th \<equiv> {th' . (Th th', Th th) \<in> (RAG_raw wq)^+}"

   221   which are RAGing on thread @{text "th"} in Resource Allocation Graph

   221 

   222   @{text "RAG wq"}. Here, "RAGing" means waiting directly or indirectly on

   222 text {* 

   223   the critical resource. 

   223 

   224   \end{minipage}

   225   *}

   226 

   227   cs_dependants_def: 

   228   "dependants_raw (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (RAG_raw wq)^+}"

   229 

   230 text {* 

   238   precedence, i.e. @{text "preced th s"}. 

   231   precedence, i.e. @{text "preced th s"}. *}

   239 *}

   232 

   240 

   233 definition 

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

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

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

   235   where 

   243 

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

   244 text {*

   237 

   238 text {*

   239 

   246   @{text "th"} can be boosted (becoming larger than its own precedence) by

   241   @{text "th"} can be boosted (increased) by those threads in the @{text

   247   those threads in the @{text "dependants wq th"}-set. If one thread get

   242   "dependants wq th"}-set. If one thread gets boosted, we say it inherits

   248   boosted, we say it inherits the priority (or, more precisely, the

   243   the priority (or, more precisely, the precedence) of its dependants. This

   249   precedence) of its dependants. This is how the word "Inheritance" in

   244   is whrere the word "Inheritance" in Priority Inheritance Protocol comes

   250   Priority Inheritance Protocol comes.

   245   from. *}

   251 *}

   246 

   252 

   247 lemma cpreced_def2:

   253 (*<*)

   248   "cpreced wq s th \<equiv> Max ({preced th s} \<union> preceds (dependants_raw wq th) s)"

   254 lemma 

   249   unfolding cpreced_def image_def preceds_def

   255   cpreced_def2:

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

   257   unfolding cpreced_def image_def

   269   @{text "qs"}) released the resource: 

   259   @{text "qs"}) released the resource: *}

   270 *}

   287   affect the correctness of the PIP protocol. 

   277   affect the correctness of the PIP protocol. *}

   288 *}

   278 

   289 

   279 text {*

   290 text {*

   280   

   295   etc) and a function assigning precedence to threads:

   285   etc) and a function assigning precedence to threads: *}

   296   *}

   318 text {* \noindent

   308 text {* 

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

   309 

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

   310   \noindent The initial current precedence for a thread can be anything,

   321   *}

   311   because there is no thread then. We simply assume every thread has

   312   precedence @{text "Prc 0 0"}. *}

   327 text {* \noindent

   318 text {* 

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

   319 

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

   320   \noindent The following function @{text "schs"} is used to calculate the

   330   *}

   321   system's schedule state @{text "schs s"} out of the current system state

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

   322   @{text "s"}. It is the central function to model Priority Inheritance.

   332   where 

   323 

   333   -- {*

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

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

   326     (see the explanations above).

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

   329 

   371    "schs (Create th prio # s) = 

   362 

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

   364   where 

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

   366 | "schs (Create th prio # s) = 

   398 apply(simp add: cs_dependants_def cs_RAG_raw cs_waiting_raw cs_holding_raw)

   394 apply(simp add: dependants_raw_def RAG_raw_def waiting_raw_def holding_raw_def)

   402 lemma sch_old_def:

   398 text {* 

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

   399 

   404                   let pwq = wq_fun ps in 

   400   \noindent The following @{text "wq"} is a shorthand for @{text "wq_fun"}.

   405                   let nwq = case e of

   401   *}

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

   402 

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

   408                                                       [] \<Rightarrow> [] | 

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

   410                                             in pwq(cs:=nq)                 |

   411                               _ \<Rightarrow> pwq

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

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

   414                  )"

   415 apply(cases e)

   416 apply(simp_all)

   417 done

   418 

   419 

   420 text {* 

   421   \noindent

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

   423   *}

   427 text {* \noindent 

   406 text {* 

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

   407 

   429   *}

   408   \noindent The following @{text "cp"} is a shorthand for @{text

   409   "cprec_fun"}. *}

   410 

   433 text {* \noindent

   414 text {* 

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

   415 

   435   @{text "dependants"} still have the 

   416   \noindent Functions @{text "holding"}, @{text "waiting"}, @{text "RAG"}

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

   417   and @{text "dependants"} still have the same meaning, but redefined so

   437   fictitious {\em waiting queue function}

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

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

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

   439   *}

   440 

   458 

   437 text {* 

   459 text {* 

   438 

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

   439   The following four lemmas relate the @{term wq} and non-@{term wq}

   461   *}

   440   versions of @{term waiting}, @{term holding}, @{term dependants} and

   441   @{term cp}. *}

   442 

   443 lemma waiting_eq: 

   444   shows "waiting s th cs = waiting_raw (wq s) th cs"

   445   by (simp add: s_waiting_abv wq_def)

   446 

   447 lemma holding_eq: 

   448   shows "holding s th cs = holding_raw (wq s) th cs"

   449   by (simp add: s_holding_abv wq_def)

   450 

   451 lemma eq_dependants: 

   452   shows "dependants_raw (wq s) = dependants s"

   453   by (simp add: s_dependants_abv wq_def)

   454 

   455 lemma cp_eq: 

   456   shows "cp s th = cpreced (wq s) s th"

   457 unfolding cp_def wq_def

   458 apply(induct s rule: schs.induct)

   459 apply(simp add: Let_def cpreced_initial)

   460 apply(simp add: Let_def)

   461 apply(simp add: Let_def)

   462 apply(simp add: Let_def)

   463 apply(subst (2) schs.simps)

   464 apply(simp add: Let_def)

   465 apply(subst (2) schs.simps)

   466 apply(simp add: Let_def)

   467 done

   468 

   469 text {* 

   470 

   471   The following lemma can be proved easily, and the meaning is obvious. *}

   466   by (auto simp:s_holding_abv wq_def cs_holding_raw)

   476   by (auto simp:s_holding_abv wq_def holding_raw_def)

   470   by (auto simp:s_waiting_abv wq_def cs_waiting_raw)

   480   by (auto simp:s_waiting_abv wq_def waiting_raw_def)

   474     {(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}"

   484     {(Th th, Cs cs) | th cs. waiting_raw (wq s) th cs} \<union> 

   475   by (auto simp:s_RAG_abv wq_def cs_RAG_raw)

   485     {(Cs cs, Th th) | cs th. holding_raw (wq s) th cs}"

   476 

   486   by (auto simp:s_RAG_abv wq_def RAG_raw_def)

   477 lemma

   487 

   478   s_dependants_def: 

   488 lemma eq_RAG: 

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

   489   "RAG_raw (wq s) = RAG s"

   480   by (auto simp:s_dependants_abv wq_def cs_dependants_def)

   490   by (unfold RAG_raw_def s_RAG_def, auto)

   481 

   491 

   482 text {*

   492 

   493 lemma s_dependants_def: 

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

   495 using dependants_raw_def eq_RAG s_dependants_abv wq_def by auto

   496 

   497 text {*

   498   

   485   is not waiting for any critical resource.

   501   is not waiting for any critical resource. *}

   486   *}

   492   \noindent The following function @{text "runing"} calculates the set of

   507   

   493   running thread, which is the ready thread with the highest precedence.

   508   \noindent The following function @{text "running"} calculates the set of

   494   *}

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

   495 

   510 

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

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

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

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

   498 

   513 

   499 text {* 

   514 text {* 

   515   

   502   (the one in @{text "runing"} set) lowered its precedence by resetting its

   518   (the one in @{text "running"} set) lowered its precedence by resetting its

   504   @{text "ready"}-set and be superseded. 

   520   @{text "ready"}-set and be superseded. *}

   505 *}

   521 

   506 

   522 text {* 

   507 text {* 

   523   

   523 text {* \noindent

   539 text {* 

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

   540 

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

   541   \noindent According to the convention of Paulson's inductive method, the

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

   542   decision made by a protocol that event @{text "e"} is eligible to happen

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

   543   next under state @{text "s"} is expressed as @{text "step s e"}. The

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

   544   predicate @{text "step"} is inductively defined as follows (notice how the

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

   545   decision is based on the {\em observation function}s defined above, and

   530   faithfulness):

   546   also notice how a complicated protocol is modeled by a few simple

   531   *}

   547   observations, and how such a kind of simplicity gives rise to improved

   548   trust on faithfulness): *}

   549 

   550 

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

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

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

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

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

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

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

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

   568 

   587 

   569 text {*

   588 text {*

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

   589 

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

   590   In Paulson's inductive method, every protocol is defined by such a @{text

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

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

   573 *}

   592   defines the PIP protocol. So, it can also be called "PIP". *}

   579 text {* \noindent

   598 text {* 

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

   599 

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

   600   \noindent For any protocol defined by a @{text "step"} predicate, the fact

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

   601   that @{text "s"} is a legal state in the protocol is expressed as: @{text

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

   602   "vt step s"}, where the predicate @{text "vt"} can be defined as the

   584   *}

   603   following: *}

   604 

   605 

   599 text {*  \noindent

   620 text {*  

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

   621 

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

   622   \noindent It is easy to see that the definition of @{text "vt"} is

   602   legal states of that particular protocol.

   623   generic. It can be applied to any specific protocol specified by a @{text

   603   *}

   624   "step"}-predicate to get the set of legal states of that particular

   604 

   625   protocol. *}

   605 text {* 

   626 

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

   627 text {* 

   607 *}

   628   

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

   703              s_holding_abv cs_RAG_raw, auto)

   725              s_holding_abv RAG_raw_def, auto)