SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Thu 19 Nov 2020 13:20 - 13:40 at SPLASH-I - R-4 Chair(s): Robert Rand, Rohan Padhye
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
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.

Fri 20 Nov

Displayed time zone: Central Time (US & Canada) change