Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants

Abstract

Although randomization has long been used in distributed computing, formal methods for reasoning about probabilistic concurrent programs have lagged behind. No existing program logics can express specifications about the full distributions of outcomes resulting from programs that are both probabilistic and concurrent. To address this, we introduce Probabilistic Concurrent Outcome Logic (pcOL), which incorporates ideas from concurrent and probabilistic separation logics into Outcome Logic to introduce new compositional reasoning principles. At its core, pcOL reinterprets the rules of Concurrent Separation Logic in a setting where separation models probabilistic independence, so as to compositionally describe joint distributions over variables in concurrent threads. Reasoning about outcomes also proves crucial, as case analysis is often necessary to derive precise information about threads that rely on randomized shared state. We demonstrate pcOL on a variety of examples, including to prove almost sure termination of unbounded loops.

References in corpus (14)

• The Lean mathematical library
• Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Programs
• Mixed powerdomains for probability and nondeterminism
• Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
• A Separation Logic for Concurrent Randomized Programs
• A Probabilistic Separation Logic
• Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
• A Separation Logic for Negative Dependence
• Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
• Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
• A Demonic Outcome Logic for Randomized Nondeterminism
• Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
• Almost-Sure Termination by Guarded Refinement
• Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects