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

[Doug Lea]

On 03/31/2014 01:20 PM, Peter Sewell wrote:
> 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
>>> Sewell)

>>> 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.

Removing an unused access should not be too interesting in itself.
The same visible outcomes should be allowed whether you actually remove
them or not. So the interesting part is introducing substitutions
that cause accesses to not be used.

>>
>>
>> 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.
>
> Not sure I really understand what you mean there.  Got a slightly
> concrete example in mind?

Not that any of them are realistic, but see TC1 and some others at
   http://www.cs.umd.edu/~pugh/java/memoryModel/unifiedProposal/testcases.html

The main idea is that by "manually" time-slicing across
threads, you can reduce whole-program inter-thread analysis
to whole-program intra-thread analysis, but only under
closed-world SC. Of all possible global analyses,
one would think that at least this form should be allowed.
And in fact, taken alone, it seems always allowable
in any plausible memory model.

The uncertain part is whether and how you can apply
value constraints etc from such an analysis to
non-SC executions. A quick first stab at this in
the style of your or Alan's approaches looks problematic,
so I'll explore more before further commenting.

-Doug