108 to discriminate threads with the same priority by giving threads whose priority |
108 to discriminate threads with the same priority by giving threads whose priority |
109 is assigned earlier higher precedences, becasue such threads are more urgent to finish. |
109 is assigned earlier higher precedences, becasue such threads are more urgent to finish. |
110 This explains the following definition: |
110 This explains the following definition: |
111 *} |
111 *} |
112 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence" |
112 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence" |
113 where "preced thread s = Prc (original_priority thread s) (birthtime thread s)" |
113 where "preced thread s \<equiv> Prc (original_priority thread s) (birthtime thread s)" |
114 |
114 |
115 |
115 |
116 text {* |
116 text {* |
117 \noindent |
117 \noindent |
118 A number of important notions are defined here: |
118 A number of important notions are defined here: |
187 inherited from the maximum of all its dependents, i.e. the threads which are waiting |
187 inherited from the maximum of all its dependents, i.e. the threads which are waiting |
188 directly or indirectly waiting for some resources from it. If no such thread exits, |
188 directly or indirectly waiting for some resources from it. If no such thread exits, |
189 @{text "th"}'s {\em current precedence} equals its original precedence, i.e. |
189 @{text "th"}'s {\em current precedence} equals its original precedence, i.e. |
190 @{text "preced th s"}. |
190 @{text "preced th s"}. |
191 *} |
191 *} |
192 definition cpreced :: "state \<Rightarrow> (cs \<Rightarrow> thread list) \<Rightarrow> thread \<Rightarrow> precedence" |
192 definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence" |
193 where "cpreced s wq = (\<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 |
|
195 lemma |
|
196 cpreced_def2: |
|
197 "cpreced wq s th = Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependents wq th})" |
|
198 unfolding cpreced_def image_def |
|
199 apply(rule arg_cong) |
|
200 back |
|
201 by (auto) |
194 |
202 |
195 text {* \noindent |
203 text {* \noindent |
196 The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}. |
204 The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}. |
197 It is the key function to model Priority Inheritance: |
205 It is the key function to model Priority Inheritance: |
198 *} |
206 *} |
199 fun schs :: "state \<Rightarrow> schedule_state" |
207 fun schs :: "state \<Rightarrow> schedule_state" |
200 where "schs [] = \<lparr>waiting_queue = \<lambda> cs. [], cur_preced = cpreced [] (\<lambda> cs. [])\<rparr>" | |
208 where |
|
209 "schs [] = (| waiting_queue = \<lambda> cs. [], cur_preced = cpreced (\<lambda> cs. []) [] |)" | |
|
210 |
201 -- {* |
211 -- {* |
202 \begin{minipage}{0.9\textwidth} |
212 \begin{minipage}{0.9\textwidth} |
203 \begin{enumerate} |
213 \begin{enumerate} |
204 \item @{text "ps"} is the schedule state of last moment. |
214 \item @{text "ps"} is the schedule state of last moment. |
205 \item @{text "pwq"} is the waiting queue function of last moment. |
215 \item @{text "pwq"} is the waiting queue function of last moment. |
225 *} |
235 *} |
226 "schs (e#s) = (let ps = schs s in |
236 "schs (e#s) = (let ps = schs s in |
227 let pwq = waiting_queue ps in |
237 let pwq = waiting_queue ps in |
228 let pcp = cur_preced ps in |
238 let pcp = cur_preced ps in |
229 let nwq = case e of |
239 let nwq = case e of |
230 P thread cs \<Rightarrow> pwq(cs:=(pwq cs @ [thread])) | |
240 P th cs \<Rightarrow> pwq(cs:=(pwq cs @ [th])) | |
231 V thread cs \<Rightarrow> let nq = case (pwq cs) of |
241 V th cs \<Rightarrow> let nq = case (pwq cs) of |
232 [] \<Rightarrow> [] | |
242 [] \<Rightarrow> [] | |
233 (th'#qs) \<Rightarrow> (SOME q. distinct q \<and> set q = set qs) |
243 (_#qs) \<Rightarrow> (SOME q. distinct q \<and> set q = set qs) |
234 in pwq(cs:=nq) | |
244 in pwq(cs:=nq) | |
235 _ \<Rightarrow> pwq |
245 _ \<Rightarrow> pwq |
236 in let ncp = cpreced (e#s) nwq in |
246 in let ncp = cpreced nwq (e#s) in |
237 \<lparr>waiting_queue = nwq, cur_preced = ncp\<rparr> |
247 \<lparr>waiting_queue = nwq, cur_preced = ncp\<rparr> |
238 )" |
248 )" |
239 |
249 |
240 text {* |
250 text {* |
241 \noindent |
251 \noindent |