Repository logo
 

A Separation Logic for a Promising Semantics

Published version
Peer-reviewed

Type

Conference Object

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

Volume Title

Publisher

Springer International Publishing
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.