AWDIT: An Optimal Weak Database Isolation Tester
summary
AWDIT implemented in Rust tests Read Committed, Read Atomic, and Causal Consistency with proven bounds O(n^{3/2}) for RC/RA, O(n·k) for CC, runs on histories up to 2^20 transactions (~50M ops), and compares against Plume to deliver median speedups of hundreds× and 245× on the largest histories. The paper proves an n^{3/2} lower bound under the BMM hypothesis, provides artifact links, and the tool reliably finds candidate violations and pinpoints offending transactions.
AI-written summary · about
chapters (13)
- 0:00AWDIT and weak isolation
- 1:05Why weak isolation matters
- 2:31Database histories and isolation
- 4:34Efficient isolation testing
- 5:59AWDIT’s optimality and complexity
- 7:47Graph formalization of isolation
- 10:15AWDIT’s performance
- 11:38Experimental results and speed
- 12:42Conclusion and future work
- 13:25Q&A: Test suites for bugs
- 14:08Q&A: Rollbacks and concurrency
- 14:49Q&A: Finding violations
- 16:37Q&A: Declarative queries
related talks
17mJust-Right Consistency
14mMonkeyDB: Effectively Testing Correctness under Weak Isolation Levels
42mA Race To The Bottom: Database Transactions Undermining Your AppSec
44mAntidoteDB: highly available, transactional database
15mTesting Consensus Implementations using Communication Closure
52mTransactions: Myths, Surprises and Opportunities
16mDynamic Partial Order Reduction for Checking Correctness Against Transaction Isolation(…)
06mLightning talk: Testing Distributed Databases