Onward! 2017
Sun 22 - Fri 27 October 2017 Vancouver, Canada
co-located with SPLASH 2017
Wed 25 Oct 2017 14:30 - 15:00 at Regency B - Program Generation and Synthesis Chair(s): Emina Torlak

Existing superoptimization and synthesis approaches consider candidate instruction sequences of increasing length and use constraint solvers to check whether a candidate correctly implements the source code. This works well for optimizing short straight-line code. With the increase in length of the target sequence, the search space dramatically increases, posing a challenge for existing approaches.

We describe a new approach to code generation and optimization. Our approach uses an SMT solver in a novel way to generate efficient code for modern architectures and guarantee that the generated code correctly implements the source code. The distinguishing characteristic of our approach is that the size of the constraints does not depend on the length of the candidate sequence of instructions.

We implemented a preliminary prototype of the approach and applied it to optimize small but tricky examples used as standard benchmarks for other superoptimization and synthesis tools. Our implementation handles arbitrary loop-free code (not only basic blocks) as input and output. The quality of generated code compares favorably with production compilers and other superoptimization tools.

Wed 25 Oct

onward-2017-Onward-Papers
13:30 - 15:00: Onward! Papers - Program Generation and Synthesis at Regency B
Chair(s): Emina TorlakUniversity of Washington
onward-2017-Onward-Papers13:30 - 14:00
Talk
Mandana VaziriIBM Research, Louis MandelIBM Research, Avraham ShinnarIBM Research, Jerome SimeonIBM Research, Martin HirzelIBM Research
onward-2017-Onward-Papers14:00 - 14:30
Talk
Edmund LamUniversity of Colorado Boulder, Peilun Zhang, Bor-Yuh Evan ChangUniversity of Colorado Boulder
onward-2017-Onward-Papers14:30 - 15:00
Talk
Abhinav JangdaUniversity of Massachusetts, Amherst, Greta YorshQueen Mary University of London