119 where "preced thread s \<equiv> Prc (priority thread s) (last_set thread s)" |
119 where "preced thread s \<equiv> Prc (priority thread s) (last_set thread s)" |
120 |
120 |
121 |
121 |
122 text {* |
122 text {* |
123 \noindent |
123 \noindent |
124 A number of important notions in PIP are represented as functions defined |
124 A number of important notions in PIP are represented as the following functions, |
125 in terms of the waiting queues of the system, where the waiting queues |
125 defined in terms of the waiting queues of the system, where the waiting queues |
126 , as a whole, is represented by the @{text "wq"} argument of every notion function. |
126 , as a whole, is represented by the @{text "wq"} argument of every notion function. |
127 The @{text "wq"} argument is itself a functions which |
127 The @{text "wq"} argument is itself a functions which maps every critical resource |
128 maps every critical resource @{text "cs"} to the list of threads which are holding or waiting for it. |
128 @{text "cs"} to the list of threads which are holding or waiting for it. |
129 The thread at the head of this list is designated as the thread which is current |
129 The thread at the head of this list is designated as the thread which is current |
130 holding the resrouce, which is slightly different from tradition where |
130 holding the resrouce, which is slightly different from tradition where |
131 all threads in the waiting queue are considered as waiting for the resource. |
131 all threads in the waiting queue are considered as waiting for the resource. |
132 *} |
132 *} |
133 |
133 |
175 \end{minipage} |
175 \end{minipage} |
176 *} |
176 *} |
177 cs_dependants_def: |
177 cs_dependants_def: |
178 "dependants (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}" |
178 "dependants (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}" |
179 |
179 |
180 (* I stop here for the moment ccc *) |
|
181 |
|
182 text {* |
180 text {* |
183 The data structure used by the operating system for scheduling is referred to as |
181 The data structure used by the operating system for scheduling is referred to as |
184 {\em schedule state}. It is represented as a record consisting of |
182 {\em schedule state}. It is represented as a record consisting of |
185 a function assigning waiting queue to resources and a function assigning precedence to |
183 a function assigning waiting queue to resources |
186 threads: |
184 (to be used as the @{text "wq"} argument in @{text "holding"}, @{text "waiting"} |
187 *} |
185 and @{text "RAG"}, etc) and a function assigning precedence to threads: |
|
186 *} |
|
187 |
188 record schedule_state = |
188 record schedule_state = |
189 wq_fun :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *} |
189 wq_fun :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *} |
190 cprec_fun :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *} |
190 cprec_fun :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *} |
191 |
191 |
192 text {* \noindent |
192 text {* \noindent |
211 apply(rule eq_reflection) |
211 apply(rule eq_reflection) |
212 apply(rule_tac f="Max" in arg_cong) |
212 apply(rule_tac f="Max" in arg_cong) |
213 by (auto) |
213 by (auto) |
214 (*>*) |
214 (*>*) |
215 |
215 |
|
216 (* |
216 abbreviation |
217 abbreviation |
217 "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)" |
218 "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)" |
218 |
219 |
219 abbreviation |
220 abbreviation |
220 "initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0" |
221 "initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0" |
221 |
222 *) |
|
223 |
|
224 text {* \noindent |
|
225 Assuming @{text "qs"} be the waiting queue of a critical resource, |
|
226 the following abbreviation "release qs" is the waiting queue after the thread |
|
227 holding the resource (which is thread at the head of @{text "qs"}) released |
|
228 the resource: |
|
229 *} |
222 abbreviation |
230 abbreviation |
223 "release qs \<equiv> case qs of |
231 "release qs \<equiv> case qs of |
224 [] => [] |
232 [] => [] |
225 | (_#qs) => (SOME q. distinct q \<and> set q = set qs)" |
233 | (_#qs') => (SOME q. distinct q \<and> set q = set qs')" |
226 |
234 text {* \noindent |
227 text {* \noindent |
235 It can be seen from the definition that the thread at the head of @{text "qs"} is removed |
228 The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}. |
236 from the return value, and the value @{term "q"} is an reordering of @{text "qs'"}, the |
229 It is the key function to model Priority Inheritance: |
237 tail of @{text "qs"}. Through this reordering, one of the waiting threads (those in @{text "qs'"} } |
|
238 is chosen nondeterministically to be the head of the new queue @{text "q"}. |
|
239 Therefore, this thread is the one who takes over the resource. This is a little better different |
|
240 from common sense that the thread who comes the earliest should take over. |
|
241 The intention of this definition is to show that the choice of which thread to take over the |
|
242 release resource does not affect the correctness of the PIP protocol. |
|
243 *} |
|
244 |
|
245 (* ccc *) |
|
246 |
|
247 text {* \noindent |
|
248 The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"} |
|
249 out of the current system state @{text "s"}. |
|
250 It is the central function to model Priority Inheritance: |
230 *} |
251 *} |
231 fun schs :: "state \<Rightarrow> schedule_state" |
252 fun schs :: "state \<Rightarrow> schedule_state" |
232 where |
253 where |
233 "schs [] = (| wq_fun = \<lambda> cs. [], cprec_fun = (\<lambda>_. Prc 0 0) |)" | |
254 "schs [] = (| wq_fun = \<lambda> cs. [], cprec_fun = (\<lambda>_. Prc 0 0) |)" | |
234 |
255 |