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.

翻译：非确定性使得并行程序的编写与推理颇具挑战。为避免这些挑战，研究者开发了内部确定性并行编程技术，其中并行计算的步骤以确定性的方式推进。内部确定性之所以有用，是因为它允许程序员像程序按顺序执行一样进行推理。然而，目前尚缺乏能够利用这一特性并简化内部确定性程序形式化推理的验证框架。为捕捉内部确定性程序应更易于推理的本质原因，本文定义了一种称为调度无关安全性的性质。若一个程序满足调度无关安全性，则要证明该程序在所有执行顺序下均安全，仅需证明其某一可终止执行是安全的即可。随后，我们提出了一种名为Musketeer的分离逻辑，用于证明程序满足调度无关安全性。一旦并行程序被证明满足调度无关安全性，我们便可使用一种称为Angelic的新逻辑对其进行验证，该逻辑允许动态选择并仅验证程序的单一顺序执行路径。借助Musketeer，我们证明了MiniDet（一种用于强制内部确定性的仿射类型系统）的可靠性。MiniDet支持研究文献中已识别的若干内部确定性编程核心算法原语，包括确定性版本的并发哈希集合。由于任何语法良类型的MiniDet程序均满足调度无关安全性，我们可以应用Angelic逻辑对此类程序进行验证。本文所有结果均已使用Iris分离逻辑框架在Rocq中完成形式化验证。