Skip to content

Allen School Blog

Allen School researchers receive CACM Research Highlight for making equality saturation more practical


A yellow carton full of white eggs sits against a yellow background.
(Pexels/Elif Tekkaya)

Many software tools, including compilers, optimizers and synthesizers, all depend on a common core to transform long and complicated programs into a simplified equivalent. This pattern stretches across a variety of problems, from shrinking three-dimensional CAD models to optimizing SQL queries. 

Portrait of Zachary Tatlock
Allen School professor Zachary Tatlock

Previously, each problem required developing an ad hoc and application-specific search strategy. But then a team of researchers led by Allen School professor Zachary Tatlock, including his former postdoc Max Willsey (Ph.D., ‘21) and current Ph.D. student Oliver Flatt, came up with a novel approach that could be generalized and reused across a variety of situations — allowing developers to focus on optimization and efficiency.

The researchers introduced egg, an open-source library that uses e-graphs, or equality graphs, along with equality saturation to optimize term representations. Since its release, egg has inspired the emergence of an entire community, with annual workshops, multiple follow-up papers and industry adoption. The team’s paper “egg: Fast and Extensible Equality Saturation” was recently selected as a Communications of the ACM (CACM) Research Highlight, which recognizes outstanding research with strong, novel contributions to the field and broad interest to the computing community. 

“What’s remarkable about the egg project is how quickly it went from a research idea to a wide-ranging toolkit,” said Tatlock, who holds the Paul G. Allen Career Development Professorship in the Allen School. “In just a few years, it’s been adopted across domains from deep learning to hardware design. We’re seeing 50x speedups in neural network optimizations, 63% smaller hardware circuits, and even production compilers being rebuilt around e-graphs.”

While equality saturation and e-graphs were in use before egg’s introduction, the researchers introduced two new techniques to make this approach fast and extensible — amortized invariant maintenance and e-class analyses. The former, a new amortized invariant restoration technique called rebuilding, loosens the e-graph’s data structure invariants and only enforces them at the right time to make them run much faster. The latter makes e-graphs more flexible by allowing users to bring program analyses such as constant propagation into the e-graph environment, reducing the need for ad hoc manipulations.

By making equality saturation practical, egg essentially gave everyone a powerful new hammer — and it turns out many nails were waiting.

Zachary TatlockAllen School professor

Already, egg has been applied broadly and re-implemented across the tech industry. For example, hardware engineers at companies such as Intel have adopted e-graph rewriting to improve their chip design. In the field of numerical computing, researchers were able to integrate egg into parts of Herbie, a tool for reducing floating-point error, making it 3,000 times faster.

“By making equality saturation practical, egg essentially gave everyone a powerful new hammer — and it turns out many nails were waiting,” Tatlock said.

The egg research team is made up of current or former members of the University of Washington’s Programming Languages and Software Engineering (PLSE) group. Additional authors include Allen School alumni Chandrakana Nandi (Ph.D., ‘21), Allen School affiliate faculty member and director of U.S. R&D at Certora; Yisu Remy Wang (Ph.D., ‘23), faculty at University of California, Los Angeles; and Pavel Panchekha (Ph.D. ‘19), faculty at University of Utah. 

Read the full paper on egg here, as well as the CACM Research Highlight and a related CACM Technical Perspective.