Optimal Stateless Model Checking under the Release-Acquire Semantics
summary
Claims a provably optimal stateless model checking method for the Release-Acquire fragment of C/C++11 that explores each program order and read‑from relation exactly once and avoids exploring coherence orders, cutting redundancy (examples show reductions like four traces down to three). Implements the method in the tool Tracer, runs on litmus-style suites (≈1000 tests) and standard benchmarks, and reports fewer executed traces and faster runtimes than comparable RA-capable tools (CMC and others).
AI-written summary · about
chapters (8)
- 0:00Introduction
- 0:34Outline
- 1:22Concurrent Programs
- 5:45Safety Properties
- 8:03ReleaseAcquire semantics
- 11:46Super Optimal Stateless Algorithm
- 16:15Experimental Results
- 19:42Conclusion
related talks
15mOptimal Reads-From Consistency Checking for C11-Style Memory Models
17mRELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
21mModel Checking C/C++ with Mixed-Size Accesses
14mSecRSL: Security Separation Logic for C11 Release-Acquire Concurrency
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
15mThread-modular Analysis of Release-Acquire Concurrency
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency
23mVerifying Observational Robustness Against a C11-style Memory Model