12 vt ("valid'_state") and |
12 vt ("valid'_state") and |
13 runing ("running") and |
13 runing ("running") and |
14 birthtime ("last'_set") and |
14 birthtime ("last'_set") and |
15 If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and |
15 If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and |
16 Prc ("'(_, _')") and |
16 Prc ("'(_, _')") and |
|
17 holding ("holds") and |
|
18 waiting ("waits") and |
|
19 Th ("_") and |
|
20 Cs ("_") and |
|
21 readys ("ready") and |
17 DUMMY ("\<^raw:\mbox{$\_\!\_$}>") |
22 DUMMY ("\<^raw:\mbox{$\_\!\_$}>") |
18 (*>*) |
23 (*>*) |
19 |
24 |
20 section {* Introduction *} |
25 section {* Introduction *} |
21 |
26 |
154 The Priority Inheritance Protocol, short PIP, is a scheduling |
159 The Priority Inheritance Protocol, short PIP, is a scheduling |
155 algorithm for a single-processor system.\footnote{We shall come back |
160 algorithm for a single-processor system.\footnote{We shall come back |
156 later to the case of PIP on multi-processor systems.} Our model of |
161 later to the case of PIP on multi-processor systems.} Our model of |
157 PIP is based on Paulson's inductive approach to protocol |
162 PIP is based on Paulson's inductive approach to protocol |
158 verification \cite{Paulson98}, where the \emph{state} of a system is |
163 verification \cite{Paulson98}, where the \emph{state} of a system is |
159 given by a list of events that happened so far. \emph{Events} fall |
164 given by a list of events that happened so far. \emph{Events} in PIP fall |
160 into five categories defined as the datatype |
165 into five categories defined as the datatype |
161 |
166 |
162 \begin{isabelle}\ \ \ \ \ %%% |
167 \begin{isabelle}\ \ \ \ \ %%% |
163 \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l} |
168 \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l} |
164 \isacommand{datatype} event |
169 \isacommand{datatype} event |
190 @{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\ |
195 @{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\ |
191 \end{tabular}} |
196 \end{tabular}} |
192 \end{isabelle} |
197 \end{isabelle} |
193 |
198 |
194 \noindent |
199 \noindent |
195 Another calculates the priority for a thread @{text "th"}, defined as |
200 Another function calculates the priority for a thread @{text "th"}, defined as |
196 |
201 |
197 \begin{isabelle}\ \ \ \ \ %%% |
202 \begin{isabelle}\ \ \ \ \ %%% |
198 \mbox{\begin{tabular}{lcl} |
203 \mbox{\begin{tabular}{lcl} |
199 @{thm (lhs) original_priority.simps(1)[where thread="th"]} & @{text "\<equiv>"} & |
204 @{thm (lhs) original_priority.simps(1)[where thread="th"]} & @{text "\<equiv>"} & |
200 @{thm (rhs) original_priority.simps(1)[where thread="th"]}\\ |
205 @{thm (rhs) original_priority.simps(1)[where thread="th"]}\\ |
222 @{thm (rhs) birthtime.simps(3)[where thread="th" and thread'="th'"]}\\ |
227 @{thm (rhs) birthtime.simps(3)[where thread="th" and thread'="th'"]}\\ |
223 @{term "birthtime th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "birthtime th s"}\\ |
228 @{term "birthtime th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "birthtime th s"}\\ |
224 \end{tabular}} |
229 \end{tabular}} |
225 \end{isabelle} |
230 \end{isabelle} |
226 |
231 |
227 \footnote{Can Precedence be the real birth-time / or must be time precedence last set?} |
|
228 |
|
229 \noindent |
232 \noindent |
230 A \emph{precedence} of a thread @{text th} in a state @{text s} is a pair of |
233 In this definition @{term "length s"} stands for the length of the list |
231 natural numbers defined as |
234 of events @{text s}. Again the default value in this function is @{text 0} |
|
235 for threads that have not been created yet. A \emph{precedence} of a thread @{text th} in a |
|
236 state @{text s} is a pair of natural numbers defined as |
232 |
237 |
233 \begin{isabelle}\ \ \ \ \ %%% |
238 \begin{isabelle}\ \ \ \ \ %%% |
234 @{thm (rhs) preced_def[where thread="th"]} |
239 @{thm (rhs) preced_def[where thread="th"]} |
235 \end{isabelle} |
240 \end{isabelle} |
236 |
241 |
237 \noindent |
242 \noindent |
238 The point of precedences is to schedule threads not according to priorities (what should |
243 The point of precedences is to schedule threads not according to priorities (because what should |
239 we do in case two threads have the same priority), but according to precedences. |
244 we do in case two threads have the same priority), but according to precedences. |
240 Precedences allow us to always discriminate two threads with equal priority by |
245 Precedences allow us to always discriminate two threads with equal priority by |
241 tacking into account the time when the priority was last set. We order precedences so |
246 tacking into account the time when the priority was last set. We order precedences so |
242 that threads with the same priority get a higher precedence if their priority has been |
247 that threads with the same priority get a higher precedence if their priority has been |
243 set earlier, since for such threads it is more urgent to finish. In an impementation |
248 set earlier, since for such threads it is more urgent to finish. In an impementation |
249 this list is chosen to be in the one that is in possession of the |
254 this list is chosen to be in the one that is in possession of the |
250 ``lock'' of the corresponding resource. We model waiting queues as |
255 ``lock'' of the corresponding resource. We model waiting queues as |
251 functions, below abbreviated as @{text wq}, taking a resource as |
256 functions, below abbreviated as @{text wq}, taking a resource as |
252 argument and returning a list of threads. This allows us to define |
257 argument and returning a list of threads. This allows us to define |
253 when a thread \emph{holds}, respectively \emph{waits}, for a |
258 when a thread \emph{holds}, respectively \emph{waits}, for a |
254 resource @{text cs}. |
259 resource @{text cs} given a waiting queue function. |
255 |
260 |
256 \begin{isabelle}\ \ \ \ \ %%% |
261 \begin{isabelle}\ \ \ \ \ %%% |
257 \begin{tabular}{@ {}l} |
262 \begin{tabular}{@ {}l} |
258 @{thm cs_holding_def[where thread="th"]}\\ |
263 @{thm s_holding_def[where thread="th"]}\\ |
259 @{thm cs_waiting_def[where thread="th"]} |
264 @{thm s_waiting_def[where thread="th"]} |
260 \end{tabular} |
265 \end{tabular} |
261 \end{isabelle} |
266 \end{isabelle} |
262 |
267 |
|
268 \noindent |
|
269 In this definition we assume @{text "set"} converts a list into a set. |
|
270 |
|
271 \begin{isabelle}\ \ \ \ \ %%% |
|
272 \begin{tabular}{@ {}l} |
|
273 @{thm s_depend_def}\\ |
|
274 \end{tabular} |
|
275 \end{isabelle} |
|
276 |
|
277 \begin{isabelle}\ \ \ \ \ %%% |
|
278 \begin{tabular}{@ {}l} |
|
279 @{thm readys_def}\\ |
|
280 \end{tabular} |
|
281 \end{isabelle} |
|
282 |
|
283 \begin{isabelle}\ \ \ \ \ %%% |
|
284 \begin{tabular}{@ {}l} |
|
285 @{thm runing_def}\\ |
|
286 \end{tabular} |
|
287 \end{isabelle} |
263 |
288 |
264 |
289 |
265 resources |
290 resources |
|
291 |
|
292 done: threads not done: running |
266 |
293 |
267 step relation: |
294 step relation: |
268 |
295 |
269 \begin{center} |
296 \begin{center} |
270 \begin{tabular}{c} |
297 \begin{tabular}{c} |
271 @{thm[mode=Rule] thread_create[where thread=th]}\hspace{1cm} |
298 @{thm[mode=Rule] thread_create[where thread=th]}\hspace{1cm} |
272 @{thm[mode=Rule] thread_exit[where thread=th]}\medskip\\ |
299 @{thm[mode=Rule] thread_exit[where thread=th]}\medskip\\ |
273 |
300 |
|
301 @{thm[mode=Rule] thread_set[where thread=th]}\medskip\\ |
274 @{thm[mode=Rule] thread_P[where thread=th]}\medskip\\ |
302 @{thm[mode=Rule] thread_P[where thread=th]}\medskip\\ |
275 @{thm[mode=Rule] thread_V[where thread=th]}\\ |
303 @{thm[mode=Rule] thread_V[where thread=th]}\\ |
276 \end{tabular} |
304 \end{tabular} |
277 \end{center} |
305 \end{center} |
278 |
306 |