1 (*<*)

     2 theory PrioGDef

     3 imports Precedence_ord Moment

     4 begin

     5 (*>*)

     6 

     7 text {*

     8   In this section, the formal model of Priority Inheritance is presented. 

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

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

    11   event put at the head. 

    12 

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

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

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

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

    17 *}

    18 

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

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

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

    22 

    23 text {*

    24   \noindent

    25   Every event in the system corresponds to a system call, the formats of which are

    26   defined as follows:

    27   *}

    28 

    29 datatype event = 

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

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

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

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

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

    35 

    36 text {* 

    37 \noindent

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

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

    40   *}

    41 datatype node = 

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

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

    44 

    45 text {* 

    46   In Paulson's inductive method, the states of system are represented as lists of events,

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

    48   *}

    49 type_synonym state = "event list"

    50 

    51 text {*

    52   \noindent

    53   The following function

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

    55   in state @{text "s"}.

    56   *}

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

    58   where 

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

    60   "threads [] = {}" | 

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

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

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

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

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

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

    67 text {* \noindent

    68   Functions such as @{text "threads"}, which extract information out of system states, are called

    69   {\em observing functions}. A series of observing functions will be defined in the sequel in order to 

    70   model the protocol. 

    71   Observing function @{text "original_priority"} calculates 

    72   the {\em original priority} of thread @{text "th"} in state @{text "s"}, expressed as

    73   : @{text "original_priority th s" }. The {\em original priority} is the priority 

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

    75   @{text "Set thread priority"}.

    76 *}

    77 

    78 fun original_priority :: "thread \<Rightarrow> state \<Rightarrow> priority"

    79   where

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

    81   "original_priority thread [] = 0" |

    82   "original_priority thread (Create thread' prio#s) = 

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

    84   "original_priority thread (Set thread' prio#s) = 

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

    86   "original_priority thread (e#s) = original_priority thread s"

    87 

    88 text {*

    89   \noindent

    90   In the following,

    91   @{text "birthtime th s"} is the time when thread @{text "th"} is created, 

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

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

    94 *}

    95 fun birthtime :: "thread \<Rightarrow> state \<Rightarrow> nat"

    96   where

    97   "birthtime thread [] = 0" |

    98   "birthtime thread ((Create thread' prio)#s) = 

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

   100   "birthtime thread ((Set thread' prio)#s) = 

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

   102   "birthtime thread (e#s) = birthtime thread s"

   103 

   104 text {*

   105   \noindent 

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

   107   a thread is the combination of its {\em original priority} and {\em birth time}. The intention is

   108   to discriminate threads with the same priority by giving threads whose priority

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

   110   This explains the following definition:

   111   *}

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

   113   where "preced thread s \<equiv> Prc (original_priority thread s) (birthtime thread s)"

   114 

   115 

   116 text {*

   117   \noindent

   118   A number of important notions are defined here:

   119   *}

   120 

   121 consts 

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

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

   124   depend :: "'b \<Rightarrow> (node \<times> node) set"

   125   dependents :: "'b \<Rightarrow> thread \<Rightarrow> thread set"

   126 

   127 text {*

   128   \noindent

   129   In the definition of the following several functions, it is supposed that

   130   the waiting queue of every critical resource is given by a waiting queue 

   131   function @{text "wq"}, which servers as arguments of these functions.

   132   *}

   133 defs (overloaded) 

   134   -- {* 

   135   \begin{minipage}{0.9\textwidth}

   136   We define that the thread which is at the head of waiting queue of resource @{text "cs"}

   137   is holding the resource. This definition is slightly different from tradition where

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

   139   This notion is reflected in the definition of @{text "holding wq th cs"} as follows:

   140   \end{minipage}

   141   *}

   142   cs_holding_def: 

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

   144   -- {* 

   145   \begin{minipage}{0.9\textwidth}

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

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

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

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

   150   \end{minipage}

   151   *}

   152   cs_waiting_def: 

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

   154   -- {* 

   155   \begin{minipage}{0.9\textwidth}

   156   @{text "depend wq"} represents the Resource Allocation Graph of the system under the waiting 

   157   queue function @{text "wq"}.

   158   \end{minipage}

   159   *}

   160   cs_depend_def: 

   161   "depend (wq::cs \<Rightarrow> thread list) \<equiv>

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

   163   -- {* 

   164   \begin{minipage}{0.9\textwidth}

   165   The following @{text "dependents wq th"} represents the set of threads which are depending on

   166   thread @{text "th"} in Resource Allocation Graph @{text "depend wq"}:

   167   \end{minipage}

   168   *}

   169   cs_dependents_def: 

   170   "dependents (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (depend wq)^+}"

   171 

   172 text {*

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

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

   175   a function assigning waiting queue to resources and a function assigning precedence to 

   176   threads:

   177   *}

   178 record schedule_state = 

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

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

   181 

   182 text {* \noindent 

   183   The following

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

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

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

   187   inherited from the maximum of all its dependents, i.e. the threads which are waiting 

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

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

   190   @{text "preced th s"}.

   191   *}

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

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

   194 

   195 (*<*)

   196 lemma 

   197   cpreced_def2:

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

   199   unfolding cpreced_def image_def

   200   apply(rule eq_reflection)

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

   202   by (auto)

   203 (*>*)

   204 

   205 abbreviation

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

   207 

   208 abbreviation 

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

   210  

   211 abbreviation

   212   "release qs \<equiv> case qs of

   213              [] => [] 

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

   215 

   216 text {* \noindent

   217   The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}.

   218   It is the key function to model Priority Inheritance:

   219   *}

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

   221   where 

   222   "schs [] = (| wq_fun = \<lambda> cs. [],  cprec_fun = (\<lambda>_. Prc 0 0) |)" |

   223 

   224   -- {*

   225   \begin{minipage}{0.9\textwidth}

   226   \begin{enumerate}

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

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

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

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

   231   \begin{enumerate}

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

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

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

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

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

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

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

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

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

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

   242   \end{enumerate}

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

   244         function. The dependency of precedence function on waiting queue function is the reason to 

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

   246   \end{enumerate}

   247   \end{minipage}

   248      *}

   249    "schs (Create th prio # s) = 

   250        (let wq = wq_fun (schs s) in

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

   252 |  "schs (Exit th # s) = 

   253        (let wq = wq_fun (schs s) in

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

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

   256        (let wq = wq_fun (schs s) in

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

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

   259        (let wq = wq_fun (schs s) in

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

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

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

   263        (let wq = wq_fun (schs s) in

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

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

   266 

   267 lemma cpreced_initial: 

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

   269 apply(simp add: cpreced_def)

   270 apply(simp add: cs_dependents_def cs_depend_def cs_waiting_def cs_holding_def)

   271 apply(simp add: preced_def)

   272 done

   273 

   274 lemma sch_old_def:

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

   276                   let pwq = wq_fun ps in 

   277                   let nwq = case e of

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

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

   280                                                       [] \<Rightarrow> [] | 

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

   282                                             in pwq(cs:=nq)                 |

   283                               _ \<Rightarrow> pwq

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

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

   286                  )"

   287 apply(cases e)

   288 apply(simp_all)

   289 done

   290 

   291 

   292 text {* 

   293   \noindent

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

   295   *}

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

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

   298 

   299 text {* \noindent 

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

   301   *}

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

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

   304 

   305 text {* \noindent

   306   Functions @{text "holding"}, @{text "waiting"}, @{text "depend"} and 

   307   @{text "dependents"} still have the 

   308   same meaning, but redefined so that they no longer depend on the 

   309   fictitious {\em waiting queue function}

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

   311   *}

   312 defs (overloaded) 

   313   s_holding_abv: 

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

   315   s_waiting_abv: 

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

   317   s_depend_abv: 

   318   "depend (s::state) \<equiv> depend (wq_fun (schs s))"

   319   s_dependents_abv: 

   320   "dependents (s::state) \<equiv> dependents (wq_fun (schs s))"

   321 

   322 

   323 text {* 

   324   The following lemma can be proved easily:

   325   *}

   326 lemma

   327   s_holding_def: 

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

   329   by (auto simp:s_holding_abv wq_def cs_holding_def)

   330 

   331 lemma s_waiting_def: 

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

   333   by (auto simp:s_waiting_abv wq_def cs_waiting_def)

   334 

   335 lemma s_depend_def: 

   336   "depend (s::state) =

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

   338   by (auto simp:s_depend_abv wq_def cs_depend_def)

   339 

   340 lemma

   341   s_dependents_def: 

   342   "dependents (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}"

   343   by (auto simp:s_dependents_abv wq_def cs_dependents_def)

   344 

   345 text {*

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

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

   348   *}

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

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

   351 

   352 text {* \noindent

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

   354   thread with the highest precedence. 

   355   *}

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

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

   358 

   359 text {* \noindent

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

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

   362   *}

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

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

   365 

   366 lemma holdents_test: 

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

   368 unfolding holdents_def

   369 unfolding s_depend_def

   370 unfolding s_holding_abv

   371 unfolding wq_def

   372 by (simp)

   373 

   374 text {* \noindent

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

   376   state @{text "s"}:

   377   *}

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

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

   380 

   381 text {* \noindent

   382   The fact that event @{text "e"} is eligible to happen next in state @{text "s"} 

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

   384   follows:

   385   *}

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

   387   where

   388   -- {* 

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

   390   *}

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

   392   -- {*

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

   394   *}

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

   396   -- {*

   397   \begin{minipage}{0.9\textwidth}

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

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

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

   401   carefully programmed so that deadlock can not happen:

   402   \end{minipage}

   403   *}

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

   405                                                                 step s (P thread cs)" |

   406   -- {*

   407   \begin{minipage}{0.9\textwidth}

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

   409   if it is running and holding that resource:

   410   \end{minipage}

   411   *}

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

   413   -- {*

   414   A thread can adjust its own priority as long as it is current running:

   415   *}  

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

   417 

   418 text {* \noindent

   419   With predicate @{text "step"}, the fact that @{text "s"} is a legal state in 

   420   Priority Inheritance protocol can be expressed as: @{text "vt step s"}, where

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

   422   *}

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

   424   where

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

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

   427   -- {* 

   428   \begin{minipage}{0.9\textwidth}

   429   If @{text "s"} a legal state, and event @{text "e"} is eligible to happen

   430   in state @{text "s"}, then @{text "e#s"} is a legal state as well:

   431   \end{minipage}

   432   *}

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

   434 

   435 text {*  \noindent

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

   437   any step predicate to get the set of legal states.

   438   *}

   439 

   440 text {* \noindent

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

   442   critical resource and thread respectively out of RAG nodes.

   443   *}

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

   445   where "the_cs (Cs cs) = cs"

   446 

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

   448   where "the_th (Th th) = th"

   449 

   450 text {* \noindent

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

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

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

   454   *}

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

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

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

   458 

   459 text {* \noindent

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

   461   in list @{text "l"}:

   462   *}

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

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

   465 

   466 text {* \noindent

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

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

   469   *}

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

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

   472 

   473 text {* \noindent

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

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

   476   *}

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

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

   479 (*<*)

   480 

   481 end

   482 (*>*)

   483