PL/SE Seminar: Proving the Correctness of Parallelizing Optimizations
Speaker: CJ Bell, Princeton University
Date: Wednesday, March 13 2013
Time: 4:00PM to 5:30PM
Location: 32-D463 (Star)
Host: Adam Chlipala, CSAIL
Contact: Adam Chlipala, adamc@csail.mit.edu
Relevant URL: http://www.cs.princeton.edu/~cbell/
Abstract:
I will present a proof theory for reasoning about the correctness of
parallelizing optimizations based on a new notion of behavioral
equivalence, called decoupled bisimulation. This development is
motivated by the fact that existing behavioral equivalences, such as
those based on bisimulation, are too strong to state the soundness of
even trivial parallelizing transformations.
I show that decoupled bisimulation has several key properties.
Decoupled bisimulation is implied by bisimulation, implies trace
equivalence, and has a succinct characteristic logic. Despite being
weaker than bisimulation, it is strong enough to distinguish between
the classic examples of non-behaviorally equivalent programs. In the
context of the calculus of communicating systems (CCS), decoupled
bisimulation is a congruence (with the usual caveat for the choice
operator and weak transitions).
Crucially, I show that it is sufficient to state the soundness of a
general parallelizing transformation for CCS extended with sequential
composition. Using this and other sound transformations, I demonstrate
how to implement several canonical optimizations done by parallelizing
compilers. I have formalized this system and proofs in the Coq Proof
Assistant.
See other events happening in March 2013
