Abstract

Equality saturation is a recent technique that mitigates the phase ordering problem in compilers. Instead of performing destructive rewrite rules over the input program, equality saturation memorizes all the equivalent representations compactly in a data structure called e-graph (equality graphs) and executes multiple rewrite rules simultaneously over e-graphs. 

Designing an efficient algorithm for term extraction from e-graphs is challenging because the candidate space can be exponentially large and candidate terms can be cyclic. We present a Weighted Partial MaxSAT encoding of the extraction problem by identifying cycles in the e-graph and encoding acyclic constraints with Tseitin transformation to avoid extracting cyclic terms. Our evaluation of real-world workload shows a ~3x speed-up in comparison with extraction with the ILP encoding. Next, we present a case study of applying equality saturation to resource synthesis for packet programs. We propose CatsTail, a packet program compilation pipeline that leverages equality saturation to find feasible ALU mappings to reconfigurable switches. We benchmarked CatsTail using real-world switch programs and compared its synthesis performance with a previous work CaT. CatsTail shows comparable stage utilization optimality while being up to two orders of magnitude faster than CaT in resource synthesis for real-world P4 programs.

Finally, if time permits, we will talk about an ongoing project of automated invariant synthesis for distributed systems.

Reading List

Textbooks

Software Foundations, Vol 1, Vol 2 Chapters 1~11

Logic in Computer Science, Chapters 1, 2, 3.1-3.5, 4, 6.1

Papers

Equality Saturation and its Applications

1. egg: Fast and extensible equality saturation (POPL’21)

2. Pure Tensor Program Rewriting via Access Patterns (MAPS’21)

3. CaT: A Solver-Aided Compiler for Packet-Processing Pipelines (ASPLOS’23)

4. Cetus: Releasing P4 Programmers from the Chore of Trial and Error Compiling (NSDI’22)

Verification for Distributed Systems

5. Syntax-guided Synthesis (FMCAD’13)

6. DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols (OSDI’22)

7. Message Chain Invariant for Distributed System Verification (OOPSLA’23)

8. Verdi: A Framework for Implementing and Formally Verifying Distributed Systems (PLDI’15)

Formal Methods Background

9. Software model checking (ACM Computing Survey)