A Separation Logic for Concurrent Randomized Programs

TL;DR

Polaris is a novel concurrent separation logic that enables probabilistic reasoning about randomized concurrent programs, verified through mechanized proofs of complex algorithms.

Contribution

It extends separation logic with probabilistic coupling techniques to handle both probabilistic and non-deterministic choices in concurrent programs.

Findings

Verified a randomized concurrent counter algorithm

Verified a two-level concurrent skip list

Mechanized proofs in Coq

Abstract

We present Polaris, a concurrent separation logic with support for probabilistic reasoning. As part of our logic, we extend the idea of coupling, which underlies recent work on probabilistic relational logics, to the setting of programs with both probabilistic and non-deterministic choice. To demonstrate Polaris, we verify a variant of a randomized concurrent counter algorithm and a two-level concurrent skip list. All of our results have been mechanized in Coq.