Maximal Simplification of Polyhedral Reductions
Louis Narmour, Tomofumi Yuki, Sanjay V. Rajopadhye
Abstract
Reductions combine collections of input values with an associative and often commutative operator to produce collections of results. When the same input value contributes to multiple outputs, there is an opportunity to reuse partial results, enabling reduction simplification . Simplification often produces a program with lower asymptotic complexity. Typical compiler optimizations yield, at best, a constant fold speedup, but a complexity improvement from, say, cubic to quadratic complexity yields unbounded speedup for sufficiently large problems. It is well known that reductions in polyhedral programs may be simplified automatically , but previous methods cannot exploit all available reuse. This paper resolves this long-standing open problem, thereby attaining minimal asymptotic complexity in the simplified program. We propose extensions to prior work on simplification to support any independent commutative reduction. At the heart of our approach is piece-wise simplification, the notion that we can split an arbitrary reduction into pieces and then independently simplify each piece. However, the difficulty of using such piece-wise transformations is that they typically involve an infinite number of choices. We give constructive proofs to deal with this and select a finite number of pieces for simplification.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 25c4ffdd-d9c9-498f-8286-0889480b7e7cBuilds on2
Related papers
- Reductions for safety proofsAzadeh Farzan, Anthony VandikasPOPL 2020 · 21 citations
- Commutativity Simplifies Proofs of Parameterized ProgramsAzadeh Farzan, Dominik Klumpp, Andreas PodelskiPOPL 2024 · 11 citations
- Type Batched Program ReductionGolnaz Gharachorlu, Nick SumnerISSTA 2023 · 1 citation
- Reverse engineering for reduction parallelization via semiring polynomialsAkimasa Morihata, Shigeyuki SatoPLDI 2021 · 3 citations
- Stratified Commutativity in Verification Algorithms for Concurrent ProgramsAzadeh Farzan, Dominik Klumpp, Andreas PodelskiPOPL 2023 · 11 citations
