Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning
This program is tentative and subject to change.
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 avoids 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 RG logic and atomic functions in a declarative program logic that provides a rigorous and accessible logical foundation for future work.
This program is tentative and subject to change.
Wed 18 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00 | |||
13:30 15mTalk | A Dynamic Logic for Symbolic Execution for the Smart Contract Programming Language Michelson Technical Papers Barnabas Arvay University of Freiburg, Thi Thu Ha Doan University of Freiburg, Peter Thiemann University of Freiburg, Germany | ||
13:45 15mTalk | Qafny: A Quantum-Program Verifier Technical Papers Liyi Li Iowa State University, Mingwei Zhu University of Maryland, College Park, Rance Cleaveland University of Maryland, Alexander Nicolellis Iowa State University, Yi Lee University of Maryland, College Park, Le Chang University of Maryland, College Park, Xiaodi Wu University of Maryland | ||
14:00 15mTalk | Verifying Lock-free Search Structure Templates Technical Papers Nisarg Patel New York University, Dennis Shasha New York University, Thomas Wies New York University | ||
14:15 15mTalk | Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning Technical Papers | ||
14:30 15mTalk | Compositional Symbolic Execution for Correctness and Incorrectness Reasoning Technical Papers Andreas Lööw Imperial College London, Daniele Nantes-Sobrinho Imperial College London, Sacha-Élie Ayoun Imperial College London, Caroline Cronjäger Ruhr-Universität Bochum, Petar Maksimović Imperial College London, UK, Philippa Gardner Imperial College London | ||
14:45 15mTalk | Tenspiler: A Verified Lifting-Based Compiler for Tensor Operations Technical Papers Jie Qiu Duolingo, Colin Cai University of California, Berkeley, Sahil Bhatia University of California, Berkeley, Niranjan Hasabnis Intel Labs, Sanjit Seshia UC Berkeley, Alvin Cheung University of California at Berkeley |