150 behaviour for $L$ is to switch to the highest remaining priority of |
150 behaviour for $L$ is to switch to the highest remaining priority of |
151 the threads that it blocks. A similar error is made in the textbook |
151 the threads that it blocks. A similar error is made in the textbook |
152 \cite[Section 2.3.1]{book} which specifies for a process that |
152 \cite[Section 2.3.1]{book} which specifies for a process that |
153 inherited a higher priority and exits a critical section ``{\it it resumes |
153 inherited a higher priority and exits a critical section ``{\it it resumes |
154 the priority it had at the point of entry into the critical section}''. |
154 the priority it had at the point of entry into the critical section}''. |
|
155 The same error can also be found in the more recent textbook |
|
156 \cite[Page 119]{Laplante11} which states ``{\it when [the task] exits the critical |
|
157 section that caused the block, it reverts to the priority it had when |
|
158 it entered that section}''. |
155 |
159 |
156 While \cite{book} and |
160 While \cite{Laplante11,book,Sha90} are the only formal publications we have |
157 \cite{Sha90} are the only formal publications we have |
|
158 found that describe the incorrect behaviour, not all, but many |
161 found that describe the incorrect behaviour, not all, but many |
159 informal\footnote{informal as in ``found on the Web''} |
162 informal\footnote{informal as in ``found on the Web''} |
160 descriptions of PIP overlook the possibility that another |
163 descriptions of PIP overlook the possibility that another |
161 high-priority might wait for a low-priority process to finish. |
164 high-priority might wait for a low-priority process to finish. |
162 The advantage of formalising the |
165 The advantage of formalising the |
1562 if done informally by ``pencil-and-paper''. We infer this from the flawed proof |
1565 if done informally by ``pencil-and-paper''. We infer this from the flawed proof |
1563 in the paper by Sha et al.~\cite{Sha90} and also from \cite{Regehr} where Regehr |
1566 in the paper by Sha et al.~\cite{Sha90} and also from \cite{Regehr} where Regehr |
1564 points out an error in a paper about Preemption |
1567 points out an error in a paper about Preemption |
1565 Threshold Scheduling \cite{ThreadX}. The use of a theorem prover was |
1568 Threshold Scheduling \cite{ThreadX}. The use of a theorem prover was |
1566 invaluable to us in order to be confident about the correctness of our reasoning |
1569 invaluable to us in order to be confident about the correctness of our reasoning |
1567 (no case can be overlooked). |
1570 (for example no corner case can be overlooked). |
1568 The most closely related work to ours is the formal verification in |
1571 The most closely related work to ours is the formal verification in |
1569 PVS of the Priority Ceiling Protocol done by Dutertre |
1572 PVS of the Priority Ceiling Protocol done by Dutertre |
1570 \cite{dutertre99b}---another solution to the Priority Inversion |
1573 \cite{dutertre99b}---another solution to the Priority Inversion |
1571 problem, which however needs static analysis of programs in order to |
1574 problem, which however needs static analysis of programs in order to |
1572 avoid it. There have been earlier formal investigations |
1575 avoid it. There have been earlier formal investigations |