equal
deleted
inserted
replaced
81 \emph{incorrect} algorithm. In this paper we fix the problem of this |
81 \emph{incorrect} algorithm. In this paper we fix the problem of this |
82 proof by making all notions precise and implementing a variant of a |
82 proof by making all notions precise and implementing a variant of a |
83 solution proposed earlier. We also generalise the scheduling problem |
83 solution proposed earlier. We also generalise the scheduling problem |
84 to the practically relevant case where critical sections can |
84 to the practically relevant case where critical sections can |
85 overlap. Our formalisation in Isabelle/HOL is based on Paulson's |
85 overlap. Our formalisation in Isabelle/HOL is based on Paulson's |
86 inductive approach to verifying protocols. The formalisation not |
86 inductive approach to protocol verification. The formalisation not |
87 only uncovers facts overlooked in the literature, but also helps |
87 only uncovers facts overlooked in the literature, but also helps |
88 with an efficient implementation of this protocol. Earlier |
88 with an efficient implementation of this protocol. Earlier |
89 implementations were criticised as too inefficient. Our |
89 implementations were criticised as too inefficient. Our |
90 implementation builds on top of the small PINTOS operating system |
90 implementation builds on top of the small PINTOS operating system |
91 used for teaching.\medskip |
91 used for teaching.\medskip |