152 \noindent |
152 \noindent |
153 {\bf Contributions:} There have been earlier formal investigations |
153 {\bf Contributions:} There have been earlier formal investigations |
154 into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model |
154 into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model |
155 checking techniques. This paper presents a formalised and |
155 checking techniques. This paper presents a formalised and |
156 mechanically checked proof for the correctness of PIP (to our |
156 mechanically checked proof for the correctness of PIP (to our |
157 knowledge the first one; an earlier informal proof by Sha et |
157 knowledge the first one; the earlier informal proof by Sha et |
158 al.~\cite{Sha90} is flawed). In contrast to model checking, our |
158 al.~\cite{Sha90} is flawed). In contrast to model checking, our |
159 formalisation provides insight into why PIP is correct and allows us |
159 formalisation provides insight into why PIP is correct and allows us |
160 to prove stronger properties that, as we will show, inform an |
160 to prove stronger properties that, as we will show, inform an |
161 implementation. For example, we found by ``playing'' with the formalisation |
161 implementation. For example, we found by ``playing'' with the formalisation |
162 that the choice of the next thread to take over a lock when a |
162 that the choice of the next thread to take over a lock when a |
163 resource is released is irrelevant for PIP being correct. |
163 resource is released is irrelevant for PIP being correct. Something |
|
164 which has not been mentioned in the relevant literature. |
164 *} |
165 *} |
165 |
166 |
166 section {* Formal Model of the Priority Inheritance Protocol *} |
167 section {* Formal Model of the Priority Inheritance Protocol *} |
167 |
168 |
168 text {* |
169 text {* |