compiler.ai

Superoptimizer, Equivalence Checker, and Related Stuff

About

compiler.ai is a research effort at re-imagining the compilation infrastructure. We employ AI algorithms to automatically optimize programs. We employ formal verification techniques to generate confidence in the correctness of the optimizations. As our research matures, we intend to provide links to working demos and downloadable packages on this page.

Counter algorithm for blackbox equivalence checking

Are you an assembly language developer? Or do you want to validate the code generated by a compiler? Our equivalence checker can compute equivalence between a C program and its optimized, usually aggressively vectorized assembly code implementation. The assembly code implementation may be generated by a compiler or hand-written. The algorithm that automatically constructs an equivalence proof is calledCounter, and to the best of our knowledge, it is the most robust equivalence checking algorithm till date. You can try it yourself at the following online demo links. Our OOPSLA 2020 paper on the Counter algorithm will be out soon.

Counter Demo and Examples

You can run the Counter equivalence checking algorithm for yourself here. Here are some pre-configured examples that demonstrate the Counter algorithm in action. Each row lists a benchmark name (C code); for each benchmark, we demonstrate equivalence computation against O3-optimized assembly implementations generated by the GCC and Clang/LLVM compilers.
s000clanggcc
s1112clanggcc
s112clanggcc
s121clanggcc
s1221clanggcc
s122clanggcc
s1251clanggcc
s127clanggcc
s1281clanggcc
s1351clanggcc
s162clanggcc
s173clanggcc
s176clanggcc
s2244clanggcc
s243clanggcc
s251clanggcc
s3251clanggcc
s351clanggcc
s452clanggcc
s453clanggcc
sum1dclanggcc
vdotrclanggcc
vpvclanggcc
vpvpvclanggcc
vpvtsclanggcc
vpvtvclanggcc
vtvclanggcc
vtvtvclanggcc
s1111clanggcc
s1115clanggcc
s1119clanggcc
s111clanggcc
s113clanggcc
s114clanggcc
s1161clanggcc
s116clanggcc
s119clanggcc
s1213clanggcc
s124clanggcc
s125clanggcc
s1279clanggcc
s128clanggcc
s131clanggcc
s132clanggcc
s1421clanggcc
s171clanggcc
s174clanggcc
s2233clanggcc
s252clanggcc
s253clanggcc
s254clanggcc
s2710clanggcc
s2711clanggcc
s2712clanggcc
s271clanggcc
s272clanggcc
s273clanggcc
s274clanggcc
s276clanggcc
s293clanggcc
s3111clanggcc
s311clanggcc
s317clanggcc
s319clanggcc
s331clanggcc
s352clanggcc
s4115clanggcc
s421clanggcc
s423clanggcc
s441clanggcc
s442clanggcc
s443clanggcc
s471clanggcc
vaclanggcc
vborclanggcc
vifclanggcc

Counter Download

Counter source code is available at github.com/compilerai/counter.

OOElala optimizing compiler

Programming languages like C and C++ leave the Order of Evaluation of operands in an expression unspecified. This provides optimization leverage, with resulting speedups as high as 2.6x on real-world code. This optimization opportunity was hitherto not exploited by modern compilers. Our optimizing compiler, OOElala, which is based onClang/LLVM, includes an algorithm to realize this latent performance opportunity. Please see the PLDI 2020 paper on OOElala for more details.

OOElala Demo and Examples

You can try OOElala for yourself here. Here are some pre-configured examples that demonstrate OOElala in action.

OOElala Download

OOElala source code is available at github.com/compilerai/ooelala-project.

Relevant Publications

Brief descriptions of these papers are available at this Github page.

Collaborate with us

We are looking for both young and accomplished researchers and engineers to work and/or collaborate with us. If you are interested in sharing the excitement and joy of participating in our efforts towards the creation of a new type of compilation infrastructure, here are some potential ways we can collaborate.
  • Collaborate with us remotely in our development efforts. If you are interested in such a collaboration, please send us a note. We would love to have a meaningful collaboration that may help all of us achieve our research goals faster. That said, we cannot accept all collaboration requests, as we need to carefully balance the synchronization and starting overheads with the benefits of collaborating. Such a collaboration would perhaps work best if you are already an expert working in this domain and you feel interested in knowing more about our efforts.
  • Join us at IIT Delhi either as visiting faculty, Postdoc, or PhD candidate.
  • Join us at IIT Delhi as a Research Associate for a minimum duration of eighteen months.
Please reach out to Sorav Bansal to take this conversation forward.

Acknowledgements: The online demo links are based on Compiler Explorer.