Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version)

TL;DR

This paper introduces an operational semantics for C11 programs using intra-thread partial orders, extending Owicki-Gries reasoning to handle relaxed dependencies and proving its soundness and completeness.

Contribution

It develops a new operational semantics based on semantic dependencies and extends Owicki-Gries logic for relaxed C11 programs, addressing previous limitations.

Findings

Proves the soundness and completeness of the semantics

Demonstrates the logic on several example proofs

Extends reasoning techniques for relaxed C11 programs

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.