[talks] CJ Bell preFPO

Melissa M. Lawson mml at CS.Princeton.EDU
Mon Jan 7 16:54:45 EST 2013

CJ Bell will present his preFPO on Monday January 14 at 8AM in Room 402.
The members of his committee are:  David Walker, advisor; Andrew Appel and 
David August, readers; Sharad Malik (ELE) and Ed Felten, nonreaders.  Everyone 
is invited to attend his talk.  His abstract follows below.  

Title: Proving the Correctness of Parallelizing Optimizations

Sustaining scalable performance trends in the multicore era requires
that programmers and compiler writers rely on thread-level parallelism
to attain greater performance from their programs. One way to do so is
to develop a sequential program and then apply parallelizing
transformations to that sequential program; some compilers do this
automatically. However, the optimization phase is the most common
source of bugs in a compiler; they are often subtle and hard to detect
because many complex optimizations are combined in unique ways for
each input program.

Thus we have developed a framework of local program rewrite rules,
triggered by logical preconditions, and have proven this framework
sound in the Coq proof assistant. These local transformations may be
composed and recombined in a variety of different ways; in particular,
they may be used to implement classic parallelizing optimizations such
as DOALL and DOACROSS as well as more modern techniques such as DSWP
(Decoupled Software Pipelining) and combinations of the above.

The key challenges to proving the soundness of our framework were to
develop a generic loop transformation that can rewrite two parallel
while loops into one single while loop; a parallelization
transformation that allows threads to communicate and does not require
termination; and a new definition of behavioral equivalence that is
preserved by parallelization, which we call decoupled bisimulation. In
this talk, our primary focus is on the details of decoupled
bisimulation: why existing definitions of equivalence are insufficient
for stating the correctness of parallelization, how it compares to
existing definitions, and which behavioral properties it preserves.

More information about the talks mailing list