How to Prove Algorithms Linearisable

摘要

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.