Robustness against Power is PSpace-complete
Robustness against Power is PSpace-complete
复制标题
抗功率鲁棒性是 PSpace 完备的
DOI：
10.1007/978-3-662-43951-7_14
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
R. Meyer
中科院分区：
文献类型：
--
作者：
E. Derevenetc;R. Meyer
Power是由IBM、飞思卡尔和其他几家公司开发的RISC架构，并在一系列Power处理器中实现。该体系结构的特点是一个宽松的内存模型，在内存访问的顺序和原子性方面提供了非常弱的保证。由于这些弱点，一些在顺序一致性（SC）下正确的程序在Power下运行时会出现不希望看到的效果。我们说这些程序对于Power内存模型来说不是健壮的。从形式上讲，如果Power下的每个计算都与某些SC计算具有相同的数据和控制依赖关系，则程序是健壮的。我们的贡献是一个针对Power内存模型的并发程序健壮性的决策过程。它基于三个观点。首先，我们根据happensbefore关系的不周期性重新表述鲁棒性。其次，我们证明了在循环发生前关系的计算中存在一个具有一定范式的计算。最后，我们将这种范式计算的存在性简化为语言空性问题。总的来说，这产生了一个pspace算法，用于检查对Power的鲁棒性。我们用一个匹配的下界来补齐它以证明pspace的完备性。
Power is a RISC architecture developed by IBM, Freescale, and several other companies and implemented in a series of POWER processors. The architecture features a relaxed memory model providing very weak guarantees with respect to the ordering and atomicity of memory accesses.Due to these weaknesses, some programs that are correct under sequential consistency (SC) show undesirable effects when run under Power. We say that these programs are not robust against the Power memory model. Formally, a program is robust if every computation under Power has the same data and control dependencies as some SC computation.Our contribution is a decision procedure for robustness of concurrent programs against the Power memory model. It is based on three ideas. First, we reformulate robustness in terms of the acyclicity of a happensbefore relation. Second, we prove that among the computations with cyclic happens-before relation there is one in a certain normal form. Finally, we reduce the existence of such a normal-form computation to a language emptiness problem. Altogether, this yields a PSpacealgorithm for checking robustness against Power. We complement it by a matching lower bound to show PSpace-completeness.
登录
查看更多内容
DOI：
10.1007/978-3-540-70545-1_12
发表时间：
2008-07
期刊：
--
影响因子：
--
作者：
S. Burckhardt;M. Musuvathi
通讯作者：
S. Burckhardt;M. Musuvathi
DOI：
10.4230/lipics.fsttcs.2013.127
发表时间：
2013
期刊：
ArXiv
影响因子：
--
作者：
G. Călin;E. Derevenetc;R. Majumdar;R. Meyer
通讯作者：
R. Meyer
更好的 x86 内存模型：x86-TSO（扩展版本）
DOI：
--
发表时间：
2009
期刊：
影响因子：
--
作者：
Scott Owens;Susmit Sarkar;Peter Sewell
通讯作者：
Peter Sewell
对宽松记忆模型的顺序一致性进行健全且完整的监控
DOI：
--
发表时间：
2011
期刊：
International Conference on Tools and Algorithms for Construction and Analysis of Systems
影响因子：
--
作者：
Jacob Burnim;Koushik Sen;C. Stergiou
通讯作者：
C. Stergiou
了解 POWER 多处理器
影响因子：
--
作者：
Sarkar S
通讯作者：
Sarkar S