Minotaur: A SIMD-Oriented Synthesizing Superoptimizer
Zhengyang Liu, Stefan Mada, John Regehr
Abstract
A superoptimizing compiler—one that performs a meaningful search of the program space as part of the optimization process—can find optimization opportunities that are missed by even the best existing optimizing compilers. We created Minotaur: a superoptimizer for LLVM that uses program synthesis to improve its code generation, focusing on integer and floating-point SIMD code. On an Intel Cascade Lake processor, Minotaur achieves an average speedup of 7.3% on the GNU Multiple Precision library (GMP)’s benchmark suite, with a maximum speedup of 13%. On SPEC CPU 2017, our superoptimizer produces an average speedup of 1.5%, with a maximum speedup of 4.5% for 638.imagick. Every optimization produced by Minotaur has been formally verified, and several optimizations that it has discovered have been implemented in LLVM as a result of our work.
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 45dd9452-802e-4bfc-97e5-f65e2a80642cCited by top-tier papers9
- Optimizing Quantum Circuits, Fast and SlowAmanda Xu, Abtin Molavi, Swamit Tannu, Aws AlbarghouthiASPLOS 2025 · 8 citations
- Hydride: A Retargetable and Extensible Synthesis-based Compiler for Modern Hardware ArchitecturesAkash Kothari, Abdul Rafae Noor, Muchen Xu, Hassam Uddin et al.ASPLOS 2024 · 8 citations
- TensorRight: Automated Verification of Tensor Graph RewritesJai Arora, Sirui Lu, Devansh Jain, Tianfan Xu et al.POPL 2025 · 6 citations
- Exploiting Undefined Behavior in C/C++ Programs for Optimization: A Study on the Performance ImpactLucian Popescu, Nuno P. LopesPLDI 2025 · 2 citations
- LPO: Discovering Missed Peephole Optimizations with Large Language ModelsZhenyang Xu, Hongxu Xu, Yongqiang Tian, Xintong Zhou et al.ASPLOS 2026 · 1 citation
Builds on4
- Alive2: bounded translation validation for LLVMNuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu et al.PLDI 2021 · 109 citations
- Vectorization for digital signal processors via equality saturationAlexa VanHattum, Rachit Nigam, Vincent T. Lee, James Bornholt et al.ASPLOS 2021 · 57 citations
- VeGen: a vectorizer generator for SIMD and beyondYishen Chen, Charith Mendis, Michael Carbin, Saman P. AmarasingheASPLOS 2021 · 43 citations
- Vector instruction selection for digital signal processors using program synthesisMaaz Bin Safeer Ahmad, Alexander J. Root, Andrew Adams, Shoaib Kamil et al.ASPLOS 2022 · 13 citations
Related papers
- Dataflow-based pruning for speeding up superoptimizationManasij Mukherjee, Pranav Kant, Zhengyang Liu, John RegehrOOPSLA 2020 · 21 citations
- Hydra: Generalizing Peephole Optimizations with Program SynthesisManasij Mukherjee, John RegehrOOPSLA 2024 · 11 citations
- 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
- Seeking Evidence of Further Optimization: Detecting Missed Optimizations through Compiler’s Native AnalysesYi Zhang, Yu Wang, Ke Wang, Linzhang WangOOPSLA 2026
- Mirage: A Multi-Level Superoptimizer for Tensor ProgramsMengdi Wu, Xinhao Cheng, Shengyu Liu, Chunan Shi et al.OSDI 2025 · 49 citations
