Write a Blog >>
Fri 22 Jan 2016 11:20 - 11:45 at Grand Bay South - Track 2: Semantics and memory models Chair(s): Alexey Gotsman

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 use our improved C11 model to present 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 prove that all of the formalised C11 and OpenCL compilation schemes of which we are aware (Power and x86 for C11, AMD GPU 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.

Poster (poster.pdf)906KiB

Fri 22 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10: Track 2: Semantics and memory modelsResearch Papers at Grand Bay South
Chair(s): Alexey GotsmanIMDEA
10:30 - 10:55
Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA
Research Papers
Shaked FlurUniversity of Cambridge, Kathryn E. GrayUniversity of Cambridge, Christopher PulteUniversity of Cambridge, Susmit SarkarUniversity of St Andrews, Luc MarangetINRIA Rocquencourt, Ali SezginUniversity of Cambridge, Will DeaconARM Ltd., Peter SewellUniversity of Cambridge
Media Attached File Attached
10:55 - 11:20
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
Research Papers
Jean Pichon-PharabodUniversity of Cambridge, Peter SewellUniversity of Cambridge
File Attached
11:20 - 11:45
Overhauling SC atomics in C11 and OpenCL
Research Papers
John WickersonImperial College London, Mark BattyUniversity of Cambridge, Alastair DonaldsonImperial College London
Pre-print File Attached
11:45 - 12:10
Taming Release-Acquire Consistency
Research Papers
Ori LahavMPI-SWS, Nick GiannarakisMPI-SWS, Viktor VafeiadisMPI-SWS, Germany
Pre-print Media Attached File Attached