Model Checking with User-Definable Memory Consistency Models
Model Checking with User-Definable Memory Consistency Models
复制标题
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Tatsuya Abe;T. Maeda
中科院分区：
文献类型：
--
作者：
Tatsuya Abe;T. Maeda
从性能和可扩展性的角度来看，宽松的内存一致性模型是常见的，并且对于多个进程能够共享单个全局地址空间的并行/分布式编程语言（例如分区全局地址空间语言）是必不可少的。然而，松弛的存储器一致性模型的问题在于编程是困难的并且容易出错，因为它们允许在普通顺序存储器一致性模型中不发生的非直观行为。为了解决这个问题，本文提出了一个模型检测框架，用户可以定义自己的内存一致性模型，并检查程序下定义的模型。我们的模型检测框架的关键点是，我们定义了一个基础模型，允许非常宽松的行为，并允许用户定义他们的内存一致性模型作为对基础模型的约束。
From the viewpoint of performance and scalability, relaxed memory consistency models are common and essential for parallel/distributed programming languages in which multiple processes are able to share a single global address space, such as Partitioned Global Address Space languages. However, a problem with relaxed memory consistency models is that programming is difficult and error-prone because they allow non-intuitive behaviors that do not occur in the ordinary sequential memory consistency model. To address the problem, this paper presents a model checking framework in which users are able to define their own memory consistency models, and check programs under the defined models. The key point of our model checking framework is that we define a base model that allows very relaxed behavior, and allow users to define their memory consistency models as constraints on the base model.