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.
- Non-multi-copy-atomic 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 non-multi-copy-atomic 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 high-level 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 (MPI-SWS)
- Viktor Vafeiadis (MPI-SWS)
Coq formalization
- Download the formalization [trns-1.0.zip] [README.txt] [CHANGELOG.txt]
- Browse the formalization online [proofs hidden] [proofs visible]