一句话：用程序合成与形式验证为 LLVM 搜索整数/浮点 SIMD 优化，获得实际加速。
超优化编译器通过在程序空间中进行有意义的搜索，能发现现有最优优化器遗漏的机会。本文提出 Minotaur，一个面向 LLVM 的超优化器，利用程序合成改进代码生成，重点关注整数与浮点 SIMD 代码。它搜索可替换原有指令序列的等价候选，并对每个生成的优化进行形式验证，从而保证语义正确。在 Intel Cascade Lake 上，Minotaur 在 GNU GMP 基准套件上平均加速 7.3%，最高 13%；在 SPEC CPU 2017 上平均加速 1.5%，638.imagick 最高 4.5%。其发现的若干优化已被合入 LLVM。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{0003MR24,
title = {Minotaur: A SIMD-Oriented Synthesizing Superoptimizer},
author = {Zhengyang Liu and Stefan Mada and John Regehr},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689766}
}