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.
翻译:现代应用程序如社交网络系统和电子商务平台等都以大型数据库为中心,用于存储和检索数据。对数据库的访问通常被封装在事务中,以使共享数据的计算与其他并发计算隔离,并具有容错能力。现代数据库以牺牲隔离性为代价来提高性能。隔离级别越低,数据库容许的行为就越多,开发人员需要确保应用程序能够容忍这些行为。在本文中,我们提出了一种针对动态部分顺序约简的无状态模型检查算法,用于研究依赖于该算法的应用程序的正确性。这些算法适用于广泛使用的若干种弱隔离级别,包括Read Committed、Causal Consistency、Snapshot Isolation和Serializability。我们证明了这些算法既完备、又正确,并在所有情况下都具有多项式内存消耗的优点。我们报告了在Java Pathfinder的上下文中应用这些算法到一些具有挑战性的应用程序上,并从分布式系统和数据库领域的文献中选取案例进行了验证。