A memory consistency model (MCM) is the part of a programming language or computer architecture specification that defines which values can legally be read when a thread in a concurrent program reads from a shared memory location. Because MCMs have to take into account various optimisations employed by modern architectures (such as store buffering and instruction reordering) and compilers (such as constant propagation), they often end up being complex and counterintuitive, which makes them challenging to design and to understand.
In this work, we identify four important tasks involved in designing and understanding MCMs: generating conformance tests, distinguishing two MCMs, checking compiler optimisations, and checking compiler mappings. We show that all four tasks can be cast as instances of a general constraint-satisfaction problem to which the solution is either a program or a pair of programs. We further show that although these constraints aren’t tractable for automatic solvers when phrased over programs directly, we can solve analogous constraints over program executions, and then reconstruct programs that satisfy the original constraints.
We illustrate our technique, which is implemented in the Alloy modelling framework, on a range of software- and architecture-level MCMs, both axiomatically and operationally defined. First, we automatically recreate – often in a simpler form – several known results, including: distinctions between several variants of the C/C++ MCM; a failure of the ‘SC-DRF guarantee’ in an early C++ draft; that x86 is ‘multi-copy atomic’ and Power is not; bugs in common C/C++ compiler optimisations; and bugs in compiler mappings from OpenCL to AMD-style and NVIDIA GPUs. Second, we use our technique to develop and validate a stronger MCM for NVIDIA GPUs that supports a natural mapping from OpenCL.
This is joint work with Mark Batty (U Kent), Tyler Sorensen (Imperial) and George A. Constantinides (Imperial).