Superoptimizer Project

This page is intended to be an introduction to our ongoing superoptimizer project for prospective students looking to join our research team.


Today, compilers are overwhelmingly complex (GCC is over 14 million lines of code) and are rapidly increasing in their complexity. Yet they are quite weak and fragile in meeting modern computing needs:

Proposed solution : synthesis and superoptimization

Researchers have been working on applying the vast amount of computing resources to chip at this problem at least for over 12-13 years now, and some of these ideas are now coming to fruition. Essentially, these techniques involve applying search techniques (ala AI/ML techniques) to automatically infer high-performance software implementations (for a given machine) from high-level program specifications. You can read more about these techniques on the wikipedia pages for program synthesis and superoptimization.

Our efforts

We are working on an automatic "peephole superoptimizer", an idea that is described in detail in this paper on Automatic Generation of Peephole Superoptimizers. While this work automatically generated peephole optimizations through search-based (AI/ML) techniques, later work on binary translation extended these ideas to automatically generate translations from one ISA (PowerPC) to another (x86). In current work, we have been generalizing these ideas to automatically generate translations from LLVM IR to x86 ISA. We have also generalized the nature of these translations to allow reasoning about loops and aliasing, two very important features that enable effective compiler optimizations. An important sub-problem is automatic equivalence checking across an unoptimized and an optimized program. Some of our recent work has been published in this context of equivalence checking:

Impact so far

We collect some links to what others have been saying publicly about our efforts. Here are some bug reports that were generated by applying our equivalence checker to a few software artifacts:

What would a BTech/MTech project in this area look like

We would like to involve you in our tools that The exact project may depend on the current needs of the project and your interests.

Demo hosts an early demo of our optimizing compiler, and our equivalence checker. This is work in progress.

Whom to contact

If you are interested in working on something like this, you can write to Sorav Bansal. You can also contact some of the current and previous people who have worked (or are working on) this project to get more clarity: