Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Noam Zilberstein, Alexandra Silva, Joseph Tassarotti

TL;DR

pcOL addresses the challenge of formal reasoning about distributions of outcomes in probabilistic concurrent programs by integrating elements from CSL, PSL, and Demonic Outcome Logic into a measure-theoretic framework. It introduces outcome conjunctions and conditioning, two modes of separation (strong and weak), and an invariant-sensitive semantics built on Pomsets with Formulae to achieve compositional reasoning about both independence and inter-thread correlations. The framework supports unbounded loops with almost-sure termination, and demonstrates four case studies (Entropy Mixer, Concurrent Shuffle, PrivFetch, and the von Neumann Trick) to illustrate practical verification of randomized concurrent algorithms. This work establishes a foundation for rigorous, scalable verification of probabilistic concurrency with direct applications to synchronization protocols and distributed systems.

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.

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

TL;DR

pcOL addresses the challenge of formal reasoning about distributions of outcomes in probabilistic concurrent programs by integrating elements from CSL, PSL, and Demonic Outcome Logic into a measure-theoretic framework. It introduces outcome conjunctions and conditioning, two modes of separation (strong and weak), and an invariant-sensitive semantics built on Pomsets with Formulae to achieve compositional reasoning about both independence and inter-thread correlations. The framework supports unbounded loops with almost-sure termination, and demonstrates four case studies (Entropy Mixer, Concurrent Shuffle, PrivFetch, and the von Neumann Trick) to illustrate practical verification of randomized concurrent algorithms. This work establishes a foundation for rigorous, scalable verification of probabilistic concurrency with direct applications to synchronization protocols and distributed systems.

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.

Paper Structure

This paper contains 49 sections, 38 theorems, 130 equations, 12 figures.

Table of Contents

  1. Introduction
  2. Overview: Familiar Reasoning Principles in a New Setting
  3. Concurrent Separation Logic meets Probabilistic Separation Logic
  4. Handling Randomized Shared State with Outcome Logic
  5. Taming Nondeterminism with Precise Assertions
  6. Weak Separation and Case Analysis over Shared State
  7. A Probabilistic and Concurrent Programming Language
  8. Preliminaries: Memories and the Convex Powerset
  9. Actions and Invariants
  10. Semantics of Randomized Concurrent Programs
  11. The Model of Probabilistic Assertions
  12. Pure Assertions
  13. Measure Theory and Probability Spaces
  14. Probabilistic Assertions
  15. Convex and Precise Assertions and Entailment Laws
  16. ...and 34 more sections

Key Result

theorem 1

For all of the rules in fig:cmd-rulesfig:csl-rulesfig:structural-rulesfig:while-rule, if $I\vdash_m{\color{purple}\boldsymbol\langle} \varphi{\color{purple}\boldsymbol\rangle} ~C~ {\color{purple}\boldsymbol\langle} \psi{\color{purple}\boldsymbol\rangle}$ then $I\vDash_m{\color{purple}\boldsymbol\la

Figures (12)

  • Figure 1: Syntax of a probabilistic concurrent language, where $x\in\mathsf{Var}$, $v \in \mathsf{Val}$, and $\mathord{\asymp} \in \{ =, \le, <, \ldots \}$.
  • Figure 2: Satisfaction relation for pure assertions.
  • Figure 3: The satisfaction relation, where $\Gamma \colon \mathsf{LVar} \to\mathsf{Var}$ is a logical context and $\mathcal{P} = \langle \mathsf{Mem}[ S ], \mathcal{F}_\mathcal{P}, \mu_\mathcal{P} \rangle$ is a complete probability space. All the existentially quantified probability spaces are also complete.
  • Figure 4: Selected entailment laws, where $\varphi[E/X]$ denotes a syntactic substitution of $E$ for $X$ in $\varphi$. Recall that $m\in \{\mathsf{s}, \mathsf{w}\}$ and when $m$ is omitted, $\ast = \ast_\mathsf{s}$.
  • Figure 5: Rules for Sequential Commands
  • ...and 7 more figures

Theorems & Definitions (43)

  • definition 1: Precision
  • definition 2: Convex Assertions
  • definition 3: pcOL Triples
  • theorem 1: Soundness
  • lemma 1: Invariant Monotonicity
  • definition 4: Labelled Partial Order with Formulae (LPOFs)
  • definition 5: Pomsets with Formulae
  • lemma 2
  • lemma 3
  • lemma 4
  • ...and 33 more