License: Creative Commons Attribution 3.0 Germany license (CC BY 3.0 DE)
When quoting this document, please refer to the following
DOI: 10.4230/DARTS.3.2.15
URN: urn:nbn:de:0030-drops-72966
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7296/
Go back to Dagstuhl Artifacts Series

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

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

pdf-format:
DARTS-3-2-15.pdf (0.3 MB)

Abstract

This artifact provides the soundness proofs for the encodings in Iris the RSL and GPS logics, as well as the verification for all standard examples known to be verifiable in those logics. All of these proofs are formalized in Coq, which is the main content of this artifact. The formalization is provided in a virtual machine for the convenience of testing, but can also be built from source.

BibTeX - Entry

@Article{kaiser_et_al:DARTS:2017:7296,
  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 (Artifact)}},
  pages =	{15:1--15:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2017},
  volume =	{3},
  number =	{2},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7296},
  URN =		{urn:nbn:de:0030-drops-72966},
  doi =		{10.4230/DARTS.3.2.15},
  annote =	{Keywords: weak memory models, release-acquire, concurrency, separation logic}
}

Keywords: weak memory models, release-acquire, concurrency, separation logic
Collection: DARTS, Volume 3, Issue 2
Related Scholarly Article: http://dx.doi.org/10.4230/LIPIcs.ECOOP.2017.17
Issue Date: 2017
Date of publication: 20.06.2017

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