Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version)
Abstract
Deductive verification techniques for C11 programs have advanced significantly in recent years with the development of operational semantics and associated logics for increasingly large fragments of C11. However, these semantics and logics have been developed in a restricted setting to avoid the thin-air-read problem. In this paper, we propose an operational semantics that leverages an intra-thread partial order (called semantic dependencies) induced by a recently developed denotational event-structure-based semantics. We prove that our operational semantics is sound and complete with respect to the denotational semantics. We present an associated logic that generalises a recent Owicki-Gries framework for RC11 (repaired C11), and demonstrate the use of this logic over several example proofs.
Keywords
Cite
@article{arxiv.2108.01418,
title = {Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version)},
author = {Daniel Wright and Mark Batty and Brijesh Dongol},
journal= {arXiv preprint arXiv:2108.01418},
year = {2021}
}
Comments
Extended version of the corresponding paper in FM2021