一句话：将序列程序的重现集推广到弱内存并发程序，给出公平非终止的可靠且多模型完备的证明与自动检测技术。
经典重现集用于刻画序列程序的不终止。本文将其推广到弱内存模型下的并发程序：经典定义要求状态集在迁移下存在封闭，而新定义要求执行集在扩展下存在封闭，并相对于调度器或内存子系统等公平性假设给出。作者证明该推广在所有实用内存模型上对证明公平非终止是可靠的，并在许多模型上完备。为落地，他们提出用基于执行的 lasso 有限表示重现集，在 Dartagnan 中实现 lasso 查找算法，并在 CPU 与 GPU 内存模型下的程序上评估。
Recurrence sets characterize non-termination in sequential programs. We present a generalization of recurrence sets to concurrent programs that run on weak memory models. Sequential programs have operational semantics in terms of states and transitions, and classical recurrence sets are defined as sets of states that are existentially closed under transitions. Concurrent programs have axiomatic semantics in terms of executions, and our new recurrence sets are defined as sets of executions that are existentially closed under extensions. The semantics of concurrent programs is not only affected by the memory model, but also by fairness assumptions about its environment, be it the scheduler or the memory subsystems. Our new recurrence sets are formulated relative to such fairness assumptions. We show that our recurrence sets are sound for proving fair non-termination on all practical memory models, and even complete on many. To turn our theory into practice, we develop a new automated technique for proving fair non-termination in concurrent programs on weak memory models. At the heart of this technique is a finite representation of recurrence sets in terms of execution-based lassos. We implemented a lasso-finding algorithm in Dartagnan, and evaluated it on a number of programs running under CPU and GPU memory models.
@article{HaasMLG26,
title = {Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models},
author = {Thomas Haas and Roland Meyer and Hernán Ponce de León and Andrés Lomelí Garduño},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776687}
}