Show simple item record

dc.contributor.authorSvendsen, Kasperen
dc.contributor.authorPichon-Pharabod, Jeanen
dc.contributor.authorDoko, Markoen
dc.contributor.authorLahav, Orien
dc.contributor.authorVafeiadis, Viktoren
dc.date.accessioned2019-07-16T23:31:19Z
dc.date.available2019-07-16T23:31:19Z
dc.date.issued2018en
dc.identifier.isbn9783319898834en
dc.identifier.issn0302-9743
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/294709
dc.description.abstractWe present SLR, the first expressive program logic for reason- ing about concurrent programs under a weak memory model addressing the out-of-thin-air problem. Our logic includes the standard features from existing logics, such as RSL and GPS, that were previously known to be sound only under stronger memory models: (1) separation, (2) per-location invariants, and (3) ownership transfer via release-acquire synchronisation—as well as novel features for reasoning about (4) the absence of out-of-thin-air behaviours and (5) coherence. The logic is proved sound over the recent “promising” memory model of Kang et al., using a substantially different argument to soundness proofs of logics for simpler memory models.
dc.description.sponsorshipThe research was supported in part by the Danish Council for Independent Research (project DFF – 4181-00273), by a European Research Council Consolidator Grant for the project “RustBelt” (grant agreement no. 683289), and by Len Blavatnik and the Blavatnik Family foundation.
dc.publisherSpringer Link
dc.rightsAttribution 4.0 International
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/
dc.titleA Separation Logic for a Promising Semanticsen
dc.typeConference Object
prism.endingPage384
prism.publicationDate2018en
prism.publicationNameProgramming Languages and Systemsen
prism.startingPage357
dc.identifier.doi10.17863/CAM.41814
rioxxterms.versionofrecord10.1007/978-3-319-89884-1_13en
rioxxterms.versionVoR
rioxxterms.licenseref.urihttp://creativecommons.org/licenses/by/4.0/en
rioxxterms.licenseref.startdate2018en
dc.identifier.eissn1611-3349
rioxxterms.typeConference Paper/Proceeding/Abstracten
cam.issuedOnline2018-04-14en


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

Attribution 4.0 International
Except where otherwise noted, this item's licence is described as Attribution 4.0 International