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.

翻译：依赖-保证（RG）是一种极具影响力的并发程序组合式验证技术，其最初开发时假设了顺序一致性的共享内存。本文首先通过引入一个适用于任何由霍尔三元组公理化表征内存模型的RG框架，将RG推广为可参数化适应底层内存模型的通用形式。其次，我们针对因果一致性内存下的并发程序推理实例化该框架——该内存模型采用最近提出的基于势能的操作语义进行形式化，从而为此类语义提供了首个推理技术。我们提出的程序逻辑（称为Piccolo）采用了一种新颖的断言语言，允许规约每个线程可能达到的有序状态序列。我们通过多个litmus测试用例，以及针对因果一致性内存适配的Peterson互斥算法，验证了Piccolo的有效性。