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框架中的实现，并应用于分布式系统和数据库文献中若干具有挑战性的应用实例。