66 has never been formally verified in a theorem prover. As already |
66 has never been formally verified in a theorem prover. As already |
67 pointed out in the literature, the original informal investigation of |
67 pointed out in the literature, the original informal investigation of |
68 the Property Inheritance Protocol presents a correctness ``proof'' for |
68 the Property Inheritance Protocol presents a correctness ``proof'' for |
69 an \emph{incorrect} algorithm. In this paper we fix the problem of |
69 an \emph{incorrect} algorithm. In this paper we fix the problem of |
70 this proof by making all notions precise and implementing a variant of |
70 this proof by making all notions precise and implementing a variant of |
71 a solution proposed earlier. Our formalisation in Isabelle/HOL |
71 a solution proposed earlier. We also generalise the result to the |
|
72 practically relevant case where critical sections can |
|
73 overlap. Our formalisation in Isabelle/HOL not just |
72 uncovers facts not mentioned in the literature, but also shows how to |
74 uncovers facts not mentioned in the literature, but also shows how to |
73 efficiently implement this protocol. Earlier correct implementations |
75 efficiently implement this protocol. Earlier correct implementations |
74 were criticised as too inefficient. Our formalisation is based on |
76 were criticised as too inefficient. Our formalisation is based on |
75 Paulson's inductive approach to verifying protocols; our implementation |
77 Paulson's inductive approach to verifying protocols; our implementation |
76 is on top of the small PINTOS operating system.\medskip |
78 builds on top of the small PINTOS operating system.\medskip |
77 |
79 |
78 %{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, |
80 %{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, |
79 %real-time systems, Isabelle/HOL |
81 %real-time systems, Isabelle/HOL |
80 \end{abstract} |
82 \end{abstract} |
81 |
83 |