All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs

TL;DR

The paper addresses nondeterminism in parallel programs by advocating internal determinism and introducing schedule-independent safety, which reduces verification across all interleavings to a single terminating execution. It introduces Musketeer, a separation logic for proving schedule-independent safety, and Angelic, a logic to verify one safe interleaving, both mechanized in Rocq using Iris. It connects to an affine type system (MiniDet) and demonstrates soundness for determinism-preserving primitives like priority writes and a deterministic concurrent hash set, culminating in a deduplication example. Together, these contributions offer a cohesive framework for verifying determinism-based parallel programs and provide mechanized proofs that support real-world tooling. The work advances the state of hyperproperty reasoning by enabling forallforall verification through structured logics and embeddings into Iris-based frameworks, with practical implications for building reliable internally deterministic parallel software.

Abstract

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.

Theorems & Definitions (5)

• Theorem 4.1: Soundness of
• Theorem 5.1: Soundness of Chained Triples
• Theorem 6.1: Soundness of
• lemma 1: Soundness of
• lemma 2: Fundamental