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.2020.11
URN: urn:nbn:de:0030-drops-131687
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13168/
Go to the corresponding LIPIcs Volume Portal

Dalvandi, Sadegh ; Doherty, Simon ; Dongol, Brijesh ; Wehrheim, Heike

Owicki-Gries Reasoning for C11 RAR

pdf-format:
LIPIcs-ECOOP-2020-11.pdf (0.8 MB)

Abstract

Owicki-Gries reasoning for concurrent programs uses Hoare logic together with an interference freedom rule for concurrency. In this paper, we develop a new proof calculus for the C11 RAR memory model (a fragment of C11 with both relaxed and release-acquire accesses) that allows all Owicki-Gries proof rules for compound statements, including non-interference, to remain unchanged. Our proof method features novel assertions specifying thread-specific views on the state of programs. This is combined with a set of Hoare logic rules that describe how these assertions are affected by atomic program steps. We demonstrate the utility of our proof calculus by verifying a number of standard C11 litmus tests and Peterson’s algorithm adapted for C11. Our proof calculus and its application to program verification have been fully mechanised in the theorem prover Isabelle.

BibTeX - Entry

@InProceedings{dalvandi_et_al:LIPIcs:2020:13168,
  author =	{Sadegh Dalvandi and Simon Doherty and Brijesh Dongol and Heike Wehrheim},
  title =	{{Owicki-Gries Reasoning for C11 RAR}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{11:1--11:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Robert Hirschfeld and Tobias Pape},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13168},
  URN =		{urn:nbn:de:0030-drops-131687},
  doi =		{10.4230/LIPIcs.ECOOP.2020.11},
  annote =	{Keywords: C11, Verification, Hoare logic, Owicki-Gries, Isabelle}
}

Keywords: C11, Verification, Hoare logic, Owicki-Gries, Isabelle
Collection: 34th European Conference on Object-Oriented Programming (ECOOP 2020)
Issue Date: 2020
Date of publication: 06.11.2020
Supplementary Material: ECOOP 2020 Artifact Evaluation approved artifact available at https://doi.org/10.4230/DARTS.6.2.15.

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