TY - CHAP
T1 - A Separation Logic for a Promising Semantics
AU - Svendsen, Kasper
AU - Pichon-Pharabod, Jean
AU - Doko, Marko
AU - Lahav, Ori
AU - Vafeiadis, Viktor
PY - 2018
Y1 - 2018
N2 - We present SLR, the first expressive program logic for reasoning 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.
AB - We present SLR, the first expressive program logic for reasoning 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.
U2 - 10.1007/978-3-319-89884-1_13
DO - 10.1007/978-3-319-89884-1_13
M3 - Chapter (peer-reviewed)
SN - 9783319898834
T3 - Lecture Notes in Computer Science
SP - 357
EP - 384
BT - Programming Languages and Systems. ESOP 2018
A2 - Ahmed, Amal
PB - Springer
ER -