Fri 20 Nov 2020 01:20 - 01:40 at SPLASH-I - R-4 Chair(s): Gushu Li, Sylvain Boulmé
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.
Thu 19 Nov Times are displayed in time zone: Central Time (US & Canada) change
13:00 - 14:20: R-4OOPSLA at SPLASH-I +12h Chair(s): Rohan PadhyeCarnegie Mellon University, Robert RandUniversity of Chicago | |||
13:00 - 13:20 Talk | Assertion-Based Optimization of Quantum Programs OOPSLA Link to publication DOI Media Attached | ||
13:20 - 13:40 Talk | Dataflow-Based Pruning for Speeding up Superoptimization OOPSLA Manasij MukherjeeUniversity of Utah, Pranav KantUniversity of Utah, Zhengyang LiuUniversity of Utah, John RegehrUniversity of Utah Link to publication DOI Media Attached | ||
13:40 - 14:00 Talk | Enabling Accuracy-Aware Quantum Compilers using Symbolic Resource Estimation OOPSLA Link to publication DOI Media Attached | ||
14:00 - 14:20 Talk | Eliminating Abstraction Overhead of Java Stream Pipelines using Ahead-of-Time Program Optimization OOPSLA Link to publication DOI Pre-print Media Attached |
Fri 20 Nov Times are displayed in time zone: Central Time (US & Canada) change
01:00 - 02:20: R-4OOPSLA at SPLASH-I Chair(s): Gushu LiUniversity of California at Santa Barbara, Sylvain BoulméGrenoble Alps University / CNRS / Grenoble INP / VERIMAG | |||
01:00 - 01:20 Talk | Assertion-Based Optimization of Quantum Programs OOPSLA Link to publication DOI Media Attached | ||
01:20 - 01:40 Talk | Dataflow-Based Pruning for Speeding up Superoptimization OOPSLA Manasij MukherjeeUniversity of Utah, Pranav KantUniversity of Utah, Zhengyang LiuUniversity of Utah, John RegehrUniversity of Utah Link to publication DOI Media Attached | ||
01:40 - 02:00 Talk | Enabling Accuracy-Aware Quantum Compilers using Symbolic Resource Estimation OOPSLA Link to publication DOI Media Attached | ||
02:00 - 02:20 Talk | Eliminating Abstraction Overhead of Java Stream Pipelines using Ahead-of-Time Program Optimization OOPSLA Link to publication DOI Pre-print Media Attached |