MemSAT: checking axiomatic specifications of memory models
MemSAT: checking axiomatic specifications of memory models
复制标题
MemSAT：检查内存模型的公理规范
DOI：
10.1145/1806596.1806635
复制
发表时间：
2010
影响因子：
--
通讯作者：
Julian T Dolby
中科院分区：
文献类型：
--
作者：
Emina Torlak;M. Vaziri;Julian T Dolby
内存模型很难解释，因为它们很复杂，这源于需要在编程简易性和允许编译器和硬件优化之间取得平衡。在本文中，我们提出了一个自动化工具MemSAT，它可以帮助调试和推理内存模型。给定内存模型的公理规范和包含断言的多线程测试程序，如果可以找到断言和内存模型公理，MemSAT输出程序的跟踪。该工具是全自动的，基于SAT解算器。如果它找不到踪迹，它会输出内存模型和程序约束的最小子集，这些约束是无法满足的。我们使用MemSAT根据它们发布的测试用例检查了几个现有的内存模型，包括Manson等人的当前Java内存模型。塞夫西克和阿斯皮纳尔对其进行了修订。我们发现测试程序的预期结果和实际结果之间存在细微的差异。
Memory models are hard to reason about due to their complexity, which stems from the need to strike a balance between ease-of-programming and allowing compiler and hardware optimizations. In this paper, we present an automated tool, MemSAT, that helps in debugging and reasoning about memory models. Given an axiomatic specification of a memory model and a multi-threaded test program containing assertions, MemSAT outputs a trace of the program in which both the assertions and the memory model axioms are satisfied, if one can be found. The tool is fully automatic and is based on a SAT solver. If it cannot find a trace, it outputs a minimal subset of the memory model and program constraints that are unsatisfiable. We used MemSAT to check several existing memory models against their published test cases, including the current Java Memory Model by Manson et al. and a revised version of it by Sevcik and Aspinall. We found subtle discrepancies between what was expected and the actual results of test programs.