一句话：提出支持概率推理的并发分离逻辑 Polaris，并机器化验证随机化并发计数器与跳表。
并发随机化程序兼具概率选择与非确定选择，给模块化验证带来挑战。本文提出 Polaris：一种支持概率推理的并发分离逻辑。其核心是把概率关系逻辑中的 coupling 思想推广到同时包含概率和非确定选择的程序，从而在分离逻辑框架下推理随机化并发代码。作者用该逻辑验证了一个随机化并发计数器变体和一个两级并发跳表，并在 Coq 中机器化验证了全部结果，表明该逻辑可处理实际并发随机算法。
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.
@article{paperbot659,
title = {A separation logic for concurrent randomized programs},
author = {Joseph Tassarotti and Robert Harper},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290377}
}