Dataflow-Based Pruning for Speeding up Superoptimization
summary
Applies abstract interpretation to prune Souper's enumerative synthesis by proving whole families of partially symbolic candidates infeasible using domains like known bits, ranges, bivalent bits and forced bits. Pruning reduces expensive SMT/CEGIS work, cuts solver calls and avoids enumerating expansions. Evaluated on SPEC CPU2017 with a 128‑thread machine and 300s per problem, the implementation speeds Souper by >2×, synthesizes 8% more optimizations and reduces timeouts by ~40%.
AI-written summary · about
chapters (15)
- 0:00Intro
- 0:13BACKGROUND
- 0:28SUPEROPTIMIZATION
- 1:34LAZY ENUMERATIVE SYNTHESIS
- 2:29BOTTLENECKS
- 3:30PRUNING
- 5:02ABSTRACT INTERPRETATION
- 6:40EXAMPLE
- 7:47KNOWN BITS
- 8:09Candidate
- 9:02INTEGER RANGES
- 9:46BIVALENT BITS
- 11:12FORCED BITS
- 12:22Solving 269113 synthesis problems (derived from SPEC CPU 2017)
- 13:11OPTIMIZATIONS FOUND
related talks
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)
15mHieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical(…)
18mSuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT(…)
40mSuperfusion: Eliminating Intermediate Data Structures via Inductive Synthesis
19mEnhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipu...
19mMinotaur: A SIMD-Oriented Synthesizing Superoptimizer
19mPresynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics
19mOptimizing Ancilla-Based Quantum Circuits with SPARE