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.