190 @{text "preced th s"}. |
190 @{text "preced th s"}. |
191 *} |
191 *} |
192 definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence" |
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)))" |
193 where "cpreced wq s = (\<lambda> th. Max ((\<lambda> th. preced th s) ` ({th} \<union> dependents wq th)))" |
194 |
194 |
|
195 (*<*) |
195 lemma |
196 lemma |
196 cpreced_def2: |
197 cpreced_def2: |
197 "cpreced wq s th = Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependents wq th})" |
198 "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependents wq th})" |
198 unfolding cpreced_def image_def |
199 unfolding cpreced_def image_def |
|
200 apply(rule eq_reflection) |
199 apply(rule arg_cong) |
201 apply(rule arg_cong) |
200 back |
202 back |
201 by (auto) |
203 by (auto) |
|
204 (*>*) |
|
205 |
|
206 abbreviation |
|
207 "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)" |
|
208 |
|
209 abbreviation |
|
210 "initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0" |
|
211 |
|
212 abbreviation |
|
213 "release qs \<equiv> case qs of |
|
214 [] => [] |
|
215 | (_#qs) => (SOME q. distinct q \<and> set q = set qs)" |
202 |
216 |
203 text {* \noindent |
217 text {* \noindent |
204 The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}. |
218 The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}. |
205 It is the key function to model Priority Inheritance: |
219 It is the key function to model Priority Inheritance: |
206 *} |
220 *} |
207 fun schs :: "state \<Rightarrow> schedule_state" |
221 fun schs :: "state \<Rightarrow> schedule_state" |
208 where |
222 where |
209 "schs [] = (| waiting_queue = \<lambda> cs. [], cur_preced = cpreced (\<lambda> cs. []) [] |)" | |
223 "schs [] = (| waiting_queue = \<lambda> cs. [], cur_preced = (\<lambda>_. Prc 0 0) |)" | |
210 |
224 |
211 -- {* |
225 -- {* |
212 \begin{minipage}{0.9\textwidth} |
226 \begin{minipage}{0.9\textwidth} |
213 \begin{enumerate} |
227 \begin{enumerate} |
214 \item @{text "ps"} is the schedule state of last moment. |
228 \item @{text "ps"} is the schedule state of last moment. |
215 \item @{text "pwq"} is the waiting queue function of last moment. |
229 \item @{text "pwq"} is the waiting queue function of last moment. |
216 \item @{text "pcp"} is the precedence function of last moment. |
230 \item @{text "pcp"} is the precedence function of last moment (NOT USED). |
217 \item @{text "nwq"} is the new waiting queue function. It is calculated using a @{text "case"} statement: |
231 \item @{text "nwq"} is the new waiting queue function. It is calculated using a @{text "case"} statement: |
218 \begin{enumerate} |
232 \begin{enumerate} |
219 \item If the happening event is @{text "P thread cs"}, @{text "thread"} is added to |
233 \item If the happening event is @{text "P thread cs"}, @{text "thread"} is added to |
220 the end of @{text "cs"}'s waiting queue. |
234 the end of @{text "cs"}'s waiting queue. |
221 \item If the happening event is @{text "V thread cs"} and @{text "s"} is a legal state, |
235 \item If the happening event is @{text "V thread cs"} and @{text "s"} is a legal state, |
231 function. The dependency of precedence function on waiting queue function is the reason to |
245 function. The dependency of precedence function on waiting queue function is the reason to |
232 put them in the same record so that they can evolve together. |
246 put them in the same record so that they can evolve together. |
233 \end{enumerate} |
247 \end{enumerate} |
234 \end{minipage} |
248 \end{minipage} |
235 *} |
249 *} |
236 "schs (e#s) = (let ps = schs s in |
250 "schs (Create th prio # s) = |
|
251 (let wq = waiting_queue (schs s) in |
|
252 (|waiting_queue = wq, cur_preced = cpreced wq (Create th prio # s)|))" |
|
253 | "schs (Exit th # s) = |
|
254 (let wq = waiting_queue (schs s) in |
|
255 (|waiting_queue = wq, cur_preced = cpreced wq (Exit th # s)|))" |
|
256 | "schs (Set th prio # s) = |
|
257 (let wq = waiting_queue (schs s) in |
|
258 (|waiting_queue = wq, cur_preced = cpreced wq (Set th prio # s)|))" |
|
259 | "schs (P th cs # s) = |
|
260 (let wq = waiting_queue (schs s) in |
|
261 let new_wq = wq(cs := (wq cs @ [th])) in |
|
262 (|waiting_queue = new_wq, cur_preced = cpreced new_wq (P th cs # s)|))" |
|
263 | "schs (V th cs # s) = |
|
264 (let wq = waiting_queue (schs s) in |
|
265 let new_wq = wq(cs := release (wq cs)) in |
|
266 (|waiting_queue = new_wq, cur_preced = cpreced new_wq (V th cs # s)|))" |
|
267 |
|
268 lemma cpreced_initial: |
|
269 "cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))" |
|
270 apply(simp add: cpreced_def) |
|
271 apply(simp add: cs_dependents_def cs_depend_def cs_waiting_def cs_holding_def) |
|
272 apply(simp add: preced_def) |
|
273 done |
|
274 |
|
275 lemma sch_old_def: |
|
276 "schs (e#s) = (let ps = schs s in |
237 let pwq = waiting_queue ps in |
277 let pwq = waiting_queue ps in |
238 let pcp = cur_preced ps in |
|
239 let nwq = case e of |
278 let nwq = case e of |
240 P th cs \<Rightarrow> pwq(cs:=(pwq cs @ [th])) | |
279 P th cs \<Rightarrow> pwq(cs:=(pwq cs @ [th])) | |
241 V th cs \<Rightarrow> let nq = case (pwq cs) of |
280 V th cs \<Rightarrow> let nq = case (pwq cs) of |
242 [] \<Rightarrow> [] | |
281 [] \<Rightarrow> [] | |
243 (_#qs) \<Rightarrow> (SOME q. distinct q \<and> set q = set qs) |
282 (_#qs) \<Rightarrow> (SOME q. distinct q \<and> set q = set qs) |
244 in pwq(cs:=nq) | |
283 in pwq(cs:=nq) | |
245 _ \<Rightarrow> pwq |
284 _ \<Rightarrow> pwq |
246 in let ncp = cpreced nwq (e#s) in |
285 in let ncp = cpreced nwq (e#s) in |
247 \<lparr>waiting_queue = nwq, cur_preced = ncp\<rparr> |
286 \<lparr>waiting_queue = nwq, cur_preced = ncp\<rparr> |
248 )" |
287 )" |
|
288 apply(cases e) |
|
289 apply(simp_all) |
|
290 done |
|
291 |
249 |
292 |
250 text {* |
293 text {* |
251 \noindent |
294 \noindent |
252 The following @{text "wq"} is a shorthand for @{text "waiting_queue"}. |
295 The following @{text "wq"} is a shorthand for @{text "waiting_queue"}. |
253 *} |
296 *} |