Journal/Paper.thy
changeset 24 6f50e6a8c6e0
parent 23 24e6884d9258
child 25 a9c0eeb00cc3
equal deleted inserted replaced
23:24e6884d9258 24:6f50e6a8c6e0
    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 
    31 
    31  
    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 
  1468   (no case can be overlooked).  
  1468   (no case can be overlooked).   
  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