一句话：证明 TSO 下参数化并发程序可达性问题是 PSPACE 完全，并刻画初始读与原子 RMW 对复杂度的影响。
本文研究全存储序（TSO）语义下并发程序的参数化验证问题。程序由任意数量相同的进程组成，这些进程通过共享变量上的读写操作进行通信。论文证明了对于这类系统，可达性问题是 PSPACE 完全的。进一步地，作者分析了两个关键变体：如果禁止进程读取内存中变量的初始值，则可达性问题的复杂度降为多项式时间；如果允许进程执行原子读-改-写操作，则可达性问题具有非原始递归复杂度。这些结果精确刻画了 TSO 下参数化验证的复杂度边界，揭示了初始读能力和原子 RMW 操作对验证难度的根本影响。
We consider parameterized verification of concurrent programs under the Total Store Order (TSO) semantics. A program consists of a set of processes that share a set of variables on which they can perform read and write operations. We show that the reachability problem for a system consisting of an arbitrary number of identical processes is PSPACE-complete. We prove that the complexity is reduced to polynomial time if the processes are not allowed to read the initial values of the variables in the memory. When the processes are allowed to perform atomic read-modify-write operations, the reachability problem has a non-primitive recursive complexity.
@article{paperbot557,
title = {Parameterized verification under TSO is PSPACE-complete},
author = {Parosh Aziz Abdulla and Mohamed Faouzi Atig and Rojin Rezvan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371094}
}