EagleBear2002 的博客

这里必须根绝一切犹豫，这里任何怯懦都无济于事

发表于 更新于 分类于
本文字数： 950 阅读时长 ≈ 1 分钟

摘要

本文梳理了目前主流事务执行历史验证问题的解决方案，对比了各种工具的优劣，尝试提出新的技术路线以改进效率。

验证工具 解决思路 创新点 性能 待改进之处
Cobra1 约束求解 将验证问题建模为 Polygraph 上的约束求解问题 目前已知最高效的 SER 验证工具 未深度整合 SMT
PolySI2 约束求解 将 Polygraph 拓展为 BCpolygraph，同样将 SI 验证问题转化成 BC-polygraph 上的判环问题 PolySI 比 Viper 的性能更为优异，可扩展性也更强，最大规模可以在 40 小时内处理具有百万级事务数量、十亿级键数量的执行历史。 未深度整合 SMT
Viper3 约束求解 问题转化为 polygraph（某种变体）上的判环问题
dbcop4 暴力搜索 dbcop-SER 的性能低于 Cobra，这是因为它会产生大量的无效搜索分支 存在大量无效搜索，内存消耗极大，影响算法可扩展性

  1. Cheng Tan, Changgeng Zhao, Shuai Mu, and Michael Walfish. 2020. COBRA: Making transactional key-value stores verifiably serializable. In OSDI’20.Article 4, 18 pages.↩︎

  2. Kaile Huang, Si Liu, Zhenge Chen, Hengfeng Wei, David Basin, Haixiang Li, and Anqun Pan. Efficient Black-box Checking of Snapshot Isolation in Databases. PVLDB, 16(6): 1264 - 1276, 2023. To appear on PVLDB 2023.↩︎

  3. Jian Zhang, Ye Ji, Shuai Mu, Cheng Tan (2023). Viper: a fast snapshot Isolation Checker. To appear on EuroSys 2023.↩︎

  4. Ranadeep Biswas and Constantin Enea. 2019. On the complexity of checkingtransactional consistency. Proc. ACM Program. Lang. 3, OOPSLA, Article 165 (October 2019), 28 pages.↩︎