171 

   172 *)

   172 defs (overloaded) 

   173 

   174 definition 

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

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

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

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

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

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

   178   \end{minipage}

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

   179   *}

   181   \end{minipage}

   180 

   182   *}

   181   cs_holding_def: 

   183 

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

   184   cs_holding_raw:   

   185   "holding_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread = hd (wq cs))"

   186 

   187 

   188 definition

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

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

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

   192   @{text "th"} is considered waiting for @{text "cs"} if it is in the {\em

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

   193   waiting queue} of critical resource @{text "cs"}, but not at the head.

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

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

   189   \end{minipage}

   195   follows:

   190   *}

   196   \end{minipage}

   191   cs_waiting_def: 

   197   *}

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

   198 

   199   cs_waiting_raw: 

   200   "waiting_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"

   201 

   202 definition

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

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

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

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

   197   \end{minipage}

   207   argument): \end{minipage}

   198   *}

   208   *}

   199   cs_RAG_def: 

   209 

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

   210   cs_RAG_raw: 

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

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

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

   213 

   214 definition

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

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

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

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

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

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

   207   \end{minipage}

   220   the critical resource. 

   208   *}

   221   \end{minipage}

   222   *}

   223 

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

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

   211 

   226 

   212 

   227 text {* 

   213 text {* \noindent 

   228   \noindent The following @{text "cpreced s th"} gives the {\em current

   214   The following

   229   precedence} of thread @{text "th"} under state @{text "s"}. The definition

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

   230   of @{text "cpreced"} reflects the basic idea of Priority Inheritance that

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

   231   the {\em current precedence} of a thread is the precedence inherited from

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

   232   the maximum of all its dependants, i.e. the threads which are waiting

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

   233   directly or indirectly waiting for some resources from it. If no such

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

   234   thread exits, @{text "th"}'s {\em current precedence} equals its original

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

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

   221   @{text "preced th s"}.

   236 *}

   222   *}

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

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

   226 

   240 

   227 text {*

   241 text {*

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

   242   Notice that the current precedence (@{text "cpreced"}) of one thread

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

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

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

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

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

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

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

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

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

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

   247 text {* \noindent

   261 text {* 

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

   262 

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

   263   \noindent Assuming @{text "qs"} be the waiting queue of a critical

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

   264   resource, the following abbreviation "release qs" is the waiting queue

   251   the resource:

   265   after the thread holding the resource (which is thread at the head of

   252 *}

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

   267 *}

   268 

   257 text {* \noindent

   273 

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

   274 text {* 

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

   275   \noindent It can be seen from the definition that the thread at the head

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

   276   of @{text "qs"} is removed from the return value, and the value @{term

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

   277   "q"} is an reordering of @{text "qs'"}, the tail of @{text "qs"}. Through

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

   278   this reordering, one of the waiting threads (those in @{text "qs'"} } is

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

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

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

   280   Therefore, this thread is the one who takes over the resource. This is a

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

   281   little better different from common sense that the thread who comes the

   266 *}

   282   earliest should take over. The intention of this definition is to show

   267 

   283   that the choice of which thread to take over the release resource does not

   268 text {*

   284   affect the correctness of the PIP protocol. 

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

   285 *}

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

   286 

   271   a function assigning waiting queue to resources 

   287 text {*

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

   288   The data structure used by the operating system for scheduling is referred

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

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

   290   function assigning waiting queue to resources (to be used as the @{text

   291   "wq"} argument in @{text "holding"}, @{text "waiting"} and @{text "RAG"},

   292   etc) and a function assigning precedence to threads:

   280 text {* \noindent

   299 text {* 

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

   300   \noindent The following two abbreviations (@{text "all_unlocked"} and

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

   301   @{text "initial_cprec"}) are used to set the initial values of the @{text

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

   302   "wq_fun"} @{text "cprec_fun"} fields respectively of the @{text

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

   303   "schedule_state"} record by the following function @{text "sch"}, which is

   285 

   304   used to calculate the system's {\em schedule state}.

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

   305 

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

   306   Since there is no thread at the very beginning to make request, all

   288   @{text "all_unlocked"}. 

   307   critical resources are free (or unlocked). This status is represented by

   289   *}

   308   the abbreviation @{text "all_unlocked"}.

   309 *}

   310 

   374 apply(simp add: cs_dependants_def cs_RAG_def cs_waiting_def cs_holding_def)

   395 apply(simp add: cs_dependants_def cs_RAG_raw cs_waiting_raw cs_holding_raw)

   416 defs (overloaded) 

   437 

   438 

   439 definition 

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

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

   442 

   443 definition

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

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

   446 

   447 definition

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

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

   450   

   451 definition

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

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

   433   by (auto simp:s_holding_abv wq_def cs_holding_def)

   463   by (auto simp:s_holding_abv wq_def cs_holding_raw)

   437   by (auto simp:s_waiting_abv wq_def cs_waiting_def)

   467   by (auto simp:s_waiting_abv wq_def cs_waiting_raw)

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

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

   442   by (auto simp:s_RAG_abv wq_def cs_RAG_def)

   472   by (auto simp:s_RAG_abv wq_def cs_RAG_raw)

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

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

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

   480   The following function @{text "readys"} calculates the set of ready

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

   481   threads. A thread is {\em ready} for running if it is a live thread and it

   452   *}

   482   is not waiting for any critical resource.

   483   *}

   484 

   456 text {* \noindent

   488 text {* 

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

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

   458   thread with the highest precedence.  

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

   459   *}

   491   *}

   492 

   463 text {* \noindent

   496 text {* 

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

   497   \noindent Notice that the definition of @{text "running"} reflects the

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

   498   preemptive scheduling strategy, because, if the @{text "running"}-thread

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

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

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

   500   own priority to a lower one, it will lose its status of being the max in

   468 *}

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

   469 

   502 *}

   470 text {* \noindent

   503 

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

   504 text {* 

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

   505   \noindent The following function @{text "holdents s th"} returns the set

   473   *}

   506   of resources held by thread @{text "th"} in state @{text "s"}. *}

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

   507 

   508 

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

   664              s_holding_abv cs_RAG_def, auto)

   700              s_holding_abv cs_RAG_raw, auto)