Approaching Symbolic Parallelization by Synthesis of Recurrence Decompositions

TL;DR

This paper introduces GraSSP, a new method that automates parallelization of sequential programs by synthesizing recurrence decompositions, enabling efficient parallel execution for certain prefix sum problems.

Contribution

It presents GraSSP, a novel approach combining formal verification and synthesis to automatically decompose data dependencies for parallelization.

Findings

Effective parallelization for specific prefix sum classes

Automated decomposition of data dependencies in loops

Utilizes formal verification and synthesis techniques

Abstract

We present GraSSP, a novel approach to perform automated parallelization relying on recent advances in formal verification and synthesis. GraSSP augments an existing sequential program with an additional functionality to decompose data dependencies in loop iterations, to compute partial results, and to compose them together. We show that for some classes of the sequential prefix sum problems, such parallelization can be performed efficiently.