Dataflow-Based Pruning for Speeding up Superoptimization
Fri 20 Nov 2020 01:20 - 01:40 at SPLASH-I - R-4 Chair(s): Sylvain Boulmé, Gushu Li
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
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.