On abstraction and compositionality for weak-memory linearisability
Abstract elided by the publisher.
Related papers
- Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model OOPSLA 2018
- On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models POPL 2019
- Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it POPL 2015
- Proving correctness of highly-concurrent linearisable objects PPoPP 2006
- Specifying and Verifying Persistent Libraries ESOP 2024
- How to Prove Algorithms Linearisable CAV 2012
- Specifying and Verifying RDMA Synchronisation ESOP 2026
- Quarantining Weakness - Compositional Reasoning under Relaxed Memory Models (Extended Abstract) ESOP 2013