How to Prove Algorithms Linearisable
Abstract elided by the publisher.
Related papers
- Proving correctness of highly-concurrent linearisable objects PPoPP 2006
- On abstraction and compositionality for weak-memory linearisability VMCAI 2018
- Fast concurrent data sketches PPoPP 2020
- Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model OOPSLA 2018
- Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it POPL 2015
- APTE: An Algorithm for Proving Trace Equivalence TACAS 2014
- Proving the Correctness of the Implementation of a Control-Command Algorithm SAS 2009
- Verifying the SRT Division Algorithm Using Theorem Proving Techniques CAV 1996