Verifying Local Transformations on Relaxed Memory Models
Abstract elided by the publisher.
Related papers
- Compositional Verification of Compiler Optimisations on Relaxed Memory ESOP 2018
- Promising 2.0: global optimizations in relaxed memory concurrency PLDI 2020
- A Proof Recipe for Linearizability in Relaxed Memory Separation Logic PLDI 2024
- Relaxed-memory concurrency and verified compilation POPL 2011
- Partial-coherence abstractions for relaxed memory models PLDI 2011
- Modular data-race-freedom guarantees in the promising semantics PLDI 2021
- SecRSL: security separation logic for C11 release-acquire concurrency OOPSLA 2021
- Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic PLDI 2025