Minotaur: A SIMD-Oriented Synthesizing Superoptimizer

TL;DR

Minotaur is a superoptimizer for LLVM that uses program synthesis to optimize SIMD code, achieving measurable speedups and ensuring formal verification of all optimizations.

Contribution

It introduces Minotaur, a novel SIMD-oriented superoptimizer that synthesizes and verifies code improvements, with some optimizations adopted into LLVM.

Findings

Average speedup of 7.3% on GMP benchmarks

Maximum speedup of 13% on GMP benchmarks

Average speedup of 1.5% on SPEC CPU 2017

Abstract

A superoptimizing compiler--one that performs a meaningful search of the program space as part of the optimization process--can find optimization opportunities that are missed by even the best existing optimizing compilers. We created Minotaur: a superoptimizer for LLVM that uses program synthesis to improve its code generation, focusing on integer and floating-point SIMD code. On an Intel Cascade Lake processor, Minotaur achieves an average speedup of 7.3\% on the GNU Multiple Precision library (GMP)'s benchmark suite, with a maximum speedup of 13\%. On SPEC CPU 2017, our superoptimizer produces an average speedup of 1.5\%, with a maximum speedup of 4.5\% for 638.imagick. Every optimization produced by Minotaur has been formally verified, and several optimizations that it has discovered have been implemented in LLVM as a result of our work.