Rely/Guarantee Reasoning for Multicopy Atomic Weak Memory Models

Rely/guarantee reasoning provides a compositional approach to reasoning about concurrent programs. However, such reasoning traditionally assumes a sequentially consistent memory model and hence is unsound on modern hardware in the presence of data races. In this paper, we present a rely/guarantee-based approach for multicopy atomic weak memory models, i.e., where a thread's stores become observable to all other threads at the same time. Such memory models include those of the widely used x86-TSO and ARMv8 processor architectures, as well as the open-source RISC-V architecture. In this context, an operational semantics can be based on thread-local instruction reordering. We exploit this to provide an efficient compositional proof technique in which weak memory behaviour can be shown to preserve rely/guarantee reasoning on a sequentially consistent memory model. To achieve this, we introduce a side-condition, reordering interference freedom, reducing the complexity of weak memory to checks over pairs of reorderable instructions. To enable practical application, we also define a dataflow analysis capable of identifying a thread's reorderable instructions. All aspects of our approach have been encoded and proved sound in Isabelle/HOL.