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

[Doug Lea]

On 03/31/2014 09:01 AM, Peter Sewell wrote:
> http://www.cl.cam.ac.uk/~pes20/cpp/notes44.html  (Jean Pichon + Peter
> Sewell)

Great to see progress on this!

> At present it only covers reorderings, not eliminations

I'm not sure eliminations per se are a target?
If a read value is not used, or can only be one known value (where
"can" might require restricting possible executions), or is values
known to always/never satisfy a conditional, or can be only the value
obtained via another read (possibly due to aliasing), we don't need to
consider the read-event as removed. We could instead define a
substitution rule about how another value is used (if at all) instead
of the one read. (It might be convenient to formulate this by
requiring SSA form.) Similarly, while a write can be removed if no
read can readFrom it, I don't know a reason to explicitly
address this.

> The basic idea is to assume that compilers do not do inter-thread value range
> optimisations,

There seem to be some non-horrible ways to enable all inter-thread
analyses that might ever arise in practice: Allow actions of one
thread to be moved to another under any SC interleaving that preserves
liveness. Then they can be locally optimized via mechanics that we do
not need to spell out. (Then also allow actions to be moved back.)
The restriction to SC interleavings limits power but might be weakenable.
We briefly raised and (probably prematurely) dismissed variants of
these idea back in JSR133. One minor obstacle is that you'd need some
story about pre-transforming all dependencies on currentThread() and
derivatives to enable movement. Alternatively, the RAO "PR" rule
is basically the same idea but instead leaves things in place, and
allows global transformations. Pasting a version from old mail from
Vijay:

PR (Program Transformation) If q is a constraint on variables true at step f in
every SC execution, then replace f by g if g is q-equivalent to f and write-
and read-equivalent to f

* q-equivalent: for every store d satisfying q, f is defined iff g is, and f(d)=g(d)

* Say f reads from x if f read from x for some input store, and f writes v into
x if it writes v into x for some input store.

* write-equivalent: for every variable x and value v, f writes v for x iff g
writes v for x.

* read-equivalent: for every variable x, f reads from x iff g reads from x.