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

TL;DR

This paper introduces a formal verification framework for internally deterministic parallel programs, enabling simpler reasoning and verification by exploiting schedule-independent safety and specialized logics.

Contribution

It develops Musketeer and Angelic logics for verifying schedule-independent safety in internally deterministic programs, and proves the soundness of an affine type system enforcing internal determinism.

Findings

Musketeer proves schedule-independent safety for parallel programs.

Angelic logic verifies a single sequential execution suffices for safety.

MiniDet enforces internal determinism with a verified affine type system.

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.