Paper Info
Title
Verifying local transformations on relaxed memory models
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 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- automated tool called Traver and used it to verify/falsify several compiler transformations for a number of different hardware memory models.
Year
DOI
Venue
2010
10.1007/978-3-642-11970-5_7
CC
Keywords
Field
DocType
novel proof methodology,concurrent shared-memory program,memory model,program fragment,local program transformation,specific hardware memory model,local transformation,sequential program,memory model relaxation,different hardware memory model,concurrent thread,shared memory
Programming language,Program transformation,Computer science,Denotational semantics,Compiler,Thread (computing),Theoretical computer science,Memory model,Distributed shared memory,Structural induction,Semantics
Conference
Volume
ISSN
ISBN
6011
0302-9743
3-642-11969-7
Citations 
PageRank 
References 
21
0.93
16
Authors
3
Name
Order
Citations
PageRank
Sebastian Burckhardt172534.72
Madanlal Musuvathi2168781.73
Vasu Singh31869.36