A Separation Logic for a Promising Semantics
Programming Languages and Systems
MetadataShow full item record
Svendsen, K., Pichon-Pharabod, J., Doko, M., Lahav, O., & Vafeiadis, V. (2018). A Separation Logic for a Promising Semantics. Programming Languages and Systems, 357-384. https://doi.org/10.1007/978-3-319-89884-1_13
We 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.
The 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.
External DOI: https://doi.org/10.1007/978-3-319-89884-1_13
This record's URL: https://www.repository.cam.ac.uk/handle/1810/294709
Attribution 4.0 International
Licence URL: https://creativecommons.org/licenses/by/4.0/