Chasing Unicorns and Not Losing Hope in Validating Weak Memory Persistency Model...
summary
A practical method to validate NVM persistency on real machines: hardware bus interception with a SoCal DDR detective fails on x86 because the persistent domain sits in the memory controller’s write pending queue (WPQ), but succeeds on Arm (results accepted at ICSC). The alternative is a timestamp-based memory-hierarchy timing attack that distinguishes cache vs NVM access and—combined with active model learning—automatically refines a hypothesis model via Oracle queries. Early experiments show distinguishable but noisy patterns (roughly three timing clusters); Intel consultation suggests viability but implementation is still exploratory.
AI-written summary · about
chapters (9)
- 0:00Validating weak memory persistency
- 1:24Why persistency matters
- 3:57Memory bus intercept limits
- 6:29Echolocation timing attack
- 9:00Active model learning
- 12:33Discrepancy analysis refining
- 13:42Machine learning for persistency
- 17:19Concurrent clean algebra formalism
- 19:16Cache and persistency measurement
related talks
01h 11mProgramming language memory models: Problems, solutions, and directions
40mA practical approach to Java Memory Model
20mHow Hard is Weak-Memory Testing?
16mModel Checking for a Multi-Execution Memory Model
17mDynamic Robustness Verification against Weak Memory
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
13mThe Semantics of Shared Memory in Intel CPU/FPGA Systems
23mMemory Consistency Model Status Update