Superoptimizer Project

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

Problem

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:

With the saturation of Moore's law, modern hardware is fast becoming more complex and harder to program; examples include complex instruction sets, multi-core chips, programmable interconnects, accelerator hardware like GPGPUs, network processors, crypto processors, etc. While all these hardware components are programmable, the most common way of extracting high-performance from these devices (including CPUs) is still through manual coding of assembly instructions!
More fundamentally speaking: while the number of transistors on a chip has still been increasing at an exponential rate, the clock frequency has saturated several years ago. Hence, the next-generation improvements in performance and power-to-performance ratios require innovative software-hardware solutions and cannot simply rely on improving clock rate.
Modern software stacks require two primary changes to tackle this changing hardware environment:
- Higher level programming abstractions, e.g., domain-specific languages, higher-level programming constructs that are intuitive yet amenable to efficient mapping on modern hardware, abstractions that allow visibility to higher-level semantics allowing an automatic optimizer to optimize the logic, etc.
- Powerful compilation support: the optimizers in modern compilers need to be much more powerful than what they are today. Unfortunately, today's compilers are already too complex; a potential solution perhaps requires a complete redesign of compiler technology.
Both the design of programming abstractions and compiler support are tightly inter-dependent: good abstractions are those that can be compiled efficiently; a good compiler should be able to compile the desired abstractions. Thus these problems cannot be looked-at in isolation.

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:

Counterexample-Guided Correlation Algorithm for Translation Validation (authors: Shubhani Gupta, Abhishek Rose, and Sorav Bansal), conditionally accepted at OOPSLA 2020
OOElala: Order-Of-Evaluation based Alias Analysis for compiler optimization [ Short Video, Full Video ] at PLDI 2020
Effective use of SMT solvers for program equivalence checking through invariant sketching and query decomposition [ slides ] at SAT 2018
Black-box equivalence checking across compiler optimizations at APLAS 2017
Modeling undefined behaviour semantics for checking equivalence across compiler optimizations at HVC 2017
Fast Dynamic Binary Translation for the Kernel [ talk video ] at SOSP 2013
Binary Translation using Peephole Superoptimizers at OSDI 2008
Automatic Generation of Peephole Superoptimizers at ASPLOS 2006

Impact so far

We collect some links to what others have been saying publicly about our efforts.

A nice talk by John Regehr on LLVM superoptimization [at 14:40, John talks very kindly about our superoptimizer paper, calling it the first modern superoptimizer. Thanks very much John!]
Our superoptimizer algorithm has been used to optimize WebAssembly
The GNU superoptimizer 2.0 talks about our peephole superoptimizer algorithm during 11:30-17:00 using data from our ASPLOS 06 paper.
Our superoptimizer "was a direct inspiration for" (quoted from their paper) the Souper system.

Here are some bug reports that were generated by applying our equivalence checker to a few software artifacts:

Bugs in GCC and ICC compilers : all reported and fixed. See details in our APLAS17 paper and the Counter paper. Here are an example bug (in ICC):
hello

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

We would like to involve you in our tools that

compile a C program to x86 assembly (our "code generator") using automatically generated translations, and
automatically infer translations using AI/ML techniques

The exact project may depend on the current needs of the project and your interests.

Demo

compiler.ai 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:

Manjeet Dahiya. Completed PhD in 2018.
Shubhani Gupta. Pursuing PhD
Abhishek Rose. Pursuing PhD
Masters and UG students