@inproceedings{burckhardt2010verifying,
author = {Burckhardt, Sebastian and Musuvathi, Madanlal and Singh, Vasu and Musuvathi, Madan},
title = {Verifying Local Transformations of Concurrent Programs},
booktitle = {CC 2010: International Conference on Compiler Construction},
year = {2010},
month = {March},
abstract = {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.},
publisher = {Springer Verlag},
url = {http://approjects.co.za/?big=en-us/research/publication/verifying-local-transformations-of-concurrent-programs/},
edition = {CC 2010: International Conference on Compiler Construction},
}