Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models
Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models
复制标题
对宽松记忆模型的顺序一致性进行健全且完整的监控
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
C. Stergiou
中科院分区：
文献类型：
--
作者：
Jacob Burnim;Koushik Sen;C. Stergiou
我们提出了一种技术，用于验证一个程序有没有违反顺序一致性（SC）的执行时，运行在宽松的内存模型总存储顺序（TSO）和部分存储顺序（PSO）。该技术的工作原理是通过监测顺序一致的程序执行，以检测类似的程序执行可能无法顺序一致下TSO或PSO。我们提出了新的监测算法，是健全的和完整的TSO和PSO-如果一个程序可以表现出SC违反下TSO或PSO，那么相应的监视器可以检测到这对一些SC执行。监控算法自然产生于这些放松的记忆模型的操作定义，突出了操作性地而不是公理化地查看放松的记忆模型的优势。我们将我们的技术应用到几个并发数据结构和同步原语，检测一些违反顺序一致性。
We present a technique for verifying that a program has no executions violating sequential consistency (SC) when run under the relaxed memory models Total Store Order (TSO) and Partial Store Order (PSO). The technique works by monitoring sequentially consistent executions of a program to detect if similar program executions could fail to be sequentially consistent under TSO or PSO.We propose novel monitoring algorithms that are sound and complete for TSO and PSO--if a program can exhibit an SC violation under TSO or PSO, then the corresponding monitor can detect this on some SC execution. The monitoring algorithms arise naturally from the operational definitions of these relaxed memory models, highlighting an advantage of viewing relaxed memory models operationally rather than axiomatically. We apply our technique to several concurrent data structures and synchronization primitives, detecting a number of violations of sequential consistency.