Reduction for Structured Concurrent Programs

TL;DR

This paper introduces a novel reduction technique for structured concurrent programs that simplifies verification by replacing parallel composition with sequential, supporting recursive procedures, and is validated on complex case studies.

Contribution

It unifies two key reduction strategies, enabling sound simplification of concurrent programs with procedures and atomic sections, expanding the scope of commutativity reasoning.

Findings

Effective reduction in complex case studies

Supports recursive procedures and atomic sections

Implemented in Civl for practical verification

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. First, we present a reduction strategy that soundly replaces parallel composition with sequential composition. Second, 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.