The verification of concurrent programs remains an open challenge due to the non-determinism in inter-process communication. One algorithmic problem in this challenge is the consistency verification of concurrent executions. Consistency verification under a reads-from map allows to compute the reads-from (RF) equivalence between concurrent traces, with direct applications to areas such as Stateless Model Checking (SMC). The RF equivalence was recently shown to be coarser than the standard Mazurkiewicz equivalence, leading to impressive scalability improvements for SMC under SC (sequential consistency). However, for the relaxed memory models of TSO and PSO (total/partial store order), the algorithmic problem of deciding the RF equivalence, as well as its impact on SMC, has been elusive. In this work we solve the problem of consistency verification for the TSO and PSO memory models given a reads-from map, denoted VTSO-rf and VPSO-rf, respectively. For an execution of $n$ events over $k$ threads and $d$ variables, we establish novel bounds that scale as $n^{k+1}$ for TSO and as $n^{k+1}\cdot \min(n^{k^2}, 2^{k\cdot d})$ for PSO. Based on our solution to these problems, we develop an SMC algorithm under TSO and PSO that uses the RF equivalence. The algorithm is exploration-optimal, in the sense that it is guaranteed to explore each class of the RF partitioning exactly once, and spends polynomial time per class when $k$ is bounded. We implement all our algorithms in the SMC tool Nidhugg, and perform a large number of experiments over benchmarks from existing literature. Our experimental results show that our algorithms for VTSO-rf and VPSO-rf provide significant scalability improvements over standard alternatives. When used for SMC, the RF partitioning is often much coarser than the standard Shasha-Snir partitioning for TSO/PSO, which yields a significant speedup in the model checking task.

翻译：由于在进程间通信中没有确定性,对并行程序进行核查仍是一个公开的挑战。在这项挑战中,一个算法上的问题是同步处决的一致性。在地图下进行读取核查,可以计算同时的痕迹之间的读取(RF)等值,直接应用到诸如Nestlemode Checking(SMC)等域。最近显示,VF等值比标准的Mazurkiewicz等值更粗糙,导致SMC在SC(顺序一致性)下的缩放性改进。然而,由于TSO和PSO的存储模型(完全/部分存储顺序)的宽松模式,决定RF等值的算法问题以及其对SMC的影响一直难以捉摸。在这个工作中,我们解决了TSO和PSO的校正性核查问题,我们SO的SO-RV-rf 和VPSO的代数都显示,我们SO的超值事件和超值变量,我们把SO的SO=QQQQ=xxxxxxxxxxxxxxxx。