Thursday, March 25, 2021

Egg: E-Graphs Good

egg: e-graphs good

The egg project uses e-graphs to provide a new way to build program optimizers and synthesizers. egg is developed by Max Willsey and his friends on GitHub.

An e-graph compactly represents many equivalent programs. These four e-graphs represent more and more (even infinite!) ways to write (a × 2) / 2. egg makes e-graphs fast and flexible enough for use in program optimization and synthesis.

The core egg library provides high-performance, flexible e-graphs implemented in Rust. It is packaged on crates.io and documented on docs.rs, including a tutorial that provides an introduction to e-graphs and their use cases.

BibTeX
@article{2021-egg,
  author = {Willsey, Max and Nandi, Chandrakana and Wang, Yisu Remy and Flatt, Oliver and Tatlock, Zachary and Panchekha, Pavel},
  title = {egg: Fast and Extensible Equality Saturation},
  year = {2021},
  issue_date = {January 2021},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {5},
  number = {POPL},
  url = {https://doi.org/10.1145/3434304},
  doi = {10.1145/3434304},
  abstract = {An e-graph efficiently represents a congruence relation over many expressions. Although they were originally developed in the late 1970s for use in automated theorem provers, a more recent technique known as equality saturation repurposes e-graphs to implement state-of-the-art, rewrite-driven compiler optimizations and program synthesizers. However, e-graphs remain unspecialized for this newer use case. Equality saturation workloads exhibit distinct characteristics and often require ad-hoc e-graph extensions to incorporate transformations beyond purely syntactic rewrites.  This work contributes two techniques that make e-graphs fast and extensible, specializing them to equality saturation. A new amortized invariant restoration technique called rebuilding takes advantage of equality saturation's distinct workload, providing asymptotic speedups over current techniques in practice. A general mechanism called e-class analyses integrates domain-specific analyses into the e-graph, reducing the need for ad hoc manipulation.  We implemented these techniques in a new open-source library called egg. Our case studies on three previously published applications of equality saturation highlight how egg's performance and flexibility enable state-of-the-art results across diverse domains.},
  journal = {Proc. ACM Program. Lang.},
  month = jan,
  articleno = {23},
  numpages = {29},
  keywords = {equality saturation, e-graphs}
}
    

News

For updates on egg itself, see the changelog.

Projects using egg

Are you using egg in your project? Open a pull request to add your project to this list!

  • Diospyros automatically vectorizes digital signal processing code. ASPLOS 2021
  • Tensat optimizes deep learning compute graphs both better and faster (up to 50x) than the state of the art. MLSys 2021
  • Herbie improves the accuracy of floating point expressions. The egg-herbie library made parts of Herbie over 3000x faster! PLDI 2015
  • Szalinski shrinks 3D CAD programs to make them more editable. PLDI 2020
  • SPORES optimized linear algebra expressions up to 5x better than state-of-the-art. VLDB 2020
  • Glenside explores the design space of hardware accelerators for a given deep learning program.

Projects inspired by egg

  • Metatheory.jl uses e-graphs and equality saturation for algebraic reasoning in Julia.
  • Zachary DeVito made an awesome Colab exploring e-graphs.
  • Philip Zucker has two blog posts about e-graphs and e-matching in Julia.
View or edit this site on GitHub.


from Hacker News https://ift.tt/3ohLuDk

No comments:

Post a Comment

Note: Only a member of this blog may post a comment.