Deductive Verification under the C11 Memory Model

Abstract: Owicki-Gries reasoning for concurrent programs uses Hoare logic together with an interference-freedom rule for concurrency. This talk describes a Hoare logic for a fragment of the C11 memory model that includes both relaxed and release-acquire accesses. Our logic features novel assertions on thread-specific views and a set of Hoare logic axioms that describe how these assertions are affected by atomic program steps. Our framework is such that the standard Owicki-Gries proof rules for compound statements, including non-interference remain unchanged. We demonstrate the utility of our framework 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 Isabelle/HOL. If time permits, I will discuss recent efforts to verify refinement under C11 and the verification of C11 library abstractions.

This is joint work with Sadegh Dalvandi, Simon Doherty, and Heike Wehrheim.

Bio: Brijesh Dongol is Senior Lecturer at the University of Surrey. He has a BSc in Computer Science and Mathematics and a BSc (Hons) in Logic and Computation, both from Victoria University of Wellington, New Zealand. In 2009, he received a PhD on formal derivations of concurrent algorithms at the University of Queensland, Australia. After this, he held postdoctorate positions at the University of Queensland and then at the University of Sheffield. He was a lecturer at Brunel University London (2014-18).