Inferring Likely Counting-related Atomicity Program Properties for Persistent...
summary
Method infers counting-related atomicity properties for persistent memory by encoding an access-range invariance between container indices and size counters, extracting symbolic index ranges via symbolic range analysis, and validating candidates with SMT constraints. Implementation generates candidate variable groups from symbolic indices, checks the invariant, and emits likely atomicity properties. Evaluation runs on four real PM data structures, finds 14 atomicity bugs (11 new), and completes each analysis in under one second.
AI-written summary · about
chapters (6)
- 0:00Persistent memory challenges
- 2:07PM testing tools limitations
- 4:11Counting in persistent data
- 8:55Counting atomicity properties
- 15:05Bug detection results
- 16:33Summary
related talks
20mAtomiS: Data-Centric Synchronization Made Practical
01h 22mBeyond Sequential Consistency - Leveraging Atomics for Fun & Profit
16mPersistent Owicki-Gries Reasoning: A Program Logic for Reasoning about Persistent Programs on Intel-
15mSoundness of Predictive Concurrency Analyses
01h 28mAtomic’s memory orders, what for?
39mRust Atomics in the Wild: Memory Ordering Design Patterns [...]
17mJust-Right Consistency
23mPersistence Semantics for Weak Memory