Reduction for Structured Concurrent Programs
January 2026
To appear at ESOP 2026
Authors: Namratha Gangamreddypalli, Constantin Enea, Shaz Qadeer
Abstract. Commutativity reasoning based on Lipton's movers is a powerful technique for verification of concurrent programs. The idea is to define a program transformation that preserves a subset of the initial set of interleavings, which is sound modulo reorderings of commutative actions. Scaling commutativity reasoning to routinely-used features in software systems, such as procedures and parallel composition, remains a significant challenge. In this work, we introduce a novel reduction technique for structured concurrent programs that unifies two key advances:
  • We present a reduction strategy that soundly replaces parallel composition with sequential composition.
  • We generalize Lipton’s reduction to support atomic sections containing (potentially recursive) procedure calls.
Crucially, these two foundational strategies can be composed arbitrarily, greatly expanding the scope and flexibility of reduction-based reasoning. We implemented this technique in Civl and demonstrated its effectiveness on a number of challenging case studies, including a snapshot object, a fault-tolerant and linearizable register, the FLASH cache coherence protocol, and a non-trivial variant of Two-Phase Commit.
arXiv PDF DOI