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