使事务隔离检查变得实用
Making TransactionIsolation Checking Practical
AI总结：
本文提出Boomslang框架，通过模块化设计实现对事务隔离级别的高效检查，支持多种操作类型并发现TiDB等系统中的新bug。
摘要：
检查数据库事务是否符合隔离级别是一个关键但具有挑战性的问题。本文提出了Boomslang，首个通用检查框架，能够验证此前无法验证的配置。Boomslang在三个方面超越了先前工作：(1)支持现代事务性键值存储提供的任意操作类型；(2)无需了解数据库内部细节；(3)提供模块化、可扩展的流水线，便于定制和优化。Boomslang采用前后端分离设计，前端将数据库跟踪解析为抽象语义图，再通过语义分析转换为低级中间表示（IR）。后端将IR转换为SMT求解器的约束集。这种设计得益于IR中的关键抽象——超位置，能够捕捉任意操作和缺失信息带来的不确定性和复杂性。实验表明，仅用271-386行代码，即可将三个先前检查器的核心逻辑重写为Boomslang模块，实现相仿或更优的性能。使用Boomslang，我们还发现TiDB中的新bug，审计JuiceFS文件系统的元数据层，检查MariaDB的供应商特定行为，支持五个此前未检查的隔离级别，并确认严格可串行化的正确性理论结果。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
