Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Minotaur: A SIMD-Oriented Synthesizing Superoptimizer

Zhengyang Liu, Stefan Mada, John Regehr

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.

Minotaur: A SIMD-Oriented Synthesizing Superoptimizer

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.
Paper Structure (32 sections, 9 figures, 3 tables, 4 algorithms)

This paper contains 32 sections, 9 figures, 3 tables, 4 algorithms.

Table of Contents

  1. Introduction
  2. Cutting LLVM Functions
  3. Problem Statement
  4. Example
  5. Correctness Argument
  6. Detailed Solution
  7. Relation to Previous Cut-Based Superoptimizers
  8. Formalizing Vector Intrinsics in Alive2
  9. Background: Vectors in LLVM
  10. Assigning a Formal Semantics to Vector Intrinsics
  11. Validating our Changes to Alive2
  12. Synthesizing Optimizations
  13. Designing an Appropriate Synthesis Procedure
  14. Synthesis in Minotaur
  15. Identifying Profitable Rewrites
  16. ...and 17 more sections

Figures (9)

  • Figure 1: Overview of how Minotaur works, and how it fits into the LLVM optimization pipeline
  • Figure 2: Example of cutting an LLVM function
  • Figure 3: Example of cut extraction
  • Figure 4: Example of synthesizing a rewrite that contains literal constants. Purple nodes are instructions reused from the original cut; blue and orange nodes are synthesized instructions and literal constants.
  • Figure 5: Syntax for Minotaur rewrites
  • ...and 4 more figures