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

  1285   now living in a multi-processor world. Priority Inversion certainly

  1286   arises whether PIP has any relevance in such a world beyond

  1286   occurs also there.  However, there is very little ``foundational''

  1287   teaching. Priority Inversion certainly occurs also in

  1287   work about PIP-algorithms on multi-processor systems.  We are not

  1288   multi-processor systems.  However, the answer is that

  1288   aware of any correctness proofs, not even informal ones. There is an

  1289   there is very little work about PIP and multi-processors in the literature. 

  1289   implementation of a PIP-algorithm for multi-processors as part of the

  1290   We are not aware of any proofs in this area, not even informal ones. There

  1290   ``real-time'' effort in Linux, including an informal description of the implemented scheduling

  1291   is an implementation of PIP on multi-processors in Linux as part of the ``real-time'' effort,

  1291   algorithm given in \cite{LINUX}.  We estimate that the formal

  1292   with an informal description given in \cite{LINUX}.

  1292   verification of this algorithm, involving more fine-grained events,

  1293   We estimate that the formal verification of this algorithm, involving more

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

  1294   fine-grained events, is a magnitude harder than the one we presented here, but 

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

  1295   still within reach of current theorem proving technology. We leave this for future 

  1295   for future work.

  1296   work.