Verifying C11-Style Weak Memory Libraries

TL;DR

This paper presents a modular verification framework for C11-style weak memory libraries, enabling scalable and precise reasoning about concurrent programs under relaxed memory models, with formal proofs mechanized in Isabelle/HOL.

Contribution

It introduces a novel framework for specifying and verifying abstract memory objects in RC11 RAR, integrating operational semantics and refinement techniques for modular verification.

Findings

Framework precisely characterizes observability guarantees.

Verification of client programs with abstract method calls.

Mechanized proofs in Isabelle/HOL confirm correctness.

Abstract

Deductive verification of concurrent programs under weak memory has thus far been limited to simple programs over a monolithic state space. For scalabiility, we also require modular techniques with verifiable library abstractions. This paper addresses this challenge in the context of RC11 RAR, a subset of the C11 memory model that admits relaxed and release-acquire accesses, but disallows, so called, load-buffering cycles. We develop a simple framework for specifying abstract objects that precisely characterises the observability guarantees of abstract method calls. We show how this framework can be integrated with an operational semantics that enables verification of client programs that execute abstract method calls from a library it uses. Finally, we show how implementations of such abstractions in RC11 RAR can be verified by developing a (contextual) refinement framework for abstract objects. Our framework, including the operational semantics, verification technique for client-library programs, and simulation between abstract libraries and their implementations, has been mechanised in Isabelle/HOL.