Checking Robustness to Weak Persistency Models
summary
PSign dynamically checks whether a program running under the x86 weak persistency model behaves as if it ran under strict persistency by constructing per-thread potential crash intervals that constrain where an equivalent strict run could have crashed. It instruments LLVM code, controls scheduling, simulates crashes with the Geru-based checker, and reports 48 robustness violations (17 previously unknown), localizes the missing flush/fence points, and suggests minimal flush intervals validated on FastFair, VPlusTree, PMDK, Redis and Memcached.
AI-written summary · about
chapters (7)
- 0:00Start
- 0:14Persistent Memory
- 2:43Key Observation
- 6:01PSan Key Idea
- 7:44Supporting Multi-threaded Programs
- 12:28Evaluation
- 14:08Conclusion
related talks
17mDynamic Robustness Verification against Weak Memory
21mChasing Unicorns and Not Losing Hope in Validating Weak Memory Persistency Model...
23mVerifying Observational Robustness Against a C11-style Memory Model
01h 11mProgramming language memory models: Problems, solutions, and directions
23mPersistence Semantics for Weak Memory
21mWeak Memory Demands Model-based Compiler Testing
20mHow Hard is Weak-Memory Testing?
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++