Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reduction for Structured Concurrent Programs

Namratha Gangamreddypalli, Constantin Enea, Shaz Qadeer

TL;DR

The paper addresses scalable verification of structured concurrent programs by combining Lipton-style movers with a parallel-to-sequential reduction that supports atomic sections containing recursive procedures. It introduces RedPL and a refinement-based soundness theorem showing that well-typed, atomic-free programs can be reduced via par-reduce to an intermediate form and then via seq-reduce to a final form, with a refinement chain $\mathcal{P}_s \preccurlyeq \mathcal{P}_i \preccurlyeq \mathcal{P}_r$; mover types $\{\mathbf{B},\mathbf{R},\mathbf{L},\mathbf{N},\top\}$ and weak preconditions $\text{wlp}$ underpin correctness. The approach leverages abstractions such as $read_f$ (right mover) and $read_s$ (left mover) to over-approximate action effects, enabling reductions that avoid prophecy variables in linearizability proofs and support structured code with procedures. Implemented as an extension to Civl, the framework is validated on challenging case studies (e.g., a concurrent snapshot, ABD register, FLASH cache coherence, and 2PC), demonstrating scalable proofs and broader applicability to real-world concurrent and distributed protocols.

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.

Reduction for Structured Concurrent Programs

TL;DR

The paper addresses scalable verification of structured concurrent programs by combining Lipton-style movers with a parallel-to-sequential reduction that supports atomic sections containing recursive procedures. It introduces RedPL and a refinement-based soundness theorem showing that well-typed, atomic-free programs can be reduced via par-reduce to an intermediate form and then via seq-reduce to a final form, with a refinement chain ; mover types and weak preconditions underpin correctness. The approach leverages abstractions such as (right mover) and (left mover) to over-approximate action effects, enabling reductions that avoid prophecy variables in linearizability proofs and support structured code with procedures. Implemented as an extension to Civl, the framework is validated on challenging case studies (e.g., a concurrent snapshot, ABD register, FLASH cache coherence, and 2PC), demonstrating scalable proofs and broader applicability to real-world concurrent and distributed protocols.

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.
Paper Structure (24 sections, 7 theorems, 25 equations, 17 figures)

This paper contains 24 sections, 7 theorems, 25 equations, 17 figures.

Table of Contents

  1. Introduction
  2. Overview
  3. A Concurrent Snapshot Object
  4. Using Abstraction to Enable Reduction
  5. Reducing Parallel Statements
  6. The Unbounded Memory Case: Reductions for Structured Code
  7. RedPL: Syntax and Semantics
  8. Semantics
  9. Commutativity of Atomic Actions
  10. Types for Reduction
  11. Failure typing for statements
  12. Mover typing for statements
  13. Well-typed programs
  14. Reduction for RedPL Programs
  15. Implementation
  16. ...and 9 more sections

Key Result

theorem thmcountertheorem

Let $\mathcal{P}_s$ be an atomic-free and well-typed program. Let Then, the programs $\mathcal{P}_i$ and $\mathcal{P}_r$ are well-typed. Furthermore, if $\mathcal{P}_i$ is terminating, then: (1) $\mathcal{P}_s \preccurlyeq \mathcal{P}_i$, and (2) $\mathcal{P}_i \preccurlyeq \mathcal{P}_r$. Therefore, $\mathcal{P}_s \preccurlyeq \mathcal{P}_r$.

Figures (17)

  • Figure 1: A snapshot object. The scan procedure carries out two consecutive collects, meaning it reads the entire memory in parallel twice. If both collects yield identical results, the procedure returns. Otherwise, it restarts.
  • Figure 2: An abstraction scan. Compared to the original, the two memory reads call the abstracted actions read_f and read_s, resp. In these actions, $*$ is non-deterministic choice and local variables are initially assigned arbitrary values. The annotations seq-reduce and par-reduce are related to our reduction technique.
  • Figure 3: A reduced loop iteration.
  • Figure 4: Applying reduction on an abstraction of the scan procedure for an unbounded size memory.
  • Figure 5: RedPL: Syntax
  • ...and 12 more figures

Theorems & Definitions (13)

  • theorem thmcountertheorem
  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • ...and 3 more