一句话：提出 RAT-CAT-SAT，用关系逻辑可满足性与循环证明系统对 CAT 内存一致性模型进行模型检测。
内存一致性模型常以 CAT 语言公理化描述，如何自动验证其性质并比较不同模型是挑战。本文提出 RAT-CAT-SAT 模型检测方法，支持 CAT 的完整 rational 片段：除 Kleene 星、关系复合和并集外，首次支持交集、逆关系及从集合构造关系。方法将模型检测归约为关系逻辑理论的可满足性问题，核心是可靠、完备且复杂度最优的新理论求解器；其中循环证明系统可在运行中检测不变量，从而在找到模型或证明不可满足时提前终止。求解器易于实现，并可与启发式结合。作者实现其与反例引导抽象精化（CEGAR）的组合，并在多个基准上取得有希望的结果。
We present a model checking approach for axiomatic memory consistency models written in the language CAT. It can prove properties of single memory models like the monotonicity of barriers, and also compare models like TSO and ARM8. To achieve this expressiveness, our approach supports the full rational fragment of CAT. We not only support the Kleene star operation, composition, and union to define relations in a memory model, but also, for the first time, intersection, converse, and the construction of relations from sets. Our model checking approach for memory consistency models is logical in nature: we formulate the problem as satisfiability in a logical theory of relations. Our technical contribution is then a new theory solver that is sound, complete, and optimal from a complexity point of view. At the heart of our solver is a cyclic proof system that can detect invariants on-the-fly. This allows us to terminate early not only in the case that a model has been found, but also in the case of unsatisfiability. Our solver is easy to implement and easy to combine with heuristics. We have implemented a combination with counterexample-guided abstraction refinement, and exercised the prototype on a number of benchmarks — with promising results.
@article{paperbot3839,
title = {RAT-CAT-SAT: Model Checking Memory Consistency Models},
author = {Jan Grünke and Thomas Haas and Roland Meyer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798208}
}