91 priority $M$. While a few other solutions exist for the Priority |
91 priority $M$. While a few other solutions exist for the Priority |
92 Inversion problem, PIP is one that is widely deployed and |
92 Inversion problem, PIP is one that is widely deployed and |
93 implemented. This includes VxWorks (a proprietary real-time OS used |
93 implemented. This includes VxWorks (a proprietary real-time OS used |
94 in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's |
94 in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's |
95 ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for |
95 ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for |
96 example in libraries for FreeBSD, Solaris and Linux. |
96 example in libraries for FreeBSD, Solaris and Linux. ({\bf Is this True?}) |
97 |
97 |
98 One advantage of PIP is that increasing the priority of a thread |
98 One advantage of PIP is that increasing the priority of a thread |
99 can be dynamically calculated by the scheduler. This is in contrast |
99 can be dynamically calculated by the scheduler. This is in contrast |
100 to, for example, \emph{Priority Ceiling} \cite{Sha90}, another |
100 to, for example, \emph{Priority Ceiling} \cite{Sha90}, another |
101 solution to the Priority Inversion problem, which requires static |
101 solution to the Priority Inversion problem, which requires static |
165 \noindent |
165 \noindent |
166 {\bf Contributions:} There have been earlier formal investigations |
166 {\bf Contributions:} There have been earlier formal investigations |
167 into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model |
167 into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model |
168 checking techniques. This paper presents a formalised and |
168 checking techniques. This paper presents a formalised and |
169 mechanically checked proof for the correctness of PIP (to our |
169 mechanically checked proof for the correctness of PIP (to our |
170 knowledge the first one; the earlier informal proof by Sha et |
170 knowledge the first one). |
171 al.~\cite{Sha90} is flawed). In contrast to model checking, our |
171 %; the earlier informal proof by Sha et |
|
172 %al.~\cite{Sha90} is flawed). |
|
173 In contrast to model checking, our |
172 formalisation provides insight into why PIP is correct and allows us |
174 formalisation provides insight into why PIP is correct and allows us |
173 to prove stronger properties that, as we will show, can inform an |
175 to prove stronger properties that, as we will show, can inform an |
174 efficient implementation. For example, we found by ``playing'' with the formalisation |
176 efficient implementation. For example, we found by ``playing'' with the formalisation |
175 that the choice of the next thread to take over a lock when a |
177 that the choice of the next thread to take over a lock when a |
176 resource is released is irrelevant for PIP being correct---a fact |
178 resource is released is irrelevant for PIP being correct---a fact |
177 that has not been mentioned in the relevant literature. |
179 that has not been mentioned in the literature. |
178 *} |
180 *} |
179 |
181 |
180 section {* Formal Model of the Priority Inheritance Protocol *} |
182 section {* Formal Model of the Priority Inheritance Protocol *} |
181 |
183 |
182 text {* |
184 text {* |