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 interference 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 mechanizes 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. © 2010 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Tofan, B., Bäumler, S., Schellhorn, G., & Reif, W. (2010). Temporal logic verification of lock-freedom. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6120 LNCS, pp. 377–396). https://doi.org/10.1007/978-3-642-13321-3_21
Mendeley helps you to discover research relevant for your work.