1128 |
1128 |
1129 text {* |
1129 text {* |
1130 The Priority Inheritance Protocol (PIP) is a classic textbook |
1130 The Priority Inheritance Protocol (PIP) is a classic textbook |
1131 algorithm used in real-time operating systems in order to avoid the problem of |
1131 algorithm used in real-time operating systems in order to avoid the problem of |
1132 Priority Inversion. Although classic and widely used, PIP does have |
1132 Priority Inversion. Although classic and widely used, PIP does have |
1133 its faults: for example it does not prevent deadlocks where threads |
1133 its faults: for example it does not prevent deadlocks in cases where threads |
1134 have circular lock dependencies. |
1134 have circular lock dependencies. |
1135 |
1135 |
1136 We had two aims in mind with our formalisation of PIP: One is to |
1136 We had two goals in mind with our formalisation of PIP: One is to |
1137 make the notions in the correctness proof by Sha et al.~\cite{Sha90} |
1137 make the notions in the correctness proof by Sha et al.~\cite{Sha90} |
1138 precise so that they can be processed by a theorem prover, because a |
1138 precise so that they can be processed by a theorem prover. The reason is |
1139 mechanically checked proof avoids the flaws that crept into their |
1139 that a mechanically checked proof avoids the flaws that crept into their |
1140 informal reasoning. We achieved this aim: The correctness of PIP now |
1140 informal reasoning. We achieved this goal: The correctness of PIP now |
1141 only hinges on the assumptions behind our formal model. The reasoning, which is |
1141 only hinges on the assumptions behind our formal model. The reasoning, which is |
1142 sometimes quite intricate and tedious, has been checked beyond any |
1142 sometimes quite intricate and tedious, has been checked beyond any |
1143 reasonable doubt by Isabelle/HOL. We can also confirm that Paulson's |
1143 reasonable doubt by Isabelle/HOL. We can also confirm that Paulson's |
1144 inductive method to protocol verification~\cite{Paulson98} is quite |
1144 inductive method to protocol verification~\cite{Paulson98} is quite |
1145 suitable for our formal model and proof. The traditional application |
1145 suitable for our formal model and proof. The traditional application |
1146 area of this method is security protocols. The only other |
1146 area of this method is security protocols. The only other |
1147 application of Paulson's method we know of outside this area is |
1147 application of Paulson's method we know of outside this area is |
1148 \cite{Wang09}. |
1148 \cite{Wang09}. |
1149 |
1149 |
1150 The second aim is to provide a specification for actually |
1150 The second goal of our formalisation is to provide a specification for actually |
1151 implementing PIP. Textbooks, like \cite[Section 5.6.5]{Vahalia96}, |
1151 implementing PIP. Textbooks, for example \cite[Section 5.6.5]{Vahalia96}, |
1152 explain how to use various implementations of PIP and abstractly |
1152 explain how to use various implementations of PIP and abstractly |
1153 discuss its properties, but surprisingly lack most details for a |
1153 discuss their properties, but surprisingly lack most details for a |
1154 programmer. That this is an issue in practice is illustrated by the |
1154 programmer who wants to implement PIP. That this is an issue in practice is illustrated by the |
1155 email from Baker we cited in the Introduction. We achieved also this |
1155 email from Baker we cited in the Introduction. We achieved also this |
1156 aim: The formalisation gives the first author enough data to enable |
1156 goal: The formalisation gives the first author enough data to enable |
1157 his undergraduate students to implement as part of their OS course |
1157 his undergraduate students to implement PIP (as part of their OS course) |
1158 PIP on top of PINTOS, a small operating system for teaching |
1158 on top of PINTOS, a small operating system for teaching |
1159 purposes. A byproduct of our formalisation effort is that nearly all |
1159 purposes. A byproduct of our formalisation effort is that nearly all |
1160 design choices for the PIP scheduler are backed up with a proved |
1160 design choices for the PIP scheduler are backed up with a proved |
1161 lemma. We were also able to prove the property that the choice of |
1161 lemma. We were also able to establish the property that the choice of |
1162 the next thread taking over a lock is irrelevant for the correctness |
1162 the next thread which takes over a lock is irrelevant for the correctness |
1163 of PIP. Earlier model checking approaches to verifying the |
1163 of PIP. Earlier model checking approaches which verified implementations |
1164 correctness of PIP \cite{Faria08,Jahier09,Wellings07} were not able |
1164 of PIP \cite{Faria08,Jahier09,Wellings07} cannot |
1165 to provide this kind of ``deep understanding'' about PIP. |
1165 provide this kind of ``deep understanding'' about the principles behind |
|
1166 PIP and its correctness. |
1166 |
1167 |
1167 PIP is a scheduling algorithm for single-processor systems. We are |
1168 PIP is a scheduling algorithm for single-processor systems. We are |
1168 now living in a multi-processor world. So the question naturally |
1169 now living in a multi-processor world. So the question naturally |
1169 arises whether PIP has any relevance nowadays beyond |
1170 arises whether PIP has any relevance nowadays beyond |
1170 teaching. Priority inversion certainly occurs also in |
1171 teaching. Priority inversion certainly occurs also in |