Abstract
Deductive verification of concurrent programs under weak memory has thus far
been limited to simple programs over a monolithic state space. For scalability,
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 they use. 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.