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.

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 Kulkarni Purdue University
14:00
25m
Talk
Synthesis of Divide and Conquer Parallelism for Loops
PLDI Research Papers
Azadeh Farzan University of Toronto, Victor Nicolet University 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 Henriksen DIKU, University of Copenhagen, Niels G. W. Serup DIKU, University of Copenhagen, Martin Elsman Department of Computer Science, University of Copenhagen, Fritz Henglein DIKU, Denmark, Cosmin Oancea DIKU, University of Copenhagen
Media Attached
14:50
25m
Talk
Gradual Synthesis for Static Parallelization
PLDI Research Papers
Grigory Fedyukovich UW CSE, Maaz Bin Safeer Ahmad UW / CSE, Rastislav Bodik University 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 Gordon Drexel University, Michael D. Ernst University of Washington, USA, Dan Grossman University of Washington, Matthew Parkinson Microsoft Research, UK
Pre-print Media Attached