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.

翻译：基于Lipton移动子的交换性推理是一种验证并发程序的强大技术。其核心思想是定义一种程序变换，该变换在保持初始交错执行子集的同时，对可交换操作的重排序保持可靠性。将交换性推理扩展到软件系统中常规使用的特性（如过程和并行组合）仍然是一个重大挑战。本文提出了一种针对结构化并发程序的新型规约技术，该技术融合了两项关键进展。首先，我们提出了一种规约策略，能够可靠地将并行组合替换为顺序组合。其次，我们将Lipton规约推广至支持包含（可能递归的）过程调用的原子片段。关键在于，这两种基础策略可以任意组合，从而极大地拓展了基于规约的推理的适用范围和灵活性。我们在Civl中实现了该技术，并在多个具有挑战性的案例研究中验证了其有效性，包括快照对象、容错且可线性化的寄存器、FLASH缓存一致性协议以及一个非平凡的二阶段提交变体。