Verifying Local Transformations of Concurrent Programs

Sebastian Burckhardt, Madanlal Musuvathi, and Vasu Singh


The problem of locally transforming or translating programs

without altering their semantics is central to the construction of correct

compilers. For concurrent shared-memory programs this task is chal-

lenging because (1) concurrent threads can observe transformations that

would be undetectable in a sequential program, and (2) contemporary

multiprocessors commonly use relaxed memory models that complicate

the reasoning.

In this paper, we present a novel proof methodology for verifying that a

local program transformation is sound with respect to a specific hardware

memory model, in the sense that it is not observable in any context. The

methodology is based on a structural induction and relies on a novel

compositional denotational semantics for relaxed memory models that

formalizes (1) the behaviors of program fragments as a set of traces,

and (2) the effect of memory model relaxations as local trace rewrite


To apply this methodology in practice, we implemented a semi-automated

tool called Traver and used it to verify/falsify several compiler transfor-

mations for a number of different hardware memory models.


Publication typeInproceedings
Published inCC 2010: International Conference on Compiler Construction
PublisherSpringer Verlag
> Publications > Verifying Local Transformations of Concurrent Programs