522 \end{isabelle} |
522 \end{isabelle} |
523 |
523 |
524 \noindent |
524 \noindent |
525 where @{text "SOME"} stands for Hilbert's epsilon and implements an arbitrary |
525 where @{text "SOME"} stands for Hilbert's epsilon and implements an arbitrary |
526 choice for the next waiting list. It just has to be a list of distinctive threads and |
526 choice for the next waiting list. It just has to be a list of distinctive threads and |
527 contain the same elements as @{text "qs"}. This gives for @{term V} the clause: |
527 contains the same elements as @{text "qs"}. This gives for @{term V} the clause: |
528 |
528 |
529 \begin{isabelle}\ \ \ \ \ %%% |
529 \begin{isabelle}\ \ \ \ \ %%% |
530 \begin{tabular}{@ {}l} |
530 \begin{tabular}{@ {}l} |
531 @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\ |
531 @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\ |
532 \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\ |
532 \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\ |
1016 we found that the formalisation can even help us with efficiently implementing it. |
1016 we found that the formalisation can even help us with efficiently implementing it. |
1017 For example Baker complained that calculating the current precedence |
1017 For example Baker complained that calculating the current precedence |
1018 in PIP is quite ``heavy weight'' in Linux (see the Introduction). |
1018 in PIP is quite ``heavy weight'' in Linux (see the Introduction). |
1019 In our model of PIP the current precedence of a thread in a state @{text s} |
1019 In our model of PIP the current precedence of a thread in a state @{text s} |
1020 depends on all its dependants---a ``global'' transitive notion, |
1020 depends on all its dependants---a ``global'' transitive notion, |
1021 which is indeed heavy weight (see Def.~shown in \eqref{cpreced}). |
1021 which is indeed heavy weight (see Definition shown in \eqref{cpreced}). |
1022 We can however improve upon this. For this let us define the notion |
1022 We can however improve upon this. For this let us define the notion |
1023 of @{term children} of a thread @{text th} in a state @{text s} as |
1023 of @{term children} of a thread @{text th} in a state @{text s} as |
1024 |
1024 |
1025 \begin{isabelle}\ \ \ \ \ %%% |
1025 \begin{isabelle}\ \ \ \ \ %%% |
1026 \begin{tabular}{@ {}l} |
1026 \begin{tabular}{@ {}l} |
1462 To us, it seems sound reasoning about scheduling algorithms is fiendishly difficult |
1462 To us, it seems sound reasoning about scheduling algorithms is fiendishly difficult |
1463 if done informally by ``pencil-and-paper''. This is proved by the flawed proof |
1463 if done informally by ``pencil-and-paper''. This is proved by the flawed proof |
1464 in the paper by Sha et al.~\cite{Sha90} and also by Regehr \cite{Regehr} who |
1464 in the paper by Sha et al.~\cite{Sha90} and also by Regehr \cite{Regehr} who |
1465 pointed out an error in a paper about Preemption |
1465 pointed out an error in a paper about Preemption |
1466 Threshold Scheduling \cite{ThreadX}. The use of a theorem prover was |
1466 Threshold Scheduling \cite{ThreadX}. The use of a theorem prover was |
1467 invaluable to us in order to feel confident about the correctness of our results. |
1467 invaluable to us in order to be confident about the correctness of our reasoning |
|
1468 (no case can be overlooked). |
1468 The most closely related work to ours is the formal verification in |
1469 The most closely related work to ours is the formal verification in |
1469 PVS of the Priority Ceiling Protocol done by Dutertre |
1470 PVS of the Priority Ceiling Protocol done by Dutertre |
1470 \cite{dutertre99b}---another solution to the Priority Inversion |
1471 \cite{dutertre99b}---another solution to the Priority Inversion |
1471 problem, which however needs static analysis of programs in order to |
1472 problem, which however needs static analysis of programs in order to |
1472 avoid it. There have been earlier formal investigations |
1473 avoid it. There have been earlier formal investigations |