Sciweavers

POPL
2016
ACM

A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions

7 years 11 months ago
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 problem...
Jean Pichon-Pharabod, Peter Sewell
Added 09 Apr 2016
Updated 09 Apr 2016
Type Journal
Year 2016
Where POPL
Authors Jean Pichon-Pharabod, Peter Sewell
Comments (0)