Mechanizing a correctness proof for a lock-free concurrent stack

Abstract

Distributed algorithms are inherently complex to verify. In this paper we show how to verify that a concurrent lock-free implementation of a stack is correct by mechanizing the proof that it is linearizable, linearizability being a correctness notion for concurrent objects. Our approach consists of two parts: the first part is independent of the example and derives proof obligations local for one process which imply linearizabilty. The conditions establish a (special sort of non-atomic) refinement relationship between the specification and the concurrent implementation. These are used in the second part to verify the lock-free stack implementation. We use the specification language Z to describe the algorithms and the KIV theorem prover to mechanize the proof. © 2008 Springer-Verlag Berlin Heidelberg.