[jmm-dev] Jmm revision status

[Viktor Vafeiadis]

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.

Best,
Viktor

-------------- next part --------------