1442 the proof of Sha et al.: they require that critical sections nest properly, |
1442 the proof of Sha et al.: they require that critical sections nest properly, |
1443 whereas our scheduler allows critical sections to overlap. |
1443 whereas our scheduler allows critical sections to overlap. |
1444 |
1444 |
1445 PIP is a scheduling algorithm for single-processor systems. We are |
1445 PIP is a scheduling algorithm for single-processor systems. We are |
1446 now living in a multi-processor world. Priority Inversion certainly |
1446 now living in a multi-processor world. Priority Inversion certainly |
1447 occurs also there. However, there is very little ``foundational'' |
1447 occurs also there, see for example \cite{Brandenburg11, Davis11} |
|
1448 However, there is very little ``foundational'' |
1448 work about PIP-algorithms on multi-processor systems. We are not |
1449 work about PIP-algorithms on multi-processor systems. We are not |
1449 aware of any correctness proofs, not even informal ones. There is an |
1450 aware of any correctness proofs, not even informal ones. There is an |
1450 implementation of a PIP-algorithm for multi-processors as part of the |
1451 implementation of a PIP-algorithm for multi-processors as part of the |
1451 ``real-time'' effort in Linux, including an informal description of the implemented scheduling |
1452 ``real-time'' effort in Linux, including an informal description of the implemented scheduling |
1452 algorithm given in \cite{LINUX}. We estimate that the formal |
1453 algorithm given in \cite{LINUX}. We estimate that the formal |
1476 for an implementation require 2000 lines. |
1477 for an implementation require 2000 lines. |
1477 %The code of our formalisation |
1478 %The code of our formalisation |
1478 %can be downloaded from |
1479 %can be downloaded from |
1479 %\url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}. |
1480 %\url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}. |
1480 |
1481 |
1481 \medskip |
1482 %\medskip |
1482 |
1483 |
1483 \noindent |
1484 %\noindent |
1484 {\bf Acknowledgements:} |
1485 %{\bf Acknowledgements:} |
1485 We are grateful for the comments we received from anonymous |
1486 %We are grateful for the comments we received from anonymous |
1486 referees. |
1487 %referees. |
1487 |
1488 |
1488 \bibliographystyle{plain} |
1489 \bibliographystyle{plain} |
1489 \bibliography{root} |
1490 \bibliography{root} |
1490 *} |
1491 *} |
1491 |
1492 |