How to prove algorithms linearizable

G. Schellhorn, J.Derrick, and H. Wehrheim

How to prove algorithms linearizable

Linearisability is the standard correctness criterion for concurrent data structures. In this paper, we present a sound and complete proof technique for linearisability based on backward simulations. We exemplify this technique by a linearisability proof of the queue algorithm presented in Herlihy and Wing's landmark paper. Except for the manual proof by them, none of the many other current approaches to checking linearisability has successfully treated this intricate example. Our approach is grounded on complete mechanisation: the proof obligations for the queue are verified using the interactive prover KIV, and so is the general soundness and completeness result for our proof technique.

published 2012 In Proc. of Computer Aided Verification (CAV)

Publisher: Springer, LNCS, vol 7358, pp. 243-259, 2012