Explaining Relaxed Memory Models with Program Transformations
Summary
Weak memory models determine the behavior of concurrent programs. While they are often understood in terms of reorderings that the hardware or the compiler may perform, their formal definitions are typically given in a very different style—either axiomatic or operational. In this work, we investigate to what extent existing memory models can be specified in terms of reorderings and other program transformations. We have established the following results:
 TSO is equivalent to a set of two local transformations over sequential consistency.
 Nonmulticopyatomic models (such as C11, Power and ARM) cannot be explained in terms of local transformations over sequential consistency.
 Reordering of independent accesses accounts for all the relaxed behaviors of Power (restricted to the fragment without control fences) over a basic nonmulticopyatomic model account.
 ARM's relaxed behaviors, however, cannot be explained in a similar way.
Our positive results may be used to simplify correctness of compilation proofs from a highlevel language to TSO or Power.
Paper

Ori Lahav and Viktor Vafeiadis.
Explaining Relaxed Memory Models with Program Transformations.
In FM 2016: 21st International Symposium on Formal Methods, 2016.
People
 Ori Lahav (MPISWS)
 Viktor Vafeiadis (MPISWS)
Coq formalization
 Download the formalization [trns1.0.zip] [README.txt] [CHANGELOG.txt]
 Browse the formalization online [proofs hidden] [proofs visible]