A General Model Checking Framework for Various Memory Consistency Models

Relaxed memory consistency models are common and essential when multiple processes share a single global address space, such as when using multicore CPUs, partitioned global address space languages, and so forth. Programming within these models is difficult and error prone, because of non-intuitive behaviors that could not occur in a sequential memory consistency model. In addition, because the memory consistency models vary from language to language, and CPU to CPU, a program which 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 a prototype implementation of a model checker based on the proposed framework. We have specified the necessary constraints for three practical existing memory consistency models (UPC, Coarray Fortran, and Itanium). Our model checker verified some example programs correctly, and confirmed the expected differences among the three models.