Verifying and Improving Halide’s Term Rewriting System with Program Synthesis
summary
Halide’s term rewriting system is formally verified and extended using SMT and synthesis tools: Z3 proves 88% of rules automatically and Coq completes the remaining proofs, finding 4 unsound rules and later 44 broken rules after a division-by-zero semantics change. Termination is proved by a compositional reduction order after fixing 8 rules. A CEGIS-based synthesizer consumes ~100k real expressions and yields 4,000 new rules in a day, improving peak memory by up to 50% with no noticeable compile-time slowdown; fixes match or beat five human patches.
AI-written summary · about
chapters (14)
- 0:00Start
- 0:37A key component! Running benchmark suite without this engine resulted in a 5x increase in compilation times and a 26x increase in runtimes
- 1:02Uses of the reasoning engine
- 1:59Talk roadmap
- 2:44Term rewriting systems
- 3:43Limits to reasoning power Reasoning power vs. performance
- 4:50Proofs of Correctness: Soundness SMT Solver
- 5:44An example of an unsound rule
- 6:25Reverification of new semantics
- 7:29Proofs of correctness: termination
- 8:34Reduction order
- 9:25The Halide simplification order
- 11:18Strengthening the ruleset via synthesis
- 12:23Our synthesis pipeline (briefly)
related talks
21mVerifying term graph optimizations using Isabelle/HOL
15mValidating SMT Rewriters via Rewrite Space Exploration Supported by Generative(…)
30mSemantics-Guided Synthesis
21mSynthesizing Formal Semantics from Executable Interpreters
20mMISAAL: Synthesis-Based Automatic Generation of Efficient and Retargetable(…)
31mLetting users do the undecidable: lessons from program synthesis
30mAnalyzing Programs with SMT Solvers
18mVerifying Solutions to Semantics-Guided Synthesis Problems