Temporal Logic Verification of Lock-Freedom

B. Tofan, S. Bäumler, G. Schellhorn, and W. Reif

Temporal Logic Verification of Lock-Freedom

Lock-free implementations of data structures try to better utilize the capacity of modern multi-core computers, by increasing the potential to run in parallel. The resulting high degree of possible interfer- ence makes verification of these algorithms challenging. In this paper we describe a technique to verify lock-freedom, their main liveness property. The result complements our earlier work on proving linearizability, the standard safety property of lock-free algorithms. Our approach mecha- nizes both, the derivation of proof obligations as well as their verification for individual algorithms. It is based on an encoding of rely-guarantee reasoning using the temporal logic framework of the interactive theorem prover KIV. By means of a slightly improved version of Michael and Scott’s lock-free queue algorithm we demonstrate how the most complex parts of the proofs can be reduced to relatively simple steps of symbolic execution.

published 2010 In Proc. of Mathematics of Program Construction (MPC)

Publisher: Springer, LNCS, vol. 6120, pp. 377 - 396