Mike He will present his General Exam "Equality Saturation: Term Extraction and an Application to Network Synthesis" on April 16th, 2024 at 10:30am in CS 401 and Zoom. Zoom link: https://princeton.zoom.us/my/deyuan Committee Members: Aarti Gupta (adviser), Andrew Appel, and Mae Milano Link to Abstract and Reading List: [ https://docs.google.com/document/d/1hiZgxT9Jj0U_V83oK9eTD9siDWR0wdVKXE3BSknh... | https://docs.google.com/document/d/1hiZgxT9Jj0U_V83oK9eTD9siDWR0wdVKXE3BSknh... ] [ https://docs.google.com/document/d/1hiZgxT9Jj0U_V83oK9eTD9siDWR0wdVKXE3BSknh... | Abst ] [ https://docs.google.com/document/d/1hiZgxT9Jj0U_V83oK9eTD9siDWR0wdVKXE3BSknh... | ract ] 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. [ https://docs.google.com/document/d/1hiZgxT9Jj0U_V83oK9eTD9siDWR0wdVKXE3BSknh... | Reading List ] Textbooks Software Foundations, [ https://softwarefoundations.cis.upenn.edu/lf-current/index.html | Vol 1 ] , [ https://softwarefoundations.cis.upenn.edu/plf-current/index.html | 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. [ https://dl.acm.org/doi/10.1145/3434304 | egg: Fast and extensible equality saturation ] (POPL’21) 2. [ https://arxiv.org/abs/2105.09377 | Pure Tensor Program Rewriting via Access Patterns ] (MAPS’21) 3. [ https://dl.acm.org/doi/abs/10.1145/3582016.3582036 | CaT: A Solver-Aided Compiler for Packet-Processing Pipelines ] (ASPLOS’23) 4. [ https://www.usenix.org/conference/nsdi22/presentation/li-yifan | Cetus: Releasing P4 Programmers from the Chore of Trial and Error Compiling ] (NSDI’22) Verification for Distributed Systems 1. [ https://www.cis.upenn.edu/~alur/SyGuS13.pdf | Syntax-guided Synthesis ] (FMCAD’13) 2. [ https://www.usenix.org/conference/osdi22/presentation/yao | DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols ] (OSDI’22) 3. [ https://dl.acm.org/doi/pdf/10.1145/3622876 | Message Chain Invariant for Distributed System Verification ] (OOPSLA’23) 4. [ https://homes.cs.washington.edu/~ztatlock/pubs/verdi-wilcox-pldi15.pdf | Verdi: A Framework for Implementing and Formally Verifying Distributed Systems ] (PLDI’15) Formal Methods Background 1. [ https://dl.acm.org/doi/10.1145/1592434.1592438 | Software model checking ] (ACM Computing Survey) [ https://people.eecs.berkeley.edu/~sseshia/pubdir/SMT-BookChapter.pdf | Satisfiability Modulo Theories. Handbook of Model Checking ] (2018)