$$
\def\po{\mathsf{\textcolor{\red}{po}}}
\def\so{\mathsf{\textcolor{\purple}{so}}}
\def\wr{\mathsf{\textcolor{\teal}{wr}}}
\def\co{\mathsf{\textcolor{\orange}{co}}}
\def\Swap{\mathsf{Swap}}
$$
摘要
现代应用程序,如社交网络系统和电子商务平台,以大规模数据库为核心,用于存储和检索数据。对数据库的访问通常封装在事务中,允许对共享数据进行的计算与其他并发计算隔离,并具有容错性。现代数据库以性能为代价来交换隔离程度。隔离级别越低,数据库允许表现出的行为就越多,而开发人员需要确保他们的应用程序能够容忍这些行为。
在这项工作中,我们提出了一种基于动态偏序约减的无状态模型检查算法,用于研究依赖于多种常见弱隔离级别的应用程序的正确性,包括读已提交、因果一致性、快照隔离和可串行化。我们展示了这些算法在所有情况下都是完备的、正确的和最优的,并且在所有情况下都具有多项式内存消耗。我们报告了这些算法在 Java Pathfinder 环境中的实现,应用于分布式系统和数据库文献中的一些具有挑战性的应用程序。
作者: