111 text {* |
111 text {* |
112 \input{../../generated/PrioGDef} |
112 \input{../../generated/PrioGDef} |
113 *} |
113 *} |
114 |
114 |
115 section {* General properties of Priority Inheritance \label{general} *} |
115 section {* General properties of Priority Inheritance \label{general} *} |
|
116 (*<*) |
|
117 ML {* |
|
118 val () = show_question_marks_default := false; |
|
119 *} |
|
120 (*>*) |
|
121 |
|
122 text {* |
|
123 The following are several very basic prioprites: |
|
124 \begin{enumerate} |
|
125 \item All runing threads must be ready (@{text "runing_ready"}): |
|
126 @{thm[display] "runing_ready"} |
|
127 \item All ready threads must be living (@{text "readys_threads"}): |
|
128 @{thm[display] "readys_threads"} |
|
129 \item There are finite many living threads at any moment (@{text "finite_threads"}): |
|
130 @{thm[display] "finite_threads"} |
|
131 \item Every waiting queue does not contain duplcated elements (@{text "wq_distinct"}): |
|
132 @{thm[display] "wq_distinct"} |
|
133 \item All threads in waiting queues are living threads (@{text "wq_threads"}): |
|
134 @{thm[display] "wq_threads"} |
|
135 \item The event which can get a thread into waiting queue must be @{term "P"}-events |
|
136 (@{text "block_pre"}): |
|
137 @{thm[display] "block_pre"} |
|
138 \item A thread may never wait for two different critical resources |
|
139 (@{text "waiting_unique"}): |
|
140 @{thm[display] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]} |
|
141 \item Every resource can only be held by one thread |
|
142 (@{text "held_unique"}): |
|
143 @{thm[display] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]} |
|
144 \item Every living thread has an unique precedence |
|
145 (@{text "preced_unique"}): |
|
146 @{thm[display] preced_unique[of "th\<^isub>1" _ "th\<^isub>2"]} |
|
147 \end{enumerate} |
|
148 *} |
|
149 |
|
150 text {* \noindent |
|
151 The following lemmas show how RAG is changed with the execution of events: |
|
152 \begin{enumerate} |
|
153 \item Execution of @{term "Set"} does not change RAG (@{text "depend_set_unchanged"}): |
|
154 @{thm[display] depend_set_unchanged} |
|
155 \item Execution of @{term "Create"} does not change RAG (@{text "depend_create_unchanged"}): |
|
156 @{thm[display] depend_create_unchanged} |
|
157 \item Execution of @{term "Exit"} does not change RAG (@{text "depend_exit_unchanged"}): |
|
158 @{thm[display] depend_exit_unchanged} |
|
159 \item Execution of @{term "P"} (@{text "step_depend_p"}): |
|
160 @{thm[display] step_depend_p} |
|
161 \item Execution of @{term "V"} (@{text "step_depend_v"}): |
|
162 @{thm[display] step_depend_v} |
|
163 \end{enumerate} |
|
164 *} |
|
165 |
|
166 text {* \noindent |
|
167 These properties are used to derive the following important results about RAG: |
|
168 \begin{enumerate} |
|
169 \item RAG is loop free (@{text "acyclic_depend"}): |
|
170 @{thm [display] acyclic_depend} |
|
171 \item RAGs are finite (@{text "finite_depend"}): |
|
172 @{thm [display] finite_depend} |
|
173 \item Reverse paths in RAG are well founded (@{text "wf_dep_converse"}): |
|
174 @{thm [display] wf_dep_converse} |
|
175 \item The dependence relation represented by RAG has a tree structure (@{text "unique_depend"}): |
|
176 @{thm [display] unique_depend[of _ _ "n\<^isub>1" "n\<^isub>2"]} |
|
177 \item All threads in RAG are living threads |
|
178 (@{text "dm_depend_threads"} and @{text "range_in"}): |
|
179 @{thm [display] dm_depend_threads range_in} |
|
180 \end{enumerate} |
|
181 *} |
|
182 |
|
183 text {* \noindent |
|
184 The following lemmas show how every node in RAG can be chased to ready threads: |
|
185 \begin{enumerate} |
|
186 \item Every node in RAG can be chased to a ready thread (@{text "chain_building"}): |
|
187 @{thm [display] chain_building[rule_format]} |
|
188 \item The ready thread chased to is unique (@{text "dchain_unique"}): |
|
189 @{thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]} |
|
190 \end{enumerate} |
|
191 *} |
|
192 |
|
193 text {* \noindent |
|
194 Properties about @{term "next_th"}: |
|
195 \begin{enumerate} |
|
196 \item The thread taking over is different from the thread which is releasing |
|
197 (@{text "next_th_neq"}): |
|
198 @{thm [display] next_th_neq} |
|
199 \item The thread taking over is unique |
|
200 (@{text "next_th_unique"}): |
|
201 @{thm [display] next_th_unique[of _ _ _ "th\<^isub>1" "th\<^isub>2"]} |
|
202 \end{enumerate} |
|
203 *} |
|
204 |
|
205 text {* \noindent |
|
206 Some deeper results about the system: |
|
207 \begin{enumerate} |
|
208 \item There can only be one running thread (@{text "runing_unique"}): |
|
209 @{thm [display] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]} |
|
210 \item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}): |
|
211 @{thm [display] max_cp_eq} |
|
212 \item There must be one ready thread having the max @{term "cp"}-value |
|
213 (@{text "max_cp_readys_threads"}): |
|
214 @{thm [display] max_cp_readys_threads} |
|
215 \end{enumerate} |
|
216 *} |
|
217 |
|
218 text {* \noindent |
|
219 The relationship between the count of @{text "P"} and @{text "V"} and the number of |
|
220 critical resources held by a thread is given as follows: |
|
221 \begin{enumerate} |
|
222 \item The @{term "V"}-operation decreases the number of critical resources |
|
223 one thread holds (@{text "cntCS_v_dec"}) |
|
224 @{thm [display] cntCS_v_dec} |
|
225 \item The number of @{text "V"} never exceeds the number of @{text "P"} |
|
226 (@{text "cnp_cnv_cncs"}): |
|
227 @{thm [display] cnp_cnv_cncs} |
|
228 \item The number of @{text "V"} equals the number of @{text "P"} when |
|
229 the relevant thread is not living: |
|
230 (@{text "cnp_cnv_eq"}): |
|
231 @{thm [display] cnp_cnv_eq} |
|
232 \item When a thread is not living, it does not hold any critical resource |
|
233 (@{text "not_thread_holdents"}): |
|
234 @{thm [display] not_thread_holdents} |
|
235 \item When the number of @{text "P"} equals the number of @{text "V"}, the relevant |
|
236 thread does not hold any critical resource, therefore no thread can depend on it |
|
237 (@{text "count_eq_dependents"}): |
|
238 @{thm [display] count_eq_dependents} |
|
239 \end{enumerate} |
|
240 *} |
116 |
241 |
117 section {* Key properties \label{extension} *} |
242 section {* Key properties \label{extension} *} |
118 |
243 |
|
244 (*<*) |
|
245 context extend_highest_gen |
|
246 begin |
|
247 (*>*) |
|
248 |
|
249 text {* |
|
250 The essential of {\em Priority Inheritance} is to avoid indefinite priority inversion. For this |
|
251 purpose, we need to investigate what happens after one thread takes the highest precedence. |
|
252 A locale is used to describe such a situation, which assumes: |
|
253 \begin{enumerate} |
|
254 \item @{term "s"} is a valid state (@{text "vt_s"}): |
|
255 @{thm vt_s}. |
|
256 \item @{term "th"} is a living thread in @{term "s"} (@{text "threads_s"}): |
|
257 @{thm threads_s}. |
|
258 \item @{term "th"} has the highest precedence in @{term "s"} (@{text "highest"}): |
|
259 @{thm highest}. |
|
260 \item The precedence of @{term "th"} is @{term "Prc prio tm"} (@{text "preced_th"}): |
|
261 @{thm preced_th}. |
|
262 \end{enumerate} |
|
263 *} |
|
264 |
|
265 text {* \noindent |
|
266 Under these assumptions, some basic priority can be derived for @{term "th"}: |
|
267 \begin{enumerate} |
|
268 \item The current precedence of @{term "th"} equals its own precedence (@{text "eq_cp_s_th"}): |
|
269 @{thm [display] eq_cp_s_th} |
|
270 \item The current precedence of @{term "th"} is the highest precedence in |
|
271 the system (@{text "highest_cp_preced"}): |
|
272 @{thm [display] highest_cp_preced} |
|
273 \item The precedence of @{term "th"} is the highest precedence |
|
274 in the system (@{text "highest_preced_thread"}): |
|
275 @{thm [display] highest_preced_thread} |
|
276 \item The current precedence of @{term "th"} is the highest current precedence |
|
277 in the system (@{text "highest'"}): |
|
278 @{thm [display] highest'} |
|
279 \end{enumerate} |
|
280 *} |
|
281 |
|
282 text {* \noindent |
|
283 To analysis what happens after state @{term "s"} a sub-locale is defined, which |
|
284 assumes: |
|
285 \begin{enumerate} |
|
286 \item @{term "t"} is a valid extension of @{term "s"} (@{text "vt_t"}): @{thm vt_t}. |
|
287 \item Any thread created in @{term "t"} has priority no higher than @{term "prio"}, therefore |
|
288 its precedence can not be higher than @{term "th"}, therefore |
|
289 @{term "th"} remain to be the one with the highest precedence |
|
290 (@{text "create_low"}): |
|
291 @{thm [display] create_low} |
|
292 \item Any adjustment of priority in |
|
293 @{term "t"} does not happen to @{term "th"} and |
|
294 the priority set is no higher than @{term "prio"}, therefore |
|
295 @{term "th"} remain to be the one with the highest precedence (@{text "set_diff_low"}): |
|
296 @{thm [display] set_diff_low} |
|
297 \item Since we are investigating what happens to @{term "th"}, it is assumed |
|
298 @{term "th"} does not exit during @{term "t"} (@{text "exit_diff"}): |
|
299 @{thm [display] exit_diff} |
|
300 \end{enumerate} |
|
301 *} |
|
302 |
|
303 text {* \noindent |
|
304 All these assumptions are put into a predicate @{term "extend_highest_gen"}. |
|
305 It can be proved that @{term "extend_highest_gen"} holds |
|
306 for any moment @{text "i"} in it @{term "t"} (@{text "red_moment"}): |
|
307 @{thm [display] red_moment} |
|
308 |
|
309 From this, an induction principle can be derived for @{text "t"}, so that |
|
310 properties already derived for @{term "t"} can be applied to any prefix |
|
311 of @{text "t"} in the proof of new properties |
|
312 about @{term "t"} (@{text "ind"}): |
|
313 \begin{center} |
|
314 @{thm[display] ind} |
|
315 \end{center} |
|
316 |
|
317 The following properties can be proved about @{term "th"} in @{term "t"}: |
|
318 \begin{enumerate} |
|
319 \item In @{term "t"}, thread @{term "th"} is kept live and its |
|
320 precedence is preserved as well |
|
321 (@{text "th_kept"}): |
|
322 @{thm [display] th_kept} |
|
323 \item In @{term "t"}, thread @{term "th"}'s precedence is always the maximum among |
|
324 all living threads |
|
325 (@{text "max_preced"}): |
|
326 @{thm [display] max_preced} |
|
327 \item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum precedence |
|
328 among all living threads |
|
329 (@{text "th_cp_max_preced"}): |
|
330 @{thm [display] th_cp_max_preced} |
|
331 \item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum current |
|
332 precedence among all living threads |
|
333 (@{text "th_cp_max"}): |
|
334 @{thm [display] th_cp_max} |
|
335 \item In @{term "t"}, thread @{term "th"}'s current precedence equals its precedence at moment |
|
336 @{term "s"} |
|
337 (@{text "th_cp_preced"}): |
|
338 @{thm [display] th_cp_preced} |
|
339 \end{enumerate} |
|
340 *} |
|
341 |
|
342 text {* \noindent |
|
343 The main theorem is to characterizing the running thread during @{term "t"} |
|
344 (@{text "runing_inversion_2"}): |
|
345 @{thm [display] runing_inversion_2} |
|
346 According to this, if a thread is running, it is either @{term "th"} or was |
|
347 already live and held some resource |
|
348 at moment @{text "s"} (expressed by: @{text "cntV s th' < cntP s th'"}). |
|
349 |
|
350 Since there are only finite many threads live and holding some resource at any moment, |
|
351 if every such thread can release all its resources in finite duration, then after finite |
|
352 duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen |
|
353 then. |
|
354 *} |
|
355 |
|
356 (*<*) |
|
357 end |
|
358 (*>*) |
|
359 |
119 section {* Properties to guide implementation \label{implement} *} |
360 section {* Properties to guide implementation \label{implement} *} |
|
361 |
|
362 text {* |
|
363 The properties (especially @{text "runing_inversion_2"}) convinced us that model defined |
|
364 in section \ref{model} does prevent indefinite priority inversion and therefore fulfills |
|
365 the fundamental requirement of Priority Inheritance protocol. Another purpose of this paper |
|
366 is to show how this model can be used to guide a concrete implementation. |
|
367 *} |
|
368 |
120 |
369 |
121 section {* Related works \label{related} *} |
370 section {* Related works \label{related} *} |
122 |
371 |
123 text {* |
372 text {* |
124 \begin{enumerate} |
373 \begin{enumerate} |