License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2017.17
URN: urn:nbn:de:0030-drops-72753
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7275/
Go to the corresponding LIPIcs Volume Portal

Kaiser, Jan-Oliver ; Dang, Hoang-Hai ; Dreyer, Derek ; Lahav, Ori ; Vafeiadis, Viktor

Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris

pdf-format:
LIPIcs-ECOOP-2017-17.pdf (0.8 MB)

Abstract

The field of concurrent separation logics (CSLs) has recently
undergone two exciting developments: (1) the Iris framework for
encoding and unifying advanced higher-order CSLs and formalizing them in Coq, and (2) the adaptation of CSLs to account for weak memory models, notably C11's release-acquire (RA) consistency.
Unfortunately, these developments are seemingly incompatible, since
Iris only applies to languages with an operational interleaving
semantics, while C11 is defined by a declarative (axiomatic)
semantics. In this paper, we show that, on the contrary, it is not
only feasible but useful to marry these developments together. Our
first step is to provide a novel operational characterization of
RA+NA, the fragment of C11 containing RA accesses and "non-atomic"
(normal data) accesses. Instantiating Iris with this semantics, we
then derive higher-order variants of two prominent RA+NA logics, GPS
and RSL. Finally, we deploy these derived logics in order to perform
the first mechanical verifications (in Coq) of several interesting
case studies of RA+NA programming. In a nutshell, we provide the
first foundationally verified framework for proving programs correct
under C11's weak-memory semantics.

BibTeX - Entry

@InProceedings{kaiser_et_al:LIPIcs:2017:7275,
  author =	{Jan-Oliver Kaiser and Hoang-Hai Dang and Derek Dreyer and Ori Lahav and Viktor Vafeiadis},
  title =	{{Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{17:1--17:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{Peter M{\"u}ller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7275},
  URN =		{urn:nbn:de:0030-drops-72753},
  doi =		{10.4230/LIPIcs.ECOOP.2017.17},
  annote =	{Keywords: Weak memory models, release-acquire, concurrency, separation logic}
}

Keywords: Weak memory models, release-acquire, concurrency, separation logic
Collection: 31st European Conference on Object-Oriented Programming (ECOOP 2017)
Issue Date: 2017
Date of publication: 16.06.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI