Sciweavers

CC
2010
Springer

Verifying Local Transformations on Relaxed Memory Models

13 years 10 months ago
Verifying Local Transformations on Relaxed Memory Models
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 challenging 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-autom...
Sebastian Burckhardt, Madanlal Musuvathi, Vasu Sin
Added 18 May 2010
Updated 18 May 2010
Type Conference
Year 2010
Where CC
Authors Sebastian Burckhardt, Madanlal Musuvathi, Vasu Singh
Comments (0)