Formal Verification of Lock-Free Algorithms

The current trend towards multi-core processors has renewed the interest in the development and correctness of concurrent algorithms. Most of these algorithms rely on locks to protect critical sections from unwanted interference. Recently a new class of nonblocking algorithms has been developed which do not rely on critical sections, but on atomic compare-and-set instructions. Such lock-free algorithms are less vulnerable to the typical problems of concurrent algorithms: deadlocks, livelocks and priority inversion. On the other hand, the lack of a uniform principle to rule out interference results in increased complexity. This makes it harder to understand these algorithms and to verify their correctness. The paper gives a simple example to demonstrate the central correctness criteria of linearizability (a safety property) and lock-freeness (a liveness property) for lock-free algorithms. It then sketches our approach to the modular verification of lock-free algorithms which uses rely-guarantee reasoning and a powerful temporal logic to derive refinement proof obligations that can be verified with the interactive theorem prover KIV. Finally an overview over related work and techniques that are relevant to automate proofs is given.