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

operations.

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.

PDF file

In  CC 2010: International Conference on Compiler Construction

Publisher  Springer Verlag
All copyrights reserved by Springer 2007.

Details