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.

翻译：Rely-guarantee（RG）是一种对并发程序极具影响力的组合式证明技术，最初基于顺序一致性共享内存假设而提出。本文首先通过引入一个可公理化地通过Hoare三元组刻画任何内存模型的RG框架，将RG泛化为相对于底层内存模型的参数化形式。其次，我们实例化该框架以在因果一致性内存下推理并发程序，该内存模型采用最近提出的基于势的操作语义进行形式化，从而为这类语义提供了首个推理技术。所提出的程序逻辑——我们称之为Piccolo——采用了一种新颖的断言语言，能够指定每个线程可能到达的有序状态序列。我们将Piccolo应用于多个石蕊测试，以及Peterson互斥算法在因果一致性内存下的适应性改编。