Commutativity has proven to be a powerful tool in reasoning about concurrent programs. Recent work has shown that a commutativity-based reduction of a program may admit simpler proofs than the program itself. The framework of lexicographical program reductions was introduced to formalize a broad class of reductions. Approaches based on this framework, however, were limited to program models with a fixed number of threads. In this paper, we show that it is possible to define an effective parametric family of program reductions that can be used to find simple proofs for parameterized programs, i.e., programs with an unbounded number of threads. We show that reductions are indeed useful for the simplification of proofs of parameterized programs, in a sense that can be made precise: A reduction of a parameterized program may admit a proof which uses fewer or less sophisticated ghost variables. The reduction may therefore be within reach of an automated verification technique, even when the original parameterized program is not. We introduce a notion of reductions for parameterized programs such that the reduction $\mathcal{R}$ of a parameterized program $\mathcal{P}$ is again a parameterized program (the thread template of $\mathcal{R}$ is obtained by source-to-source transformation of the thread template of $\mathcal{P}$). Consequently, existing techniques for the verification of parameterized programs can be directly applied to $\mathcal{R}$ instead of $\mathcal{P}$. We define an appropriate family of pairwise preference orders which can be used to produce different lexicographical reductions. To determine whether this theoretical foundation amounts to a usable solution in practice, we have implemented the approach, based on a recently proposed framework for parameterized program verification. The results of our preliminary experiments on a representative set of examples are encouraging.

翻译：可交换性已被证明是推理并发程序的有力工具。近期研究表明，基于可交换性的程序归约可能比原程序本身支持更简单的证明。词序程序归约框架的提出形式化了广泛的归约类别。然而，基于该框架的方法仅限于固定线程数的程序模型。本文证明，可以定义有效的参数化程序归约族，用于为参数化程序（即具有无界线程数的程序）寻找简单证明。我们揭示：归约确实有助于简化参数化程序的证明——这种简化可精确表述为：参数化程序的归约可能允许使用更少或更简单的幽灵变量进行证明。因此，即使原始参数化程序超出自动验证技术的能力范围，其归约也可能在自动验证技术可处理范围内。我们为参数化程序引入了归约概念，使得参数化程序$\mathcal{P}$的归约$\mathcal{R}$自身仍是参数化程序（$\mathcal{R}$的线程模板通过对$\mathcal{P}$的线程模板进行源到源变换获得）。因此，现有的参数化程序验证技术可直接应用于$\mathcal{R}$而非$\mathcal{P}$。我们定义了恰当的成对偏好序族，可用于生成不同的词序归约。为验证该理论基础在实际应用中的可行性，我们基于近期提出的参数化程序验证框架实现了该方法。在代表性示例集合上的初步实验结果令人鼓舞。