Automatically Comparing Memory Consistency Models

Wickerson, John and Batty, Mark and Sorensen, Tyler and Constantinides, George A. (2017) Automatically Comparing Memory Consistency Models. In: POPL 2017: Symposium on Principles of Programming Languages, 18 - 20 Jan 2017, Paris, France. (doi:https://doi.org/10.1145/3093333.3009838) (Full text available)

PDF - Author's Accepted Manuscript
Download (370kB) Preview
[img]
Preview
Official URL
https://doi.org/10.1145/3093333.3009838

Abstract

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 archi- tectures and compilers, they are often complex and counterintu- itive, 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.

Item Type: Conference or workshop item (Paper)
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Mark Batty
Date Deposited: 21 Sep 2017 07:54 UTC
Last Modified: 20 Jul 2018 14:36 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/63503 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year