Commutativity has been proved to be a powerful tool in reasoning about concurrent programs. Recent work has put forward the view that a commutativity-based \emph{reduction} of a program may admit simpler proofs than the program itself. Parametric lexicographical program reductions was introduced to formalize a broad class of reductions that would include classical notions (sequential reasoning, synchronous programs). Approaches based on this framework, however, were fundamentally limited to program models with a {\em fixed/bounded} 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 {\em parameterized programs}, i.e., for programs with an unbounded number of threads. A parametrized program $\mathcal{P}$ stands for an infinite family of programs $\mathcal{P}(n)$ with $n$ threads. Each thread runs an instance of the given thread template. We show that reductions are indeed useful for the the simplification of proofs of parameterized concurrent programs, in a sense that can be made precise: A reduction of a parameterized program may admit a proof which uses {\em fewer or less sophisticated ghost variables}. The reduction may therefore be within the reach of an automated verification technique (when the input parameterized program is not).
Our first technical contribution is that we introduce a notion of a reduction for a parameterized program. The reduction $\mathcal{R}$ of the parametrized program $\mathcal{P}$ is again a parameterized program which is represented by a single thread template. This means that existing techniques for verification of parameterized programs can now be directly applied to $\mathcal{R}$ instead of $\mathcal{P}$. Our second technical contribution is that we define an appropriate family of {\em pairwise preference orders} which can be effectively used as a parameter 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 one of the recently proposed frameworks for parameterized program verification. The results of our preliminary experiments on a representative set of examples are very encouraging.