A memory consistency model (MCM) is the part of a programming
language or computer architecture specification that defines which
values can legally be read from shared memory locations. Because
MCMs take into account various optimisations employed by architectures
and compilers, they are often complex and counterintuitive,
which makes them challenging to design and to understand.
We identify four 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 are instances of a general
constraint-satisfaction problem to which the solution is either a program
or a pair of programs. Although this problem is intractable for
automatic solvers when phrased over programs directly, we show
how to solve analogous constraints over program executions, and
then construct programs that satisfy the original constraints.
Our technique, which is implemented in the Alloy modelling
framework, is illustrated on several software- and architecture-level
MCMs, both axiomatically and operationally defined.We automatically
recreate several known results, often in a simpler form, including:
distinctions between variants of the C11 MCM; a failure
of the ‘SC-DRF guarantee’ in an early C11 draft; that x86 is
‘multi-copy atomic’ and Power is not; bugs in common C11 compiler
optimisations; and bugs in a compiler mapping from OpenCL
to AMD-style GPUs. We also use our technique to develop and
validate a new MCM for NVIDIA GPUs that supports a natural
mapping from OpenCL.