Write a Blog >>
Tue 20 Jun 2017 14:50 - 15:15 at Actes, Civil Engineering - Parallelization and Concurrency Chair(s): Milind Kulkarni

Parallelizing of software improves its effectiveness and productivity. To guarantee correctness, each new parallel version of the former code must be formally verified to be equivalent to the serial version. We present a novel approach, called GRASSP, that automatically synthesizes parallel versions of software by treating the given serial versions as specifications. GRASSP statically augments an existing serial program with additional functionality to decompose data dependencies in loop iterations, to compute partial results, and to recompose them. In contrast to other parallelizers, GRASSP gradually considers several parallelization scenarios and certifies the results using Horn-based invariant synthesis. For several classes of single-pass array-processing programs, we show that such static 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.

Conference Day
Tue 20 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:40
Parallelization and ConcurrencyPLDI Research Papers at Actes, Civil Engineering
Chair(s): Milind KulkarniPurdue University
14:00
25m
Talk
Synthesis of Divide and Conquer Parallelism for Loops
PLDI Research Papers
Azadeh FarzanUniversity of Toronto, Victor NicoletUniversity of Toronto
Media Attached
14:25
25m
Talk
Futhark: Purely Functional GPU-programming with Nested Parallelism and In-place Array Updates
PLDI Research Papers
Troels HenriksenDIKU, University of Copenhagen, Niels G. W. SerupDIKU, University of Copenhagen, Martin ElsmanDepartment of Computer Science, University of Copenhagen, Fritz HengleinDIKU, Denmark, Cosmin OanceaDIKU, University of Copenhagen
Media Attached
14:50
25m
Talk
Gradual Synthesis for Static Parallelization
PLDI Research Papers
Grigory FedyukovichUW CSE, Maaz Bin Safeer AhmadUW / CSE, Rastislav BodikUniversity of Washington
Pre-print Media Attached
15:15
25m
Talk
Verifying invariants of lock-free data structures with rely-guarantee and refinement type
PLDI Research Papers
Colin GordonDrexel University, Michael D. ErnstUniversity of Washington, USA, Dan GrossmanUniversity of Washington, Matthew ParkinsonMicrosoft Research, UK
Pre-print Media Attached