[jmm-dev] Jmm revision status
viktor at mpi-sws.org
Fri Jul 18 10:19:31 UTC 2014
An update from our side: I'm attaching a draft version of the paper
that Peter mentioned.
In this paper, we show that the combination of dependency cycles with
the C11 treatment of non-atomic accesses is even more broken than ew
thought, in that it makes many standard source-to-source transformations
unsound (e.g., stengthening, expression evaluation linearisation,
roach motel reorderings).
We also found a few other technical problems with the C11 model
regarding the treatment of release sequences and SC atomics, also
preventing expected source-to-source program transformations.
We then survey a couple of fixes to the model, such as ruling out
(hb U rf) cycles, and prove (in Coq) a class of transformations
that are sound under these models.
-------------- next part --------------
More information about the jmm-dev