Automatically comparing memory consistency models

File Description SizeFormat 
JohnPOPL17.pdfAccepted version538.29 kBUnknownView/Open
Title: Automatically comparing memory consistency models
Authors: Wickerson, J
Batty, M
Sorensen, T
Constantinides, GA
Item Type: Conference Paper
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 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.
Issue Date: 1-Jan-2017
Date of Acceptance: 3-Oct-2016
URI: http://hdl.handle.net/10044/1/42342
DOI: https://dx.doi.org/10.1145/3009837.3009838
ISBN: 978-1-4503-4660-3
ISSN: 1523-2867
Publisher: Association for Computing Machinery
Start Page: 190
End Page: 204
Journal / Book Title: ACM Sigplan Notices
Volume: 52
Issue: 1
Copyright Statement: © 2017 ACM. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM Sigplan Notices, https://dl.acm.org/citation.cfm?id=3009838
Sponsor/Funder: Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Royal Academy Of Engineering
Imagination Technologies Ltd
Funder's Grant Number: EP/I020357/1
11908 (EP/K034448/1)
Prof Constantinides Chair
Prof Constantinides Chair
Conference Name: ACM Principles of Programming Languages 2017
Keywords: Science & Technology
Technology
Computer Science, Software Engineering
Computer Science
C/C plus
constraint solving
graphics processor (GPU)
model checking
OpenCL
program synthesis
shared memory concurrency
weak memory models
shared memory con-currency
Software Engineering
Publication Status: Published
Start Date: 2017-01-15
Finish Date: 2017-01-21
Conference Place: Paris, France
Appears in Collections:Faculty of Engineering
Electrical and Electronic Engineering



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

Creative Commonsx