[jmm-dev] avoiding thin-air via an operational out-of-order semantics construction

[Peter Sewell]

Dear all,

building on the summary of the thin-air problem that we sent around
earlier (http://www.cl.cam.ac.uk/~pes20/cpp/notes42.html, Mark
Batty+Peter Sewell),  we've sketched a semantics that gives the
desired non-thin-air behaviour for at least some examples, for
C11-style relaxed atomics / Linux-C ACCESS_ONCE accesses / Java
volatiles.   At present it only covers reorderings, not eliminations
and introductions, though we think it can probably be extended to
those.

The basic idea is to assume that compilers do not do inter-thread
value range optimisations, using that to let us construct a
thread-local out-of-order operational semantics out of a conventional
thread-local (value-passing) labelled transition system. We then
combine the resulting thread semantics with an operational
non-multi-copy-atomic storage subsystem, as in our PLDI11 Power model,
to be sound w.r.t. Power and ARM hardware.  The result is (we think)
attractively simple to understand.   The big question is whether that
assumption is reasonable (or can be made so),  and we'd welcome
thoughts on that.

The semantics is described here:

http://www.cl.cam.ac.uk/~pes20/cpp/notes44.html  (Jean Pichon + Peter Sewell)

(we've also got a formal version in Lem and a command-line prototype
tool for exploring it).

Comments would be very welcome

Jean + Peter