at University of Illinois at Urbana-Champaign, Compilers Seminar, May 2023
Program optimizers, synthesizers, and verifiers use term rewriting to transform code by repeatedly applying syntactic “find and replace” rules. Unfortunately, determining when to run which rules can be fiendishly difficult. My group has been developing egg, a new Equality Saturation (EqSat) toolkit to address these challenges. EqSat is now used in production in WebAssembly compilers from Fastly, circuit design tools at Intel, and ML kernel optimizers at Google. EqSat attempts to apply all rewrite rules in every order; it mitigates space explosion by repurposing the e-graph data structure for congruence reasoning from automated theorem provers. The egg EqSat toolkit provides fast implementations for searching e-graphs and maintaining their invariants, as well as extensions to integrate non-syntactic, domain-specific analyses and transformations. This talk will survey egg’s design and recent innovations applying techniques from relational databases to improve performance, expressiveness, and proof generation for EqSat.
Zachary Tatlock is an Associate Professor in the Allen School of Computer Science and Engineering at the University of Washington. He earned his PhD from UC San Diego and BS degrees from Purdue. At UW, Zach tries to keep up with his students exploring the practical limits of rewrite systems, working on compilers and runtimes to support machine learning accelerators, automatically addressing rounding error in numerical programs, and extending programming languages techniques to computational fabrication.