UMM: an operational memory model specification framework with integrated model checking capability
UMM: an operational memory model specification framework with integrated model checking capability
复制标题
DOI：
10.1002/cpe.837
复制
发表时间：
2005-04
期刊：
影响因子：
--
通讯作者：
Yue Yang;G. Gopalakrishnan;G. Lindstrom
中科院分区：
文献类型：
--
作者：
Yue Yang;G. Gopalakrishnan;G. Lindstrom
鉴于现代共享内存系统的复杂性质，至关重要的是有一种系统的方法来指定和分析记忆一致性的要求，我们提出了UMM规范框架，该框架集成了两个关键功能以支持内存模型：（i ）IT员工一个简单而通用的内存抽象，可以将大量的内存模型作为具有统一符号的保护命令，（ii）提供内置模型检查功能可以使用此框架进行正式推理，可以用参数化的样式指定内存模型 - 设计师可以简单地重新定义一些绕过一些规则和可见性订购规则，以获得另一个古典模型的可执行规范。内存模型，包括顺序一致性，连贯性和婴儿车，以说明应用此框架的一般技术Java内存模型的替代规范，基于Manson和Pugh的建议，并演示了如何使用模型检查分析Java线程语义。从一种风格到另一种样式。
Given the complicated nature of modern shared memory systems, it is vital to have a systematic approach to specifying and analyzing memory consistency requirements. In this paper, we present the UMM specification framework, which integrates two key features to support memory model verification: (i) it employs a simple and generic memory abstraction that can capture a large collection of memory models as guarded commands with a uniform notation, and (ii) it provides built‐in model checking capability to enable formal reasoning about thread behaviors. Using this framework, memory models can be specified in a parameterized style—designers can simply redefine a few bypassing rules and visibility ordering rules to obtain an executable specification of another memory model. We formalize several classical memory models, including Sequential Consistency, Coherence, and PRAM, to illustrate the general techniques of applying this framework. We then provide an alternative specification of the Java memory model, based on a proposal from Manson and Pugh, and demonstrate how to analyze Java thread semantics using model checking. We also compare our operational specification style with axiomatic specification styles and explore a mechanism that converts a memory model definition from one style to the other. Copyright © 2005 John Wiley & Sons, Ltd.