Commutativity Simplifies Proofs of Parameterized Programs
Why this work is in the frame
A frame that forgets how it found something cannot be audited. These are the routes that admitted this work.
Bibliographic record
Abstract
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 <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mi mathvariant="script">R</mml:mi> </mml:math> of a parameterized program <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mi mathvariant="script">P</mml:mi> </mml:math> is again a parameterized program (the thread template of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mi mathvariant="script">R</mml:mi> </mml:math> is obtained by source-to-source transformation of the thread template of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mi mathvariant="script">P</mml:mi> </mml:math> ). Consequently, existing techniques for the verification of parameterized programs can be directly applied to <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mi mathvariant="script">R</mml:mi> </mml:math> instead of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mi mathvariant="script">P</mml:mi> </mml:math> . 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.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
Full frame distilled prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. Learned from the 10,348 direct Codex labels and 10,348 direct Gemma labels. Candidate is the union of thresholded teacher heads; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels or direct frontier model labels.
Codex and Gemma teacher scores by category
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.001 | 0.002 |
| Meta-epidemiology (narrow) | 0.000 | 0.000 |
| Meta-epidemiology (broad) | 0.000 | 0.000 |
| Bibliometrics | 0.000 | 0.001 |
| Science and technology studies | 0.000 | 0.000 |
| Scholarly communication | 0.000 | 0.000 |
| Open science | 0.003 | 0.001 |
| Research integrity | 0.000 | 0.000 |
| Insufficient payload (model declined to judge) | 0.000 | 0.000 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from it