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)

Abstract

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
PublisherSpringer
Pages357-384
Number of pages28
ISBN (Electronic)9783319898841
ISBN (Print)9783319898834
DOIs
Publication statusPublished - 2018

Publication series

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

Fingerprint

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

Cite this