Modern applications, such as social networking systems and e-commerce platforms are centered around using large-scale databases for storing and retrieving data. Accesses to the database are typically enclosed in transactions that allow computations on shared data to be isolated from other concurrent computations and resilient to failures. Modern databases trade isolation for performance. The weaker the isolation level is, the more behaviors a database is allowed to exhibit and it is up to the developer to ensure that their application can tolerate those behaviors. In this work, we propose stateless model checking algorithms for studying correctness of such applications that rely on dynamic partial order reduction. These algorithms work for a number of widely-used weak isolation levels, including Read Committed, Causal Consistency, Snapshot Isolation, and Serializability. We show that they are complete, sound and optimal, and run with polynomial memory consumption in all cases. We report on an implementation of these algorithms in the context of Java Pathfinder applied to a number of challenging applications drawn from the literature of distributed systems and databases.
翻译:现代应用程序,例如社交网络系统和电子商务平台,基于大规模数据库进行数据存储和检索单位的操作,这些操作通常封装在事务中,从而使共享数据的计算与其他并发计算隔离,并具有容错性。现代数据库通过弱化隔离级别来提高性能。隔离级别越弱,数据库允许展现的行为越多,开发人员需要确保应用程序能够容忍这些行为。在这项工作中,我们提出了一种基于动态部分顺序规约的无状态模型检查算法,用于研究依赖于弱隔离级别的应用程序的正确性,其中包括读提交、因果一致性、快照隔离和串行化等广泛使用的隔离级别。我们证明了这些算法在所有情况下都是完备、正确且最优,同时在内存消耗方面具有多项式复杂度。我们报告了这些算法在Java Pathfinder上的实现,应用于来自分布式系统和数据库文献领域的若干具有挑战性的应用程序。