Abstract

We identify five tasks involved in designing and reasoning about memory consistency models (MCMs): generating conformance tests, distinguishing two MCMs, searching for monotonicity violations, debugging compilation schemes, and checking the “SC-DRF guarantee”. We show that each of these tasks corresponds to solving an instance of a general constraint-satisfaction problem. We further show that although these constraints are not 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. In particular, we generate: programs that distinguish several recently-published variants of the C11 MCM , monotonicity violations in both C11 and x86, compilation quirks from OpenCL to NVIDIA and AMD -style GPUs, and SC-DRF violations in an early draft of C11 . In several cases, our automatically-generated solutions are either new or substantially simpler than those found manually in previous work.

This is joint work with Mark Batty (U Kent), Tyler Sorensen (Imperial) and George A. Constantinides (Imperial).