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 of reduction in a declarative program logic that provides a foundation for future work in this area.

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