Dynamic Robustness Verification against Weak Memory
summary
Algorithm verifies robustness against C11/C++20 weak memory using location clocks and runs as the RSAN/Arson tool that reports full backtraces for violations. It claims sound and complete detection of nonrobustness witnesses, uses memory linear in the number of threads and atomic locations, and supports release, acquire, relaxed, RMW and fences. Evaluation on a 12,000 line Microsoft allocator with 600 atomic locations finds 20 robustness violations that are fixed with fewer fences than naively promoting all atomics, showing the technique scales and preserves performance.
AI-written summary · about
chapters (14)
- 0:00Introduction to dynamic verification
- 1:04Weak memory models in C++
- 2:28Store buffer example and races
- 3:30Limitations of existing race detectors
- 4:12Dynamic robustness verification concept
- 5:40Nonrobustness witness definition
- 7:08Example execution and divergence
- 8:13Location clocks for tracking
- 10:44Instrumentation with location clocks
- 12:59Predicting nonrobustness witnesses
- 14:04Implementation and supported features
- 14:45Comparison with static verification
- 15:47Case study on Microsoft allocator
- 16:31Conclusion and future work
related talks
23mVerifying Observational Robustness Against a C11-style Memory Model
21mAutomated Robustness Verification of Concurrent Data Structure Libraries Against(…)
21mWeak Memory Demands Model-based Compiler Testing
21mChasing Unicorns and Not Losing Hope in Validating Weak Memory Persistency Model...
15mOptimal Reads-From Consistency Checking for C11-Style Memory Models
16mModel Checking for a Multi-Execution Memory Model
01h 11mProgramming language memory models: Problems, solutions, and directions
20mHow Hard is Weak-Memory Testing?