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

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.

poster (popl2016-poster.pdf)93KiB

Fri 22 Jan
Times are displayed in time zone: (GMT-05:00) Guadalajara, Mexico City, Monterrey change

10:30 - 12:10: Research Papers - Track 2: Semantics and memory models at Grand Bay South
Chair(s): Alexey GotsmanIMDEA
POPL-2016-papers10:30 - 10:55
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
POPL-2016-papers10:55 - 11:20
Jean Pichon-PharabodUniversity of Cambridge, Peter SewellUniversity of Cambridge
File Attached
POPL-2016-papers11:20 - 11:45
John WickersonImperial College London, Mark BattyUniversity of Cambridge, Alastair DonaldsonImperial College London
Pre-print File Attached
POPL-2016-papers11:45 - 12:10
Ori LahavMPI-SWS, Nick GiannarakisMPI-SWS, Viktor VafeiadisMPI-SWS, Germany
Pre-print Media Attached File Attached