Verifying Observational Robustness Against a C11-style Memory Model
summary
Proves robustness against the C11-style model is decidable (PSPACE-complete) by a concrete reduction to SC reachability, implements that instrumentation in the Rocker tool and runs it on concurrent algorithms. Introduces a weaker, checkable property called observational robustness to handle speculative relaxed reads (seqlock example), gives a sound (but not complete) checking procedure, and reports a practical finding: a common C11 Peterson implementation is buggy and requires two specific fixes.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:10Sequential Consistency
- 1:56Main Contributions
- 2:53Previous Work
- 6:35Fence Release
- 7:05Load Buffers
- 8:04Robustness
- 12:19Second Contribution
- 13:46Example
- 19:13Weak Robustness
related talks
17mDynamic Robustness Verification against Weak Memory
21mAutomated Robustness Verification of Concurrent Data Structure Libraries Against(…)
15mOptimal Reads-From Consistency Checking for C11-Style Memory Models
14mMaking Weak Memory Models Fair
01h 11mProgramming language memory models: Problems, solutions, and directions
19mVerifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic
20mHow Hard is Weak-Memory Testing?
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic