一句话：提出首个高效、完备的弱隔离级别黑盒检查器 Plume，可检测数据库隔离缺陷并生成反例。
现代数据库为高可用事务采用弱隔离级别，但生产数据库中频繁出现隔离缺陷，因此需判定实现是否真正满足承诺的隔离保证。本文提出 Plume，首个高效且完备的弱隔离级别黑盒检查器。Plume 基于模块化、细粒度的事务异常模式，为读已提交、读原子性和事务因果一致性等代表性弱隔离级别建立可靠且完备的刻画，并结合向量时钟与树时钟加速检查。评估表明，Plume 能复现大量异常执行历史中的全部已知违规，在三个生产数据库中发现新的隔离缺陷并给出有信息量的反例，比现有最优检查器发现更多弱隔离异常，且能在多种工作负载下高效验证隔离保证。
Modern databases embrace weak isolation levels to cater for highly available transactions. However, weak isolation bugs have recently manifested in many production databases. This raises the concern of whether database implementations actually deliver their promised isolation guarantees in practice. In this paper we present Plume, the first efficient, complete, black-box checker for weak isolation levels. Plume builds on modular, fine-grained, transactional anomalous patterns, with which we establish sound and complete characterizations of representative weak isolation levels, including read committed, read atomicity, and transactional causal consistency. Plume leverages a novel combination of two techniques, vectors and tree clocks, to accelerate isolation checking. Our extensive assessment shows that Plume can reproduce all known violations in a large collection of anomalous database execution histories, detect new isolation bugs in three production databases along with informative counterexamples, find more weak isolation anomalies than the state-of-the-art checkers, and efficiently validate isolation guarantees under a wide variety of workloads.
@article{0003GWB24,
title = {Plume: Efficient and Complete Black-Box Checking of Weak Isolation Levels},
author = {Si Liu and Long Gu and Hengfeng Wei and David Basin},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689742}
}