153   behaviour for $L$ is to switch to the highest remaining priority of

   153   behaviour for $L$ is to switch to the highest remaining priority of

   154   the threads that it blocks. A similar error is made in the textbook

   154   the threads that it blocks. A similar error is made in the textbook

   155   \cite[Section 2.3.1]{book} which specifies for a process that 

   155   \cite[Section 2.3.1]{book} which specifies for a process that 

   156   inherited a higher priority and exits a critical section ``it resumes 

   156   inherited a higher priority and exits a critical section ``it resumes 

   157   the priority it had at the point of entry into the critical section''.

   157   the priority it had at the point of entry into the critical section''.

   159   While \cite{book} and

   159   While \cite{book} and

   160   \cite{Sha90} are the only formal publications we have 

   160   \cite{Sha90} are the only formal publications we have 

   161   found that describe the incorrect behaviour, not all, but many

   161   found that describe the incorrect behaviour, not all, but many

   162   informal\footnote{informal as in ``found on the Web''} 

   162   informal\footnote{informal as in ``found on the Web''} 

   163   descriptions of PIP overlook the possibility that another

   163   descriptions of PIP overlook the possibility that another

  1465   is a magnitude harder than the one we presented here, but still

  1465   is a magnitude harder than the one we presented here, but still

  1466   within reach of current theorem proving technology. We leave this

  1466   within reach of current theorem proving technology. We leave this

  1467   for future work.

  1467   for future work.

  1468 

  1468 

  1469   To us, it seems sound reasoning about scheduling algorithms is fiendishly difficult

  1469   To us, it seems sound reasoning about scheduling algorithms is fiendishly difficult

  1473   Threshold Scheduling \cite{ThreadX}. The use of a theorem prover was

  1473   Threshold Scheduling \cite{ThreadX}. The use of a theorem prover was

  1474   invaluable to us in order to be confident about the correctness of our reasoning 

  1474   invaluable to us in order to be confident about the correctness of our reasoning 

  1475   (no case can be overlooked).   

  1475   (no case can be overlooked).   

  1476   The most closely related work to ours is the formal verification in

  1476   The most closely related work to ours is the formal verification in

  1477   PVS of the Priority Ceiling Protocol done by Dutertre

  1477   PVS of the Priority Ceiling Protocol done by Dutertre

  1492   is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary

  1492   is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary

  1493   definitions and proofs span over 770 lines of code. The properties relevant

  1493   definitions and proofs span over 770 lines of code. The properties relevant

  1494   for an implementation require 2000 lines. 

  1494   for an implementation require 2000 lines. 

  1495   The code of our formalisation 

  1495   The code of our formalisation 

  1496   can be downloaded from the Mercurial repository at

  1496   can be downloaded from the Mercurial repository at

  1498 

  1498 

  1499   %\medskip

  1499   %\medskip

  1500 

  1500 

  1501   %\noindent

  1501   %\noindent

  1502   %{\bf Acknowledgements:}

  1502   %{\bf Acknowledgements:}