  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.
