NDLI: Automatically comparing memory consistency models

Content Provider	ACM Digital Library
Author	Sorensen, Tyler Constantinides, George A. Wickerson, John Batty, Mark
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.
Starting Page	190
Ending Page	204
Page Count	15
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/3093333.3009838
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	52
Issue Number	1
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1983-05-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	C/c++ Constraint solving Graphics processor (gpu) Model checking Opencl Shared memory concurrency Program synthesis Weak memory models
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Automatically comparing memory consistency models

GPS:navigating weak memory with ghosts, protocols, and separation

Fair stateless model checking

Relaxed separation logic:a program logic for C11 concurrency

Foundations of the C++ concurrency memory model

Dynamic synthesis for relaxed memory models

Verifying read-copy-update in a logic for weak memory

Overhauling SC atomics in c11 and OpenCL Overhauling SC atomics in C11 and OpenCL

CheckFence:checking consistency of concurrent data types on relaxed memory models

Automatically comparing memory consistency models

Similar Documents

Automatically comparing memory consistency models

GPS:navigating weak memory with ghosts, protocols, and separation

Fair stateless model checking

Relaxed separation logic:a program logic for C11 concurrency

Foundations of the C++ concurrency memory model

Dynamic synthesis for relaxed memory models

Verifying read-copy-update in a logic for weak memory

Overhauling SC atomics in c11 and OpenCL Overhauling SC atomics in C11 and OpenCL

CheckFence:checking consistency of concurrent data types on relaxed memory models

Automatically comparing memory consistency models