Skip to main content

Overhauling SC atomics in C11 and OpenCL

Batty, Mark and Donaldson, Alastair F. and Wickerson, John (2016) Overhauling SC atomics in C11 and OpenCL. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL Principles of Programming Languages . ACM, New York, USA, pp. 634-648. ISBN 978-1-4503-3549-2. (doi:10.1145/2837614.2837637) (KAR id:51385)

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


Despite the conceptual simplicity of sequential consistency (SC), the semantics of SC atomic operations and fences in the C11 and OpenCL memory models is subtle, leading to convoluted prose descriptions that translate to complex axiomatic formalisations. We conduct an overhaul of SC atomics in C11, reducing the associated axioms in both number and complexity. A consequence of our simplification is that the SC operations in an execution no longer need to be totally ordered. This relaxation enables, for the first time, efficient and exhaustive simulation of litmus tests that use SC atomics. We extend our improved C11 model to obtain the first rigorous memory model formalisation for OpenCL (which extends C11 with support for heterogeneous many-core programming). In the OpenCL setting, we refine the SC axioms still further to give a sensible semantics to SC operations that employ a ‘memory scope’ to restrict their visibility to specific threads. Our overhaul requires slight strengthenings of both the C11 and the OpenCL memory models, causing some behaviours to become disallowed. We argue that these strengthenings are natural, and that all of the formalised C11 and OpenCL compilation schemes of which we are aware (Power and x86 CPUs for C11, AMD GPUs for OpenCL) remain valid in our revised models. Using the HERD memory model simulator, we show that our overhaul leads to an exponential improvement in simulation time for C11 litmus tests compared with the original model, making exhaustive simulation competitive, time-wise, with the non-exhaustive CDSChecker tool.

Item Type: Book section
DOI/Identification number: 10.1145/2837614.2837637
Uncontrolled keywords: Formal methods; graphics processing unit (GPU); heterogeneous programming; HOL theorem prover; language design; program simulation; weak memory models
Subjects: 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: 03 Nov 2015 08:30 UTC
Last Modified: 23 Apr 2022 22:07 UTC
Resource URI: (The current URI for this page, for reference purposes)
Batty, Mark:
  • Depositors only (login required):


Downloads per month over past year