A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
View / Open Files
Authors
Pichon-Pharabod, Jean
Sewell, Peter
Publication Date
2016-04-08Journal Title
ACM SIGPLAN Notices
ISSN
1523-2867
Publisher
ACM
Volume
51
Issue
1
Pages
622-633
Type
Article
Metadata
Show full item recordCitation
Pichon-Pharabod, J., & Sewell, P. (2016). A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. ACM SIGPLAN Notices, 51 (1), 622-633. https://doi.org/10.1145/2837614.2837616
Abstract
Copyright is held by the owner/author(s). 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.
Sponsorship
This work was partly funded by the EPSRC Programme Grant REMS:
Rigorous Engineering for Mainstream Systems, EP/K008528/1
Funder references
Engineering and Physical Sciences Research Council (EP/K008528/1)
Identifiers
External DOI: https://doi.org/10.1145/2837614.2837616
This record's URL: https://www.repository.cam.ac.uk/handle/1810/285458
Rights
Licence:
http://www.rioxx.net/licenses/all-rights-reserved
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.