Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT
Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT
复制标题
使用逻辑编程和 SAT 分析 Intel Itanium 内存排序规则
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Konrad Slind
中科院分区：
文献类型：
--
作者：
Yue Yang;G. Gopalakrishnan;G. Lindstrom;Konrad Slind
我们提出了一个非操作的方法来指定和分析共享内存一致性模型。该方法使用高阶逻辑以公理化的方式捕获执行跟踪上的一组完整的排序约束。一个直接编码的语义与约束逻辑编程语言提供了一个互动的和增量的框架，行使和验证有限的测试程序。该框架也被改编为生成等价的布尔可满足性（SAT）问题。这些技术使内存模型规范可执行，这是大多数非操作方法所缺乏的强大功能。作为一个例子，我们提供了一个简洁的形式化的英特尔安腾内存模型，并显示如何约束求解和SAT求解可以有效地应用于计算机辅助分析。令人鼓舞的初步结果证明了复杂工业设计的可扩展性。
We present a non-operational approach to specifying and analyzing shared memory consistency models. The method uses higher order logic to capture a complete set of ordering constraints on execution traces, in an axiomatic style. A direct encoding of the semantics with a constraint logic programming language provides an interactive and incremental framework for exercising and verifying finite test programs. The framework has also been adapted to generate equivalent boolean satisfiability (SAT) problems. These techniques make a memory model specification executable, a powerful feature lacked in most non-operational methods. As an example, we provide a concise formalization of the Intel Itanium memory model and show how constraint solving and SAT solving can be effectively applied for computer aided analysis. Encouraging initial results demonstrate the scalability for complex industrial designs.