Checking Observational Correctness of Database Systems
summary
Tool encodes transaction behavior with a version-aware semantics and checks isolation via explicit SMT constraints so the checker asks whether any valid execution could produce the client log. A partially symbolic encoding keeps most values concrete to shrink formulas (naive BMC took ~40 minutes versus under 2 seconds for core cases). The implementation Troubadour supports a MySQL fragment, verifies PostgreSQL and an industrial system, scales to ~1M banking transactions in <2 hours and found two new bugs.
AI-written summary · about
chapters (10)
- 0:00DBMS correctness problem
- 1:03Observational correctness definition
- 2:06Correctness across isolation levels
- 3:50Version-aware transaction semantics
- 6:36Isolation level constraints
- 8:04Symbolic execution with SMT
- 9:10Partially symbolic semantics
- 10:58Experimental results and tool
- 12:01Future directions and challenges
- 12:45Q&A
related talks
11mDetecting Transactional Bugs in Database Engines via Graph-Based Oracle Construction
41mTransactions: myths, surprises and opportunities
14mDetecting Logic Bugs in Database Engines via Equivalent Expression Transformation
14mMonkeyDB: Effectively Testing Correctness under Weak Isolation Levels
18mValScope: Value-Semantics-Aware Metamorphic Testing for Detecting Logical Bugs in DBMSs
21mIsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly(…)
36mSQLancer: Automatically Finding Bugs in Database Management Systems
42mA Race To The Bottom: Database Transactions Undermining Your AppSec