HieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical Space Decomposition
Sirui Lu, Rastislav Bodík
Abstract
RASTISLAV BODÍK, Google DeepMind, USA Modern optimizing compilers generate efficient code but rarely achieve theoretical optimality, often necessitating manual fine-tuning. This is especially the case for processors with vector instructions, which can grow the instruction set by an order of magnitude. Super-optimizers can synthesize optimal code, but they face a fundamental scalability constraint: as the size of the instruction set increases, the length of the longest synthesizable program decreases rapidly.
To help super-optimizers deal with large instruction sets, we introduce HieraSynth, a parallel framework for super-optimization that decomposes the problem by hierarchically partitioning the space of candidate programs, effectively decreasing the instruction set size. It also prunes search branches when the solver proves unrealizability, and explores independent subspaces in parallel, achieving near-linear speedup. HieraSynth is sufficiently efficient to run to completeness even on many hard problems, which means that it exhaustively explores the program space. This ensures that the synthesized program is optimal according to a cost model.
We implement HieraSynth as a library and demonstrate its effectiveness with a RISC-V Vector superoptimizer capable of handling instruction sets with up to 700 instructions while synthesizing 7-8-instruction programs. This is a significant advancement over previous approaches that were limited to 1-3 instructions with similar instruction set sizes. Specifically, HieraSynth can handle instruction sets up to 10.66× larger for a given program size, or synthesize up to 4.75× larger programs for a fixed instruction set. Evaluations show that HieraSynth can synthesize code surpassing human-expert optimizations and significantly reduce synthesis time, making super-optimization more practical for modern vector architectures.
CCS Concepts: • Software and its engineering → Automatic programming.
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 18dcf84e-8a2c-4824-940b-6834bcd81353Builds on11
- egg: Fast and extensible equality saturationMax Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt et al.POPL 2021 · 170 citations
- DreamCoder: bootstrapping inductive program synthesis with wake-sleep library learningKevin Ellis, Catherine Wong, Maxwell I. Nye, Mathias Sablé-Meyer et al.PLDI 2021 · 97 citations
- Vectorization for digital signal processors via equality saturationAlexa VanHattum, Rachit Nigam, Vincent T. Lee, James Bornholt et al.ASPLOS 2021 · 57 citations
- Reconciling enumerative and deductive program synthesisKangjing Huang, Xiaokang Qiu, Peiyuan Shen, Yanjun WangPLDI 2020 · 46 citations
- Exact and approximate methods for proving unrealizability of syntax-guided synthesis problemsQinheping Hu, John Cyphert, Loris D'Antoni, Thomas W. RepsPLDI 2020 · 22 citations
Related papers
- SEER: Super-Optimization Explorer for High-Level Synthesis using E-graph RewritingJianyi Cheng, Samuel Coward, Lorenzo Chelini, Rafael Barbalho et al.ASPLOS 2024 · 18 citations
- Minotaur: A SIMD-Oriented Synthesizing SuperoptimizerZhengyang Liu, Stefan Mada, John RegehrOOPSLA 2024 · 9 citations
- Dataflow-based pruning for speeding up superoptimizationManasij Mukherjee, Pranav Kant, Zhengyang Liu, John RegehrOOPSLA 2020 · 21 citations
- All you need is superword-level parallelism: systematic control-flow vectorization with SLPYishen Chen, Charith Mendis, Saman P. AmarasinghePLDI 2022 · 20 citations
- Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector ManipulationsYuantian Ding, Xiaokang QiuPOPL 2024 · 10 citations
