Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning (Extended Version)
Cormac Flanagan, Stephen N. Freund
TL;DR
Mover logic extends rely-guarantee reasoning by introducing atomic function specifications and reduction-based verification. It uses yield annotations to demarcate interference points and Lipton-style reduction to treat reducible blocks as atomic, enabling reusable, non-entangled postconditions for libraries and clients. The framework provides formal rules for atomic/non-atomic functions, defines mover specifications, and proves soundness via instrumented semantics and a reduction theorem. This approach aims to simplify and generalize verification of sophisticated concurrent code and to serve as a foundation for future reduction-based verifiers. It demonstrates modularity through concrete examples like spin locks and lock-free data structures and positions mover logic as a unifying theory for reduction-based concurrent verification tools.
Abstract
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.