Dataflow-based pruning for speeding up superoptimization
Dataflow-based pruning for speeding up superoptimization
复制标题
基于数据流的修剪可加速超级优化
DOI：
10.1145/3428245
复制
发表时间：
2020
影响因子：
--
通讯作者：
J. Regehr
中科院分区：
文献类型：
--
作者：
Manasij Mukherjee;Pranav Kant;Zhengyang Liu;J. Regehr
超级优化是一种编译策略，它使用搜索来提高代码质量，而不是像传统的优化编译器那样依赖于固定的转换序列。这种搜索可以看作是一个程序合成问题：从未优化的代码作为规范，合成过程试图创建一个更有效的实现。一个重要的综合算法家族的工作原理是枚举候选者，然后使用SMT求解器连续检查每个候选者是否细化了规范。本文的贡献是一个修剪技术，减少了枚举搜索空间，使用快速的基于卷积的技术，丢弃合成候选人，包含符号常量和未实例化的指令。我们证明了这种技术的有效性，通过提高运行时的枚举合成过程中的Souper超优化器的LLVM中间表示。本文中提出的技术消除了Souper进行的65%的求解器调用，使其在解决Souper在优化SPEC CPU 2017的C和C++程序时遇到的所有269，113个综合问题时快2.32倍（14.54小时vs 33.76小时基线，在大型多核上）。
Superoptimization is a compilation strategy that uses search to improve code quality, rather than relying on a canned sequence of transformations, as traditional optimizing compilers do. This search can be seen as a program synthesis problem: from unoptimized code serving as a specification, the synthesis procedure attempts to create a more efficient implementation. An important family of synthesis algorithms works by enumerating candidates and then successively checking if each refines the specification, using an SMT solver. The contribution of this paper is a pruning technique which reduces the enumerative search space using fast dataflow-based techniques to discard synthesis candidates that contain symbolic constants and uninstantiated instructions. We demonstrate the effectiveness of this technique by improving the runtime of an enumerative synthesis procedure in the Souper superoptimizer for the LLVM intermediate representation. The techniques presented in this paper eliminate 65% of the solver calls made by Souper, making it 2.32x faster (14.54 hours vs 33.76 hours baseline, on a large multicore) at solving all 269,113 synthesis problems that Souper encounters when optimizing the C and C++ programs from SPEC CPU 2017.
通过类型引导的抽象细化进行程序合成
影响因子：
--
作者：
Guo, Zheng;James, Michael;Justo, David;Zhou, Jiaxiao;Wang, Ziteng;Jhala, Ranjit;Polikarpova, Nadia
通讯作者：
Polikarpova, Nadia