Minotaur: A SIMD-Oriented Synthesizing Superoptimizer
summary
Minotaur is a synthesizing superoptimizer for LLVM that searches SSA cuts and enumerates cheaper SIMD and scalar rewrites then formally verifies them with Alive2 refinement checker. It uses an SSA-based cut extractor to limit synthesis scope, an enumerator plus SMT for immediate constants, and a micro-op cost model from machine code to pick profitable rewrites. Results are formally verified, yield 7.3% average speedup on GMP (max 13%) and 1.5% on SPEC CPU2017 (max 4.5%), and several rewrites land in LLVM.
AI-written summary · about
chapters (11)
- 0:00Minotaur introduction
- 0:45Missed optimization example
- 3:35Discovering optimization rules
- 5:44Cut extraction for synthesis
- 7:51Refinement checking with Alive2
- 9:21Immediate constants in rewrites
- 11:57Cost modeling for profitability
- 12:39Discovered optimizations examples
- 15:29Performance results on libvalue and SPEC CPU 2017
- 16:30Conclusion and open-source
- 16:53Q&A
related talks
15mHieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical(…)
18mSuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT(…)
20mMISAAL: Synthesis-Based Automatic Generation of Efficient and Retargetable(…)
14mDataflow-Based Pruning for Speeding up Superoptimization
21mTowards Compiler-Guided Static Analysis
23mPoseidon: Profile-Guided Numerical Rewriting at Full-Application Scale
16mSemiring Optimizations: Dynamic Elision of Expressions with Identity and Absorbing Elements
25mThe Road Not Taken: Exploring Alias Analysis Based Optimizations Missed by the Compiler