一句话：提出 AWDIT，可证明最优地测试 RC、RA 和 CC 弱隔离级别，并显著提升效率。
现代数据库为降低延迟、提高吞吐常采用弱隔离级别，但生产系统仍存在隔离缺陷，破坏数据一致性契约。黑盒测试通过检查事务历史是否符合指定隔离级别来发现此类缺陷；已有测试器虽为多项式时间，但复杂度过高，难以扩展到大规模负载。本文提出 AWDIT，一种高效且可证明最优的弱数据库隔离测试器。给定大小为 n、含 k 个会话的历史 H，AWDIT 测试 RC、RA、CC 的时间分别为 O(n^{3/2})、O(n^{3/2})、O(n·k)，显著优于现有方法；并基于组合 BMM 假设证明，RC 到 CC 间任意弱隔离级别均有 n^{3/2} 下界，因此本质上最优。实验显示，对约 20% 最大历史，其相对最佳基线在 RC、RA、CC 上平均加速 245×、193×、62×。
Database isolation is a formal contract concerning the level of data consistency that a database provides to its clients. In order to achieve low latency, high throughput, and partition tolerance, modern databases forgo strong transaction isolation for weak isolation guarantees. However, several production databases have been found to suffer from isolation bugs , breaking their data-consistency contract. Black-box testing is a prominent technique for detecting isolation bugs, by checking whether histories of database transactions adhere to a prescribed isolation level. In order to test databases on realistic workloads of large size, isolation testers must be as efficient as possible, a requirement that has initiated a study of the complexity of isolation testing. Although testing strong isolation has been known to be NP-complete, weak isolation levels were recently shown to be testable in polynomial time, which has propelled the scalability of testing tools. However, existing testers have a large polynomial complexity, restricting testing to workloads of only moderate size, which is not typical of large-scale databases. How efficiently can we provably test weak database isolation? In this work, we develop AWDIT, a highly-efficient and provably optimal tester for weak database isolation . Given a history H of size n and k sessions, AWDIT tests whether H satisfies the most common weak isolation levels of Read Committed (RC), Read Atomic (RA), and Causal Consistency (CC) in time O ( n 3/2 ), O ( n 3/2 ), and O ( n · k ), respectively, improving significantly over the state of the art. Moreover, we prove that AWDIT is essentially optimal , in the sense that there is a lower bound of n 3/2 , based on the combinatorial BMM hypothesis, for any weak isolation level between RC and CC. Our experiments show that AWDIT is significantly faster than existing, highly optimized testers; e.g., for the ∼20﹪ largest histories, AWDIT obtains an average speedup of 245×, 193×, and 62× for RC, RA, and CC, respectively, over the best baseline.
@article{paperbot3065,
title = {AWDIT: An Optimal Weak Database Isolation Tester},
author = {Lasse Møldrup and Andreas Pavlogiannis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3742465}
}