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. ({\bf Is this True?}) |
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 |
373 we have a deadlock. Therefore when a thread requests a resource, |
373 we have a deadlock. Therefore when a thread requests a resource, |
374 we must ensure that the resulting RAG is not circular. In practice, the |
374 we must ensure that the resulting RAG is not circular. In practice, the |
375 programmer has to ensure this. |
375 programmer has to ensure this. |
376 |
376 |
377 |
377 |
378 {\bf define detached} |
378 {\bf ??? define detached} |
379 |
379 |
380 |
380 |
381 Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a |
381 Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a |
382 state @{text s}. It is defined as |
382 state @{text s}. It is defined as |
383 |
383 |
1245 of PIP. Earlier model checking approaches which verified particular implementations |
1245 of PIP. Earlier model checking approaches which verified particular implementations |
1246 of PIP \cite{Faria08,Jahier09,Wellings07} cannot |
1246 of PIP \cite{Faria08,Jahier09,Wellings07} cannot |
1247 provide this kind of ``deep understanding'' about the principles behind |
1247 provide this kind of ``deep understanding'' about the principles behind |
1248 PIP and its correctness. |
1248 PIP and its correctness. |
1249 |
1249 |
1250 {\bf rewrite the following slightly} |
1250 {\bf ??? rewrite the following slightly} |
1251 |
1251 |
1252 PIP is a scheduling algorithm for single-processor systems. We are |
1252 PIP is a scheduling algorithm for single-processor systems. We are |
1253 now living in a multi-processor world. So the question naturally |
1253 now living in a multi-processor world. So the question naturally |
1254 arises whether PIP has any relevance in such a world beyond |
1254 arises whether PIP has any relevance in such a world beyond |
1255 teaching. Priority Inversion certainly occurs also in |
1255 teaching. Priority Inversion certainly occurs also in |
1273 |
1273 |
1274 The most closely related work to ours is the formal verification in |
1274 The most closely related work to ours is the formal verification in |
1275 PVS of the Priority Ceiling Protocol done by Dutertre |
1275 PVS of the Priority Ceiling Protocol done by Dutertre |
1276 \cite{dutertre99b}---another solution to the Priority Inversion |
1276 \cite{dutertre99b}---another solution to the Priority Inversion |
1277 problem, which however needs static analysis of programs in order to |
1277 problem, which however needs static analysis of programs in order to |
1278 avoid it. {\bf mention model-checking approaches} |
1278 avoid it. {\bf ??? mention model-checking approaches} |
1279 |
1279 |
1280 Our formalisation |
1280 Our formalisation |
1281 consists of around 210 lemmas and overall 6950 lines of readable Isabelle/Isar |
1281 consists of around 210 lemmas and overall 6950 lines of readable Isabelle/Isar |
1282 code with a few apply-scripts interspersed. The formal model of PIP |
1282 code with a few apply-scripts interspersed. The formal model of PIP |
1283 is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary |
1283 is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary |
1284 definitions and proofs span over 770 lines of code. The properties relevant |
1284 definitions and proofs span over 770 lines of code. The properties relevant |
1285 for an implementation require 2000 lines. The code of our formalisation |
1285 for an implementation require 2000 lines. The code of our formalisation |
1286 can be downloaded from |
1286 can be downloaded from |
1287 \url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}. |
1287 \url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}. |
1288 |
1288 |
1289 {\bf say: |
1289 {\bf ??? say: |
1290 So this paper is a good witness for one |
1290 So this paper is a good witness for one |
1291 of the major reasons to be interested in machine checked reasoning: |
1291 of the major reasons to be interested in machine checked reasoning: |
1292 gaining deeper understanding of the subject matter. |
1292 gaining deeper understanding of the subject matter. |
1293 } |
1293 } |
1294 |
1294 |