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