2021/08/03 by Daniel Wright, Wright, Daniel, Mark Batty +3 · 1 citation
Computer Science · #Distributed systems and fault tolerance #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Programming Languages (cs.PL) #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.2108.01418
openalex publication_date 2021/08/03 · openalex created_date 2021/08/16 · openalex updated_date 2026/07/28
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.