Skip to main content
Open Access Publications from the University of California

UC San Diego

UC San Diego Electronic Theses and Dissertations bannerUC San Diego

Equality saturation : engineering challenges and applications


In this dissertation, I describe the Peggy system for performing program optimization and translation validation. Peggy is based on the concept of Equality Saturation, in which axiomatic reasoning is applied to a program to produce exponentially many equivalent versions of that program, which can then be explored simultaneously. This is achieved by using a custom intermediate representation that facilitates mathematical reasoning over programs. I will specifically address some of the engineering challenges posed by making a working implementation of the Equality Saturation technique, as well as the major applications to which we have applied it. I implemented front-ends for Peggy to convert both Java bytecode programs and LLVM programs to and from our custom intermediate representation. I designed and implemented a domain-specific language for writing the axioms that are used by the Equality Saturation engine. For the purposes of optimization, I designed the technique whereby we choose the optimal program from our representation of exponentially many equivalent programs. I implemented both our optimization and our translation validation frameworks that use the Equality Saturation engine. In addition, I performed experiments showing the effectiveness of Equality Saturation at both program optimization and translation validation

Main Content
For improved accessibility of PDF content, download the file to your device.
Current View