Sebastian Burckhardt, Madanlal Musuvathi, and Vasu Singh
25 March 2010
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.
|Published in||CC 2010: International Conference on Compiler Construction|
All copyrights reserved by Springer 2007.