Gradual Synthesis for Static Parallelization

Parallelizing of software improves its effectiveness and productivity. 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 GraSSP, 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 segmentation of the array that allows computing partial results for each segment and merging them. In contrast to other parallelizers, GraSSP gradually considers several parallelization 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

[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!