Dynamic Partial Order Reduction for Checking Correctness Against Transaction Isolation(…)
summary
First DPOR-based stateless model checking algorithm for transactional apps that is sound, complete and optimal and runs in polynomial memory. It is parametric over isolation levels (supports Read Committed, Causal Consistency, Snapshot Isolation and Serializability), proves which levels allow strong optimality, and shows impossibility results for the others. Implementation on Java Pathfinder is available with artifacts; experiments on literature benchmarks beat naive DFS in time and memory while producing concrete counterexample traces for violated safety properties.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:21Transaction isolation problem
- 3:37State explosion in verification
- 5:43Dynamic partial order reduction
- 7:08Algorithm: schedule and swap
- 10:21Swap protocols and optimality
- 11:23C-extensible isolation levels
- 12:04Evaluation and tool
- 13:31Conclusion
- 13:52Q&A
related talks
21mIsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly(…)
47mDeploying DP: Experiences from the Front Lines and Open Challenges
20mSPORE: Combining Symmetry and Partial Order Reduction
27mReasoning about Weak Isolation Levels in Separation Logic
14mChecking Observational Correctness of Database Systems
41mTransactions: myths, surprises and opportunities
22mCompositional Programming and Testing of Dynamic Distributed Systems
15mMuch ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent D