26   cp ("cprec") and

    26   cp ("cprec") and

    27   holdents ("resources") and

    27   holdents ("resources") and

    28   original_priority ("priority") and

    28   original_priority ("priority") and

    29   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")

    29   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")

    30 

    30 

    32 (*>*)

    32 (*>*)

    33 

    33 

    34 section {* Introduction *}

    34 section {* Introduction *}

    35 

    35 

    36 text {*

    36 text {*

  1463   if done informally by ``pencil-and-paper''. This is proved by the flawed proof

  1463   if done informally by ``pencil-and-paper''. This is proved by the flawed proof

  1464   in the paper by Sha et al.~\cite{Sha90} and also by Regehr \cite{Regehr} who 

  1464   in the paper by Sha et al.~\cite{Sha90} and also by Regehr \cite{Regehr} who 

  1465   pointed out an error in a paper about Preemption 

  1465   pointed out an error in a paper about Preemption 

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

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

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

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

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

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

  1470   PVS of the Priority Ceiling Protocol done by Dutertre

  1470   PVS of the Priority Ceiling Protocol done by Dutertre

  1471   \cite{dutertre99b}---another solution to the Priority Inversion

  1471   \cite{dutertre99b}---another solution to the Priority Inversion

  1472   problem, which however needs static analysis of programs in order to

  1472   problem, which however needs static analysis of programs in order to

  1473   avoid it. There have been earlier formal investigations

  1473   avoid it. There have been earlier formal investigations