[PRL] Fwd: [MIT-PL] TALK:Wednesday 3-13-13 PL/SE Seminar: Proving the Correctness of Parallelizing Optimizations

[Mitchell Wand]

---------- Forwarded message ----------
From: Csail Event Calendar <eventcalendar at csail.mit.edu>
Date: Wed, Mar 13, 2013 at 12:01 AM
Subject: [MIT-PL] TALK:Wednesday 3-13-13 PL/SE Seminar: Proving the
Correctness of Parallelizing Optimizations
To: pl at csail.mit.edu



PL/SE Seminar: Proving the Correctness of Parallelizing Optimizations
Speaker: CJ Bell
Speaker Affiliation: Princeton University
Host: Adam Chlipala
Host Affiliation: CSAIL

Date: 3-13-2013
Time: 4:00 PM - 5:30 PM
Location: 32-D463 (Star)

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.

Relevant URL(S): http://www.cs.princeton.edu/~cbell/
For more information please contact: Adam Chlipala, adamc at csail.mit.edu

_______________________________________________
Pl mailing list
Pl at lists.csail.mit.edu
https://lists.csail.mit.edu/mailman/listinfo/pl
http://projects.csail.mit.edu/pl
-------------- next part --------------
HTML attachment scrubbed and removed