文章基本信息

标题：Owicki-Gries Reasoning for C11 RAR
本地全文：下载
作者：Sadegh Dalvandi ; Simon Doherty ; Brijesh Dongol 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：166
页码：1-26
DOI：10.4230/LIPIcs.ECOOP.2020.11
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：C11; Verification; Hoare logic; Owicki-Gries; Isabelle