A Separation Logic for a Promising Semantics

Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)peer-review

24 Citations (Scopus)


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.
Original languageEnglish
Title of host publicationProgramming Languages and Systems. ESOP 2018
EditorsAmal Ahmed
Number of pages28
ISBN (Electronic)9783319898841
ISBN (Print)9783319898834
Publication statusPublished - 2018

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'A Separation Logic for a Promising Semantics'. Together they form a unique fingerprint.

Cite this