Rely-guarantee (RG) logic uses thread interference specifications (relies and guarantees) to reason about the correctness of multithreaded software. Unfortunately, RG logic requires each function postcondition to be "stabilized" or specialized to the behavior of other threads, making it difficult to write function specifications that are reusable at multiple call sites. This paper presents mover logic, which extends RG logic to address this problem via the notion of atomic functions. Atomic functions behave as if they execute serially without interference from concurrent threads, and so they can be assigned more general and reusable specifications that avoid the stabilization requirement of RG logic. Several practical verifiers (Calvin-R, QED, CIVL, Armada, Anchor, etc.) have demonstrated the modularity benefits of atomic function specifications. However, the complexity of these systems and their correctness proofs makes it challenging to understand and extend these systems. Mover logic formalizes the central ideas reduction in a declarative program logic that may provide foundation for future work in this area.

翻译：依赖-保证（RG）逻辑通过线程干扰规约（依赖条件与保证条件）来推理多线程软件的正确性。然而，RG逻辑要求每个函数后验条件必须被“稳定化”或针对其他线程的行为进行特化，这使得编写可在多个调用点复用的函数规约变得困难。本文提出移动逻辑，它通过原子函数的概念扩展了RG逻辑以解决此问题。原子函数的行为如同在没有并发线程干扰的情况下串行执行，因此可以为其分配更通用且可复用的规约，从而避免RG逻辑的稳定化要求。多个实际验证器（Calvin-R、QED、CIVL、Armada、Anchor等）已证明了原子函数规约在模块化方面的优势。然而，这些系统及其正确性证明的复杂性使得理解和扩展这些系统具有挑战性。移动逻辑以声明式程序逻辑的形式将归约的核心思想形式化，可能为该领域的未来工作提供基础。