对事务性因果一致性的鲁棒性
摘要：分布式存储系统和数据库广泛应用于各种类型的应用程序。对这些存储系统的事务性访问是一种重要的抽象，使应用程序员可以将一系列操作（即事务）作为原子执行。出于性能原因，现代数据库所实现的一致性模型比标准的可串行化模型要弱，后者对应于在顺序一致性内存上执行的事务原子性抽象。例如，因果一致性是一种在实践中被广泛使用的模型。 本文研究了几种因果一致性变体之间的应用程序特定关系，并解决了自动验证给定的事务性程序在任意因果一致性数据库上执行时是否具有因果一致性鲁棒性的问题，即其所有行为是否可串行化。我们证明了没有写-写竞争的程序在所有这些变体下具有相同的行为集，并且我们证明了检测鲁棒性问题可以在多项式时间内规约到在串行一致共享内存上的状态可达性问题。后一结果的一个令人惊讶的推论是，允许拥有不可比行为集的因果一致性变体允许拥有可比较的鲁棒程序集。此规约还打开了利用现有方法和工具来验证并发程序（假设顺序一致性）以推理在因果一致性数据库上运行的程序的可能性。此外，它还可以确定当在不同站点上执行的程序是有穷状态时，检查鲁棒性问题是可判定的。
作者：Sidi Mohamed Beillahi, Ahmed Bouajjani, and Constantin Enea
论文ID：1906.12095
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-06-22