摘要
现代数据库采用弱隔离级别来满足高可用性事务。然而,最近许多生产数据库中都出现了弱隔离错误。这引发了人们对数据库实现是否在实践中真正实现其承诺的隔离保证的担忧。在本文中,我们介绍了 Plume,这是第一个高效、完整的弱隔离级别黑盒检查器。Plume 建立在模块化、细粒度、事务异常模式的基础上,我们利用这些模式建立了代表性弱隔离级别的合理和完整特征,包括读取提交、读取原子性和事务因果一致性。Plume 利用两种技术(向量和树时钟)的新颖组合来加速隔离检查。我们广泛的评估表明,Plume 可以在大量异常数据库执行历史中重现所有已知违规行为,在三个生产数据库中检测新的隔离错误以及信息反例,比最先进的检查器发现更多的弱隔离异常,并在各种工作负载下有效地验证隔离保证。
作者:
- SI LIU, ETH Zurich, Switzerland
- LONG GU, State Key Laboratory for Novel Software Technology, Nanjing University, China
- HENGFENG WEI*, State Key Laboratory for Novel Software Technology, Nanjing University, China
- DAVID BASIN, ETH Zurich, Switzerland