对Power的鲁棒性是PSPACE完全的

Power是IBM、Freescale等公司开发的RISC架构，并在一系列POWER处理器中实现。该架构具有宽松的内存模型，在内存访问的顺序和原子性方面提供非常弱的保证。由于这些弱点，一些在顺序一致性（SC）下正确的程序在Power下运行时会出现不良效果。我们称这些程序对Power内存模型不鲁棒。形式上，如果一个程序在Power下的每次计算都具有与某个SC计算相同的数据和控制依赖关系，则该程序是鲁棒的。我们的贡献是针对Power内存模型的并发程序鲁棒性的判定过程。它基于三个想法。首先，我们将鲁棒性重新表述为happens-before关系的无环性。其次，我们证明在具有循环happens-before关系的计算中，存在一个特定范式的计算。最后，我们将这种范式计算的存在性简化为语言空性问题。总之，这产生了一个用于检查对Power鲁棒性的PSPACE算法。我们通过匹配的下界来证明PSPACE完全性。