Show simple item record

dc.contributor.authorPichon-Pharabod, Jean
dc.contributor.authorSewell, Peter
dc.date.accessioned2018-11-20T00:31:00Z
dc.date.available2018-11-20T00:31:00Z
dc.date.issued2016-04-08
dc.identifier.issn1523-2867
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/285458
dc.description.abstractCopyright 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.
dc.description.sponsorshipThis work was partly funded by the EPSRC Programme Grant REMS: Rigorous Engineering for Mainstream Systems, EP/K008528/1
dc.publisherACM
dc.titleA concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
dc.typeArticle
prism.endingPage633
prism.issueIdentifier1
prism.publicationDate2016
prism.publicationNameACM SIGPLAN Notices
prism.startingPage622
prism.volume51
dc.identifier.doi10.17863/CAM.32816
dcterms.dateAccepted2016-01-01
rioxxterms.versionofrecord10.1145/2837614.2837616
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserved
rioxxterms.licenseref.startdate2016-04-08
dc.identifier.eissn1558-1160
rioxxterms.typeJournal Article/Review
pubs.funder-project-idEngineering and Physical Sciences Research Council (EP/K008528/1)
cam.issuedOnline2016-01
rioxxterms.freetoread.startdate2017-04-08


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record