A general model checking framework for various memory consistency models
A general model checking framework for various memory consistency models
复制标题
DOI：
10.1007/s10009-016-0429-y
复制
发表时间：
2014-05
影响因子：
1.5
通讯作者：
Tatsuya Abe;T. Maeda
中科院分区：
文献类型：
--
作者：
Tatsuya Abe;T. Maeda
当多个进程共享单个全局地址空间时，例如使用多核 CPU、分布式共享内存编程语言等时，宽松的内存一致性模型是常见且必不可少的。在这些模型中进行编程非常困难并且容易出错，因为在严格的一致性模型中不可能出现非直观的行为。此外，由于内存一致性模型因语言和 CPU 的不同而不同，因此在一个系统上可以正确运行的程序可能在另一个系统上无法运行。为了解决这个问题，本文描述了一个模型检查框架，用户可以在各种内存一致性模型下检查他们的程序。更具体地说，我们的框架提供了一个表现出非常宽松的行为的基本模型，用户可以通过向基本模型添加约束来定义各种一致性模型。本文还描述了 McSPIN，它是基于所提出的框架的模型检查器的原型实现。 McSPIN可以将内存一致性模型作为输入，以及要检查的程序和属性。我们为三个实际的现有内存一致性模型（Unified Parallel C、Coarray Fortran 和 Itanium）指定了必要的约束。 McSPIN正确验证了一些示例程序，并确认了三个模型之间的预期差异。
Relaxed memory consistency models are common and essential when multiple processes share a single global address space, such as when using multicore CPUs, distributed shared-memory programming languages, and so forth. Programming within these models is difficult and error prone, because of non-intuitive behaviors that could not occur in a strict consistency model. In addition, because the memory consistency models vary from language to language, and CPU to CPU, a program that may work correctly on one system may not work on another. To address the problem, this paper describes a model checking framework in which users are able to check their programs under various memory consistency models. More specifically, our framework provides a base model that exhibits very relaxed behaviors, and users are able to define various consistency models by adding constraints to the base model. This paper also describes McSPIN, a prototype implementation of a model checker based on the proposed framework. McSPIN can take a memory consistency model as an input, as well as a program and a property to be checked. We have specified the necessary constraints for three practical existing memory consistency models (Unified Parallel C, Coarray Fortran, and Itanium). McSPIN verified some example programs correctly, and confirmed the expected differences among the three models.