A Separation Logic for a Promising Semantics
Published version
Peer-reviewed
Repository URI
Repository DOI
Change log
Authors
Svendsen, Kasper
Pichon-Pharabod, Jean
Doko, Marko
Lahav, Ori
Vafeiadis, Viktor
Abstract
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.
Description
Keywords
46 Information and Computing Sciences, 4602 Artificial Intelligence
Journal Title
LNCS 10801
Conference Name
27th European Symposium on Programming (ESOP), Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece
Journal ISSN
0302-9743
1611-3349
1611-3349
Volume Title
Publisher
Springer International Publishing
Publisher DOI
Sponsorship
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.