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.
 Gradual Synthesis for Static Parallelization of Single-Pass Array-Processing Programs
Grigory Fedyukovich, Maaz Bin Safeer Ahmad and Rastislav Bodik
PLDI 2017 (To Appear)
 Approaching Symbolic Parallelization by Synthesis of Recurrence Decompositions
Grigory Fedyukovich and Rastislav Bodik
If you have any questions, want to be kept up-to date, or just want to say hi, email us!