Skip to main content

Automatically Comparing Memory Consistency Models

Wickerson, John, Batty, Mark, Sorensen, Tyler, Constantinides, George A. (2017) Automatically Comparing Memory Consistency Models. In: ACM SIGPLAN Notices - POPL '17. POPL 2017 Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. POPL Principles of Programming Languages . pp. 190-204. ACM, New York, USA ISBN 978-1-4503-4660-3. (doi:10.1145/3093333.3009838) (KAR id:63503)

PDF Author's Accepted Manuscript
Language: English
Download (370kB) Preview
[thumbnail of memalloy.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL


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.

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)
DOI/Identification number: 10.1145/3093333.3009838
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: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Batty
Date Deposited: 21 Sep 2017 07:54 UTC
Last Modified: 10 Mar 2021 17:29 UTC
Resource URI: (The current URI for this page, for reference purposes)
Batty, Mark:
  • Depositors only (login required):


Downloads per month over past year