Verifying Linearizability and Lock-Freedom with Temporal Logic

The development and analysis of efficient concurrent algorithms is currently an active field of research. Lock-free implementations try to better utilize the capacity of modern multi-core computers, by increasing the potential to run in parallel. This leads to a high degree of possible interference which makes the verification of these algorithms challenging. Many techniques have been proposed to prove safety and liveness properties of these implementations. Our approach is fully mechanized and based upon rely-guarantee reasoning and 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 describe how the most complex parts of the proofs can be reduced to simple steps of symbolic execution.

Download PDF