We consider the verification of liveness properties for concurrent programs running on weak memory models. To that end, we identify notions of fairness that preclude demonic non-determinism, are motivated by practical observations, and are amenable to algorithmic techniques. We provide both logical and stochastic definitions of our fairness notions and prove that they are equivalent in the context of liveness verification. In particular, we show that our fairness allows us to reduce the liveness problem (repeated control state reachability) to the problem of simple control state reachability. We show that this is a general phenomenon by developing a uniform framework which serves as the formal foundation of our fairness definition and can be instantiated to a wide landscape of memory models. These models include SC, TSO, PSO, (Strong/Weak) Release-Acquire, Strong Coherence, FIFO-consistency, and RMO.

翻译：我们研究在弱内存模型上运行的并发程序的活动性验证问题。为此，我们识别出能够排除恶魔非确定性、受实际观察驱动且适用于算法技术的公平性概念。我们给出了公平性概念的逻辑定义和随机定义，并证明它们在活动性验证语境下是等价的。特别地，我们证明所提出的公平性允许将活动性问题（重复控制状态可达性）归约为简单控制状态可达性问题。通过构建统一框架——该框架作为公平性定义的形式化基础，并可实例化至广泛的内存模型谱系，我们证明了这一现象的普遍性。这些模型包括SC、TSO、PSO、（强/弱）Release-Acquire、强相干性、FIFO一致性及RMO。