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.

翻译：尽管随机化在分布式计算中应用已久，但用于推理概率并发程序的形��方法发展相对滞后。现有的程序逻辑均无法表达同时具备概率性与并发性的程序所产生结果的完整分布规范。为此，我们引入了概率并发结果逻辑（pcOL），该逻辑将并发与概率分离逻辑的思想融入结果逻辑，从而提出新的组合推理原理。pcOL的核心在于将并发分离逻辑的规则重新诠释于以分离建模概率独立性的框架中，从而组合式地描述并发线程中变量的联合分布。结果推理也被证明至关重要，因为对依赖随机化共享状态的线程进行精确信息推导常需借助案例分析。我们通过一系列示例展示了pcOL的应用，包括证明无界循环的几乎必然终止性。