[jmm-dev] avoiding thin-air via an operational out-of-order semantics construction
Peter.Sewell at cl.cam.ac.uk
Mon Mar 31 17:20:31 UTC 2014
On 31 March 2014 15:30, Doug Lea <dl at cs.oswego.edu> wrote:
> On 03/31/2014 09:01 AM, Peter Sewell wrote:
>> http://www.cl.cam.ac.uk/~pes20/cpp/notes44.html (Jean Pichon + Peter
> Great to see progress on this!
>> At present it only covers reorderings, not eliminations
> I'm not sure eliminations per se are a target?
Some eliminations could enable other reorderings, so (except perhaps
for ACCESS_ONCE) I think we have to deal with them.
> 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
> 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
Not sure I really understand what you mean there. Got a slightly
concrete example in mind?
> 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
> PR (Program Transformation) If q is a constraint on variables true at step f
> 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
> * Say f reads from x if f read from x for some input store, and f writes v
> 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.
More information about the jmm-dev