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

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

   167   \end{minipage}

   167   \end{minipage}

   168   *}

   168   *}

   169   cs_dependents_def: 

   169   cs_dependents_def: 

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

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

   171 

   172 

   172 text {*

   173 text {*

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

   174   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   {\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   a function assigning waiting queue to resources and a function assigning precedence to