157 queue function @{text "wq"}. |
157 queue function @{text "wq"}. |
158 \end{minipage} |
158 \end{minipage} |
159 *} |
159 *} |
160 cs_depend_def: |
160 cs_depend_def: |
161 "depend (wq::cs \<Rightarrow> thread list) \<equiv> |
161 "depend (wq::cs \<Rightarrow> thread list) \<equiv> |
162 {(Th t, Cs c) | t c. waiting wq t c} \<union> {(Cs c, Th t) | c t. holding wq t c}" |
162 {(Th th, Cs cs) | th cs. waiting wq th cs} \<union> {(Cs cs, Th th) | cs th. holding wq th cs}" |
163 -- {* |
163 -- {* |
164 \begin{minipage}{0.9\textwidth} |
164 \begin{minipage}{0.9\textwidth} |
165 The following @{text "dependents wq th"} represents the set of threads which are depending on |
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"}: |
166 thread @{text "th"} in Resource Allocation Graph @{text "depend wq"}: |
167 \end{minipage} |
167 \end{minipage} |
262 "holding (s::state) thread cs \<equiv> (thread \<in> set (wq s cs) \<and> thread = hd (wq s cs))" |
262 "holding (s::state) thread cs \<equiv> (thread \<in> set (wq s cs) \<and> thread = hd (wq s cs))" |
263 s_waiting_def: |
263 s_waiting_def: |
264 "waiting (s::state) thread cs \<equiv> (thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs))" |
264 "waiting (s::state) thread cs \<equiv> (thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs))" |
265 s_depend_def: |
265 s_depend_def: |
266 "depend (s::state) \<equiv> |
266 "depend (s::state) \<equiv> |
267 {(Th t, Cs c) | t c. waiting (wq s) t c} \<union> {(Cs c, Th t) | c t. holding (wq s) t c}" |
267 {(Th th, Cs cs) | th cs. waiting (wq s) th cs} \<union> {(Cs cs, Th th) | cs th. holding (wq s) th cs}" |
268 s_dependents_def: |
268 s_dependents_def: |
269 "dependents (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}" |
269 "dependents (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}" |
270 |
270 |
271 text {* |
271 text {* |
272 The following function @{text "readys"} calculates the set of ready threads. A thread is {\em ready} |
272 The following function @{text "readys"} calculates the set of ready threads. A thread is {\em ready} |
273 for running if it is a live thread and it is not waiting for any critical resource. |
273 for running if it is a live thread and it is not waiting for any critical resource. |
274 *} |
274 *} |
275 definition readys :: "state \<Rightarrow> thread set" |
275 definition readys :: "state \<Rightarrow> thread set" |
276 where "readys s = {thread . thread \<in> threads s \<and> (\<forall> cs. \<not> waiting s thread cs)}" |
276 where "readys s \<equiv> {th . th \<in> threads s \<and> (\<forall> cs. \<not> waiting s th cs)}" |
277 |
277 |
278 text {* \noindent |
278 text {* \noindent |
279 The following function @{text "runing"} calculates the set of running thread, which is the ready |
279 The following function @{text "runing"} calculates the set of running thread, which is the ready |
280 thread with the highest precedence. |
280 thread with the highest precedence. |
281 *} |
281 *} |