Making TransactionIsolation Checking Practical
Jian Zhang, Shuai Mu, Cheng Tan

TL;DR
Boomslang is a versatile framework that makes transaction isolation checking practical for modern databases by supporting arbitrary operations, requiring no internal knowledge, and enabling customization.
Contribution
It introduces a modular, extensible checking framework that handles previously uncheckable configurations and supports a wide range of isolation levels without database internals.
Findings
Reimplemented three prior checkers with comparable or better performance.
Identified a new bug in TiDB.
Audited metadata in JuiceFS and checked behavior in MariaDB.
Abstract
Checking whether database transactions adhere to isolation levels is a crucial yet challenging problem. We present Boomslang, the first general-purpose checking framework capable of verifying configurations that were previously uncheckable. Boomslang advances beyond prior work in three key aspects: (1) it supports arbitrary operation types provided by modern transactional key-value stores, (2) it requires no knowledge of database internals, and (3) it offers a modular, extensible pipeline amenable to customization and optimizations. Boomslang adopts a front-/back-end separation. As the front-end, it parses a database trace into an Abstract Semantic Graph, which is then lowered -- via semantic analysis -- into a low-level intermediate representation (IR). The back-end converts this IR to a set of constraints for SMT solving. This design is enabled by a key abstraction in the IR, called…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
