Skip to main content

Automatically Comparing Memory Consistency Models

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

PDF Author's Accepted Manuscript
Language: English
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.

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: Book section
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: 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 Feb 2020 04:09 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/63503 (The current URI for this page, for reference purposes)
Batty, Mark: https://orcid.org/0000-0001-7053-4364
  • Depositors only (login required):

Downloads

Downloads per month over past year