The Release-Acquire (RA) semantics and its variants are some of the most fundamental models of concurrent semantics for architectures, programming languages, and distributed systems. Several steps have been taken in the direction of testing such semantics, where one is interested in whether a single program execution is consistent with a memory model. The more general verification problem, i.e., checking whether any allowed program run is consistent with a memory model, has still not been studied as much. The purpose of this work is to bridge this gap. We tackle the verification problem, where, given an implementation described as a register machine, we check if any of its runs violates the RA semantics or its Strong (SRA) and Weak (WRA) variants. We show that verifying WRA in this setup is in O(n5 ), while verifying the RA and SRA is PSPACE complete. This both answers some fundamental questions about the complexity of these problems, but also provides insights on the expressive power of register machines as a model.

翻译：释放-获取（RA）语义及其变体是架构、编程语言和分布式系统中最基础的并发语义模型之一。已有研究在测试此类语义方面取得了若干进展，其关注点在于判断单次程序执行是否与内存模型一致。然而，更一般的验证问题——即检查任意允许的程序运行是否与内存模型一致——尚未得到充分研究。本文旨在弥合这一空白。我们研究验证问题：给定一个由寄存器机描述的实现，检查其任意运行是否违反RA语义或其强（SRA）与弱（WRA）变体。我们证明，在此设定下验证WRA的复杂度为O(n^5)，而验证RA和SRA的复杂度为PSPACE完全。这不仅回答了关于这些问题复杂度的一些基础问题，也为寄存器机作为一种模型的表达能力提供了洞见。