A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
Despite much research on concurrent programming languages, especially for Java and C/C++, we still do not have a satisfactory definition of their semantics, one that admits all common optimisations without also admitting undesired behaviour. Especially problematic are the ``thin-air'' examples involving high-performance concurrent accesses, such as C/C++11 relaxed atomics. The C/C++11 model is in a per-candidate-execution style, and previous work has identified a tension between that and the fact that compiler optimisations do not operate over single candidate executions in isolation; rather, they operate over syntactic representations that represent all executions.
In this paper we propose a novel approach that circumvents this difficulty. We define a concurrency semantics for a core calculus, including relaxed-atomic and non-atomic accesses and locks, that admits a wide range of optimisation while still forbidding the classic thin-air examples. It also addresses other problems relating to undefined behaviour.
The basic idea is to use an event-structure representation of the current state of each thread, capturing all of its potential executions, and to permit interleaving of execution and transformation steps over that to reflect optimisation (possibly dynamic) of the code. These are combined with a non-multi-copy-atomic storage subsystem, to reflect common hardware behaviour.
The semantics is defined in a mechanised and executable form, and designed to be implementable above current relaxed hardware and strong enough to support the programming idioms that C/C++11 does for this fragment. It offers a potential way forward for concurrent programming language semantics, beyond the current C/C++11 and Java models.
Fri 22 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
10:30 - 12:10
|Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA|
Shaked Flur University of Cambridge, Kathryn E. Gray University of Cambridge, Christopher Pulte University of Cambridge, Susmit Sarkar University of St Andrews, Luc Maranget INRIA Rocquencourt, Ali Sezgin University of Cambridge, Will Deacon ARM Ltd., Peter Sewell University of CambridgeMedia Attached File Attached
|A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions|
Research PapersFile Attached
|Overhauling SC atomics in C11 and OpenCL|
John Wickerson Imperial College London, Mark Batty University of Cambridge, Alastair F. Donaldson Imperial College LondonPre-print File Attached
|Taming Release-Acquire Consistency|
Research PapersPre-print Media Attached File Attached