一句话：用 Cosmo 并发分离逻辑在弱内存模型下形式化验证多生产者多消费者有界队列。
本文关注在 Multicore OCaml 弱内存模型下，如何对高级并发数据结构进行模块化、形式化的推理。作者使用现代并发分离逻辑 Cosmo，对多生产者多消费者（MPMC）有界并发队列的实现进行形式化规约与验证。方法上，他们结合逻辑原子三元组（logically atomic triples）与 Cosmo 的 views，在规约中精确刻画队列库与弱内存模型之间的交互。该工作被定位为一次演示与实验性验证，表明 Cosmo 能支持对高级并发数据结构的模块化形式推理；关键结果是完成该队列在弱内存模型设定下的验证，并展示上述机制在规约表达与模块化证明中的联合作用。
We use Cosmo, a modern concurrent separation logic, to formally specify and verify an implementation of a multiple-producer multiple-consumer concurrent queue in the setting of the Multicore OCaml weak memory model. We view this result as a demonstration and experimental verification of the manner in which Cosmo allows modular and formal reasoning about advanced concurrent data structures. In particular, we show how the joint use of logically atomic triples and of Cosmo's views makes it possible to describe precisely in the specification the interaction between the queue library and the weak memory model.
@article{paperbot1115,
title = {Formal verification of a concurrent bounded queue in a weak memory model},
author = {Glen Mével and Jacques-Henri Jourdan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473571}
}