Optimization and Verification of Parallel Programs

People Papers

We want to provide optimization and verification techniques for parallel programs that are on par with today's standards for sequential programs. We believe that the key enabler is to raise the level of abstraction of parallel programming.

We study parallel programs in the context of X10, a parallel langauge designed at IBM. Two of X10's key constructs for parallelism are async and finish. The async statement is a lightweight notation for spawning threads, while a finish statement (finish s) waits for termination of all async statement bodies started while executing the statement s. Additionally, X10 supports multidimensional distributed arrays.

We have rewritten a state-of-the-art plasma simulation program from Fortran 95 to X10. We have designed a core calculus with async and finish and shown that the semantics enables managable proofs of key properties. We have designed a context-sensitive may-happen-in-parallel analysis that gives precise static information about the parallel behavior of a program. We have built a compiler for a subset of X10 1.5 and shown that for our plasma simulation program, our compiler produces code that is about 5,000 times faster than the code produced by IBM's X10 1.5 compiler.

We are working on a suite of optimization and verification problems for X10. We gratefully acknowledge financial support from IBM.