1131   algorithm used in real-time 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.  While classic and widely used, PIP does have its faults: for

  1132   Priority Inversion.  Although classic and widely used, PIP does have

  1133   example it does not prevent deadlocks where threads have circular

  1133   its faults: for example it does not prevent deadlocks where threads

  1134   lock dependencies.

  1134   have circular lock dependencies.

  1135 

  1135 

  1136   We had two aims in mind with our formalisation

  1136   We had two aims in mind with our formalisation of PIP: One is to

  1137   of PIP: One is to understand the relevant literature and to make the

  1137   make the notions in the correctness proof by Sha et al.~\cite{Sha90}

  1138   notions in its correctness proof precise so that they can be

  1138   precise so that they can be processed by a theorem prover, because a

  1139   processed by a theorem prover, because a mechanically checked proof

  1139   mechanically checked proof avoids the flaws that crept into their

  1140   avoids the flaws that crept into the informal reasoning by Sha et

  1140   informal reasoning. We achieved this aim: The correctness of PIP now

  1141   al.~\cite{Sha90}. We achieved this aim: The correctness of PIP now

  1141   only hinges on the assumptions behind our formal model. The reasoning, which is

  1142   hinges only on the assumptions behind our formal model, which can

  1143   now be debated and potentially be modified. The reasoning, which is

  1145   reasonable doubt by Isabelle. We can confirm that Paulson's

  1143   reasonable doubt by Isabelle/HOL. We can also confirm that Paulson's

  1146   inductive approach to protocol verification \cite{Paulson98} is

  1144   inductive method to protocol verification~\cite{Paulson98} is quite

  1147   quite suitable for our formal model and proof. The traditianal

  1145   suitable for our formal model and proof. The traditional application

  1148   application area of this approach are security protocols.

  1146   area of this method is security protocols.  The only other

  1149   The only other application of Paulson's approach outside this area we know of 

  1147   application of Paulson's method we know of outside this area is

  1150   is \cite{Wang09}.

  1148   \cite{Wang09}.

  1151 

  1149 

  1152   The second aim is to provide a specification for PIP so that it can

  1150   The second aim is to provide a specification for actually

  1153   actually be implemented. Textbooks, like \cite[Section

  1151   implementing PIP. Textbooks, like \cite[Section 5.6.5]{Vahalia96},

  1154   5.6.5]{Vahalia96}, explain how to use various implementations of PIP

  1152   explain how to use various implementations of PIP and abstractly

  1155   and abstractly discuss its properties, but surprisinly lack many

  1153   discuss its properties, but surprisingly lack most details for a

  1156   details for an implementor.  That this is an issue in practice is

  1154   programmer.  That this is an issue in practice is illustrated by the

  1157   illustrated by the email from Baker we cited in the

  1155   email from Baker we cited in the Introduction. We achieved also this

  1158   Introduction. The formalisation gives the first author enough data

  1156   aim: The formalisation gives the first author enough data to enable

  1159   to enable his undergraduate students to implement PIP on top of

  1157   his undergraduate students to implement as part of their OS course

  1160   PINTOS, an small operating system for teaching purposes.  Given the

  1158   PIP on top of PINTOS, a small operating system for teaching

  1161   results in Section~\ref{implement}, we also succeeded with this

  1159   purposes. A byproduct of our formalisation effort is that nearly all

  1162   aim. A byproduct of our formalisation effort is that nearly all

  1164   lemma.

  1161   lemma. We were also able to prove the property that the choice of

  1165 

  1162   the next thread taking over a lock is irrelevant for the correctness

  1166 

  1163   of PIP. Earlier model checking techniques

  1164   \cite{Faria08,Jahier09,Wellings07} were not able to provided this

  1165   kind of ``deep understanding'' into PIP.

  1166 

  1167   PIP is a scheduling algorithm for single-processor systems. We are

  1168   now living in a multi-processor world. So the question naturally arises 

  1169   whether PIP has nowadays any relevance beyond teaching. 

  1170   

  1171    The work in this paper only deals with single CPU configurations. The

  1172   "one CPU" assumption is essential for our formalisation, because the

  1173   main lemma fails in multi-CPU configuration. The lemma says that any

  1174   runing thead must be the one with the highest prioirty or already held

  1175   some resource when the highest priority thread was initiated. When

  1176   there are multiple CPUs, it may well be the case that a threads did

  1177   not hold any resource when the highest priority thread was initiated,

  1178   but that thread still runs after that moment on a separate CPU. In

  1179   this way, the main lemma does not hold anymore.

  1180 

  1181 

  1182   There are some works deals with priority inversion in multi-CPU

  1183   configurations[???], but none of them have given a formal correctness

  1184   proof. The extension of our formal proof to deal with multi-CPU

  1185   configurations is not obvious. One possibility, as suggested in paper

  1186   [???], is change our formal model (the defiintion of "schs") to give

  1187   the released resource to the thread with the highest prioirty. In this

  1188   way, indefinite prioirty inversion can be avoided, but for a quite

  1189   different reason from the one formalized in this paper (because the

  1190   "mail lemma" will be different). This means a formal correctness proof

  1191   for milt-CPU configuration would be quite different from the one given

  1192   in this paper. The solution of prioirty inversion problem in mult-CPU

  1193   configurations is a different problem which needs different solutions

  1194   which is outside the scope of this paper.

  1195 

  1196   no clue about multi-processor case according to \cite{Steinberg10} 

  1429   The work in this paper only deals with single CPU configurations. The

  1422  

  1430   "one CPU" assumption is essential for our formalisation, because the

  1431   main lemma fails in multi-CPU configuration. The lemma says that any

  1432   runing thead must be the one with the highest prioirty or already held

  1433   some resource when the highest priority thread was initiated. When

  1434   there are multiple CPUs, it may well be the case that a threads did

  1435   not hold any resource when the highest priority thread was initiated,

  1436   but that thread still runs after that moment on a separate CPU. In

  1437   this way, the main lemma does not hold anymore.

  1438 

  1439 

  1440   There are some works deals with priority inversion in multi-CPU

  1441   configurations[???], but none of them have given a formal correctness

  1442   proof. The extension of our formal proof to deal with multi-CPU

  1443   configurations is not obvious. One possibility, as suggested in paper

  1444   [???], is change our formal model (the defiintion of "schs") to give

  1445   the released resource to the thread with the highest prioirty. In this

  1446   way, indefinite prioirty inversion can be avoided, but for a quite

  1447   different reason from the one formalized in this paper (because the

  1448   "mail lemma" will be different). This means a formal correctness proof

  1449   for milt-CPU configuration would be quite different from the one given

  1450   in this paper. The solution of prioirty inversion problem in mult-CPU

  1451   configurations is a different problem which needs different solutions

  1452   which is outside the scope of this paper.