Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and(…)
summary
Introduces Probabilistic Concurrent Outcome Logic (pcOL) that composes concurrent separation logic, probabilistic separation logic, and Outcome Logic to prove exact joint distributions and conditional independence results for concurrent randomized programs; key technical constraint requires precise assertions on thread postconditions to guarantee independence, and a new measure-theoretic model (based on pum-sets-with-formula style semantics) supports almost sure termination and unbounded loops. Demonstrates a parallel shuffle proof that needs independence to succeed and a von Neumann–style protocol that still yields a fair coin despite adversarially changing bias.
AI-written summary · about
chapters (21)
- 0:00Introduction
- 0:22Research goals
- 1:05Core approach
- 1:47Parallel composition
- 3:13Probabilistic independence
- 3:55Shared state reasoning
- 4:58Challenges in independence
- 6:02Precision in assertions
- 7:48Extending rules
- 8:53Shared randomness case
- 10:21Conditional independence
- 11:22Meta theory
- 12:25Compositional properties
- 13:29Soundness theorems
- 14:55Concurrent shuffling
- 16:01Von Neumann trick
- 17:07Summary
- 17:49Future directions
- 18:33Q&A on other logics
- 19:15Q&A on parallel precision
- 20:47Q&A on validity conditions
related talks
01h 00mKeynote Talk: Outcome Logic: a foundational framework for concurrent and probabilistic(…)
21mContextual Refinement of Higher-Order Concurrent Probabilistic Programs
24mA Concurrent Program Logic with a Future and History
54mReasoning about Progress of Concurrent Objects
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
19mScenario-based Proofs for Concurrent Objects
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
01h 01mThe Future of Concurrency and Parallelism