IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly(…)
summary
IsoPredict takes an observed serializable run, emits SMT constraints that encode weak isolation (causal/read‑committed), and searches for a feasible unserializable execution; it records per‑read writers in an instrumented store, replays predicted executions for validation, and uses conservative boundary constraints to avoid false positives from divergent control flow. Implementation extends the MonkeyDB store, evaluates on four benchmarks, and reports >99% feasible predicted executions while noting long constraint‑generation costs.
AI-written summary · about
chapters (11)
- 0:00IsoPredict introduction
- 4:34Unserializable behaviors detection
- 8:05IsoPredict design
- 12:10Divergence and aborts handling
- 14:00Effectiveness and performance
- 15:48Summary and future
- 16:10Q&A: SMT solver encodings
- 17:17Q&A: Performance vs isolation
- 18:41Q&A: Source vs binary analysis
- 19:24Q&A: Hooks to data libraries
- 20:05Q&A: Application invariants
related talks
14mMonkeyDB: Effectively Testing Correctness under Weak Isolation Levels
16mDynamic Partial Order Reduction for Checking Correctness Against Transaction Isolation(…)
14mChecking Observational Correctness of Database Systems
22mHow to Enforce and Verify Invariants in Weakly Consistent Databases
27mUnderstanding Distributed Systems with Deterministic Simulation
25mSafe Replication through Bounded Concurrency Verification
15mPolyjuice: High-Performance Transactions via Learned Concurrency Control
15mTesting Consensus Implementations using Communication Closure