一句话：提出覆盖 Read Committed、因果一致性、快照隔离与可串行化的动态偏序归约模型检测算法，完备、可靠、最优且多项式内存。
现代大规模数据库为性能而牺牲隔离性，隔离级别越弱，数据库允许出现的行为越多，应用程序必须自行容忍这些行为，因此需要自动检查程序在弱隔离语义下是否保持正确。本文提出基于动态偏序归约（DPOR）的无状态模型检测算法，适用于 Read Committed、因果一致性、快照隔离与可串行化等多种广泛使用的隔离级别。作者证明这些算法是完备、可靠且最优的，并始终以多项式内存运行。作者在 Java Pathfinder 中实现了上述算法，并在取自分布式系统与数据库文献的多项挑战性应用上进行了实验评估。
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.
@article{paperbot1964,
title = {Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation Levels},
author = {Ahmed Bouajjani and Constantin Enea and Enrique Román-Calvo},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591243}
}