一句话：提出参数化程序的交换性归约族，使归约后的程序可用更简单的幽灵变量证明，从而更易自动验证。
交换性归约已被证明是并发程序推理的有力工具，近期工作表明基于交换性的程序归约可能比原程序更容易证明。然而，字典序程序归约框架虽然统一了顺序（线程局部）推理与同步程序，却本质上局限于线程数固定或有界的程序模型。本文研究线程数无界的参数化程序，定义了一类有效的参数化程序归约族，并精确说明其简化证明的意义：参数化程序的归约可能允许使用更少或更不复杂的幽灵变量完成证明，因此即使原程序超出自动验证能力，其归约也可能可被自动验证。技术贡献有二：一是引入参数化程序归约概念，保证归约R仍是参数化程序（R的线程模板由P的线程模板经源到源变换得到），从而可直接复用现有参数化程序验证技术；二是定义合适的成对偏好序族，作为参数有效生成不同的字典序归约。作者在已有的参数化程序验证框架上实现了该方法，并在代表性例子集上进行了初步实验，结果令人鼓舞。
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 which accommodate sequential (thread-local) reasoning as well as synchronous programs. Approaches based on this framework, however, were fundamentally limited to program models with a 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 parameterized programs , i.e., for programs with an unbounded number of threads. We show that reductions are indeed useful for the simplification of proofs for 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. As our first technical contribution, we introduce a notion of reductions for parameterized programs such that the reduction R of a parameterized program P is again a parameterized program (the thread template of R is obtained by source-to-source transformation of the thread template of P ). Consequently, existing techniques for the verification of parameterized programs can be directly applied to R instead of P . Our second technical contribution is that we define an appropriate family of 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 a recently proposed framework for parameterized program verification. The results of our preliminary experiments on a representative set of examples are encouraging.
@article{paperbot2581,
title = {Commutativity Simplifies Proofs of Parameterized Programs},
author = {Azadeh Farzan and Dominik Klumpp and Andreas Podelski},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632925}
}