Gradual Synthesis for Static Parallelization

Parallelizing of software improves its effectiveness and pro- ductivity. To guarantee correctness, the parallel and serial versions of the same code must be formally verified to be equivalent. We present a novel approach, called G RA SSP, that automatically synthesizes parallel single-pass array- processing programs by treating the given serial versions as specifications. Given arbitrary segmentation of the input array, GRASSP synthesizes a code to determine a new seg- mentation of the array that allows computing partial results for each segment and merging them. In contrast to other parallelizers, GRASSP gradually considers several paral- lelization scenarios and certifies the results using constrained Horn solving. For several classes of programs, we show that such parallelization can be performed efficiently. The C++ translations of the GRASSP solutions sped performance by up to 5X relative to serial code on an 8-thread machine and Hadoop translations by up to 10X on a 10-node Amazon EMR cluster.


[1]  Gradual Synthesis for Static Parallelization of Single-Pass Array-Processing Programs
      Grigory Fedyukovich, Maaz Bin Safeer Ahmad and Rastislav Bodik
      PLDI 2017 (To Appear)

[2]  Approaching Symbolic Parallelization by Synthesis of Recurrence Decompositions
      Grigory Fedyukovich and Rastislav Bodik
      SYNT 2016


If you have any questions, want to be kept up-to date, or just want to say hi, email us!