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框架下针对分布式系统与数据库文献中多个具有挑战性的应用实现的算法结果。