Observation-Based Concurrent Program Logic for Relaxed Memory Consistency Models
Abstract elided by the publisher.
Related papers
- Verifying observational robustness against a c11-style memory model POPL 2021
- Library abstraction for C/C++ concurrency POPL 2013
- Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic PLDI 2025
- CheckFence: checking consistency of concurrent data types on relaxed memory models PLDI 2007
- Verifying Visibility-Based Weak Consistency ESOP 2020
- The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency POPL 2022
- An Axiomatic Basis for Computer Programming on Relaxed Hardware Architectures: The AxSL Logics TOPLAS 2026
- Assertional reasoning about data races in relaxed memory models PPoPP 2008