Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-31424-7_21 | CAV |
Keywords | Field | DocType |
complete mechanisation,proof obligation,manual proof,proof technique,queue algorithm,concurrent data structure,linearisability proof,complete proof technique,landmark paper,algorithms linearisable,completeness result | Separation logic,Computer science,Queue,Correctness,Algorithm,Soundness,Concurrent data structure,Landmark,Gas meter prover,Completeness (statistics) | Conference |
Citations | PageRank | References |
23 | 0.81 | 24 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gerhard Schellhorn | 1 | 769 | 56.43 |
| Heike Wehrheim | 2 | 1013 | 104.85 |
| John Derrick | 3 | 26 | 1.20 |