Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version)

TL;DR

This work tackles verification of concurrent programs under weak, causally consistent memory by generalizing the Rely-Guarantee (RG) framework to be parametric in memory models axiomatized with Hoare triples. It then instantiates RG for Strong Release-Acquire (SRA) using a potential-based semantics that tracks per-thread sequences of observed stores and introduces Piccolo, an interval-like assertion language, for Hoare-style reasoning about these sequences. The authors define memory triples for primitive commands, prove soundness of the RG rules in this setting, and demonstrate the approach on litmus tests and an adaptation of Peterson's mutual exclusion. They also formalize an equivalence between their SRA-based semantics and the operational SRA model (opSRA) in Coq, and discuss automation prospects and connections to related RG formalisms. Overall, Piccolo provides a tractable, compositional method for reasoning about causally consistent shared memory with potential for future automation and broader memory-model instantiations.

Abstract

Rely-guarantee (RG) is a highly influential compositional proof technique for concurrent programs, which was originally developed assuming a sequentially consistent shared memory. In this paper, we first generalize RG to make it parametric with respect to the underlying memory model by introducing an RG framework that is applicable to any model axiomatically characterized by Hoare triples. Second, we instantiate this framework for reasoning about concurrent programs under causally consistent memory, which is formulated using a recently proposed potential-based operational semantics, thereby providing the first reasoning technique for such semantics. The proposed program logic, which we call Piccolo, employs a novel assertion language allowing one to specify ordered sequences of states that each thread may reach. We employ Piccolo for multiple litmus tests, as well as for an adaptation of Peterson's algorithm for mutual exclusion to causally consistent memory.

Figures (6)

• Figure 1: Message passing in SC
• Figure 2: Message passing in SRA
• Figure 3: Program syntax
• Figure 4: Small-step semantics of (instrumented) primitive commands ($\tilde{c} \gg {\gamma} \mathrel{\raisebox{-0.8pt}{$\xrightarrow{{l}_\varepsilon}$}} {\gamma}'$)
• Figure 5: Small-step semantics of commands (${\langle{C,{\gamma}}\rangle} \mathrel{\raisebox{-0.8pt}{$\xrightarrow{{l}_\varepsilon}$}} {\langle{C',{\gamma}'}\rangle}$)

Theorems & Definitions (5)

• remark thmcounterremark
• remark thmcounterremark
• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition