因果一致共享内存的依赖-保证推理（扩展版）
Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version)
AI总结：
本文提出Piccolo逻辑，用于因果一致内存下并发程序的推理，结合新的断言语言和潜在基于的操作语义，提供首个此类语义的推理技术。
摘要：
依赖-保证（RG）是一种高度有影响力的组合证明技术，最初假设顺序一致的共享内存。本文首先将RG推广为参数化于底层内存模型，引入适用于任何通过霍尔三元组公理化表征的模型的RG框架。其次，将此框架应用于因果一致内存下并发程序的推理，该内存模型通过最近提出的潜在基于的操作语义进行表征，从而提供首个此类语义的推理技术。所提出的程序逻辑称为Piccolo，采用新颖的断言语言，允许指定线程可能达到的有序状态序列。我们使用Piccolo进行多个litmus测试，以及将Peterson算法的互斥适应到因果一致内存。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
