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.