equal
deleted
inserted
replaced
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. We also generalise the proof to the |
71 a solution proposed earlier. We also generalise the original informal proof to the |
72 practically relevant case where critical sections can |
72 practically relevant case where critical sections can |
73 overlap. Our formalisation in Isabelle/HOL not just |
73 overlap. Our formalisation in Isabelle/HOL not just |
74 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 |
75 efficiently implement this protocol. Earlier correct implementations |
75 efficiently implement this protocol. Earlier correct implementations |
76 were criticised as too inefficient. Our formalisation is based on |
76 were criticised as too inefficient. Our formalisation is based on |