Hydra: Generalizing Peephole Optimizations with Program Synthesis
summary
Hydra uses program synthesis to turn specific superoptimizer rewrites into width-independent rules by synthesizing symbolic constants, dataflow preconditions and type assignments through three synthesis loops; it reduces bitwidths to 2–8 bits to brute-force model counting and speed up SMT queries. Hydra generalizes about 75% of the ungeneralized missed peephole optimizations from LLVM’s issue tracker, formally verifies every generated rewrite with Alive2 and automatically generates LLVM C++ suitable for instcombine.
AI-written summary · about
chapters (11)
- 0:00Hydra and program synthesis
- 2:08Peephole optimizations overview
- 3:57Manual optimization limits
- 4:40Synthesis steps for optimizations
- 6:25Valid preconditions for optimizations
- 8:11Width independence in optimizations
- 10:19Handling constants in optimizations
- 12:05Symbolic data flow in optimizations
- 13:31Hydra’s optimization impact
- 14:55Hydra vs LLVM instcombine
- 15:57Q&A
related talks
15mHieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical(…)
43mHydra's Heads – Dmitriy Ivanov
22mAlgorithm-Aware Hardware Optimization using E-Graph Rewriting: how should we marry(…)
20mMISAAL: Synthesis-Based Automatic Generation of Efficient and Retargetable(…)
15mVerifying and Improving Halide’s Term Rewriting System with Program Synthesis
28mBorrow checking Hylo
23mInductive Program Synthesis by Meta-Analysis-Guided Hole Filling
30mAutomated High-Level Synthesis Design Modularization via E-Graph Anti-Unification