一句话：提出利用内部确定性简化并行程序验证的程序逻辑，并在 Rocq/Iris 中机器化验证。
并行程序中的非确定性使其难以编写与形式推理。内部确定性并行编程通过让并行计算按确定性顺序推进，使程序员能像顺序程序一样推理，但此前缺少利用该性质的验证框架。本文定义 schedule-independent safety：若只需证明程序的某一个终止执行安全，即可推出其在所有调度下安全。为证明该性质，作者提出分离逻辑 Musketeer；对满足该性质的程序，又提出 Angelic 逻辑，可动态选择一个顺序化执行进行验证。随后用 Musketeer 证明仿射类型系统 MiniDet 的可靠性，MiniDet 支持确定性并发哈希集合等核心内部确定性原语。所有结果均在 Rocq 的 Iris 框架中机器化验证。
Nondeterminism makes parallel programs challenging to write and reason about. To avoid these challenges, researchers have developed techniques for internally deterministic parallel programming, in which the steps of a parallel computation proceed in a deterministic way. Internal determinism is useful because it lets a programmer reason about a program as if it executed in a sequential order. However, no verification framework exists to exploit this property and simplify formal reasoning about internally deterministic programs. To capture the essence of why internally deterministic programs should be easier to reason about, this paper defines a property called schedule-independent safety. A program satisfies schedule-independent safety, if, to show that the program is safe across all orderings, it suffices to show that one terminating execution of the program is safe. We then present a separation logic called Musketeer for proving that a program satisfies schedule-independent safety. Once a parallel program has been shown to satisfy schedule-independent safety, we can verify it with a new logic called Angelic, which allows one to dynamically select and verify just one sequential ordering of the program. Using Musketeer, we prove the soundness of MiniDet, an affine type system for enforcing internal determinism. MiniDet supports several core algorithmic primitives for internally deterministic programming that have been identified in the research literature, including a deterministic version of a concurrent hash set. Because any syntactically well-typed MiniDet program satisfies schedule-independent safety, we can apply Angelic to verify such programs. All results in this paper have been verified in Rocq using the Iris separation logic framework.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{MoineWT26,
title = {All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs},
author = {Alexandre Moine and Sam Westrick and Joseph Tassarotti},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776668}
}