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 superpositions, which capture the uncertainty and complexity caused by arbitrary operations and missing information. Our experiments show that with just 271--386 lines of code, the core logic of three prior checkers can be reimplemented as Boomslang modules, achieving comparable or superior performance. Using Boomslang, we also identify a new bug in TiDB, audit the metadata layer of the JuiceFS file system, check vendor-specific behavior in MariaDB, support five previously unchecked isolation levels, and confirm a theoretical result on the correctness of strict serializability.

翻译：检查数据库事务是否遵守隔离级别是一项至关重要但极具挑战性的问题。我们提出Boomslang——首个通用的检查框架，能够验证以往无法检查的配置。Boomslang在三个方面超越了先前工作：（1）支持现代事务性键值存储提供的任意操作类型，（2）无需了解数据库内部实现，（3）提供模块化、可扩展的流水线，便于定制和优化。Boomslang采用前端/后端分离架构。在前端，它将数据库追踪解析为抽象语义图，再通过语义分析降级到低级中间表示（IR）。后端将此IR转化为一组供SMT求解器求解的约束。该设计依赖于IR中的关键抽象——叠加（superpositions），它捕捉了由任意操作及信息缺失所导致的不确定性和复杂性。实验表明，仅用271至386行代码，即可将三个先验检查器的核心逻辑重建为Boomslang模块，性能相当或更优。借助Boomslang，我们还在TiDB中发现了一个新漏洞，审计了JuiceFS文件系统的元数据层，检查了MariaDB中的供应商特定行为，支持了五个先前未检查过的隔离级别，并确认了严格可串行化正确性的理论结果。