Linearisability is the key correctness criterion for concurrent implementations of data structures shared by multiple processes. In this paper we present a proof of linearisability of the lazy implementation of a set due to Heller et al. The lazy set presents one of the most challenging issues in verifying linearisability: a linearisation point of an operation set by a process other than the one executing it. For this we develop a proof strategy based on refinement which uses thread local simulation conditions and the technique of potential linearisation points. The former allows us to prove linearisability for arbitrary numbers of processes by looking at only two processes at a time, the latter permits disposing with reasoning about the past. All proofs have been mechanically carried out using the interactive prover KIV. © 2011 Springer-Verlag.
CITATION STYLE
Derrick, J., Schellhorn, G., & Wehrheim, H. (2011). Verifying linearisability with potential linearisation points. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6664 LNCS, pp. 323–337). https://doi.org/10.1007/978-3-642-21437-0_25
Mendeley helps you to discover research relevant for your work.