[jmm-dev] State of play with modeling relaxed memory

[Doug Lea]

On 03/15/2014 02:28 PM, Peter Sewell wrote:
> On 15 March 2014 18:23, Doug Lea <dl at cs.oswego.edu> wrote:
>> On 03/12/2014 10:19 AM, Alan Jeffrey wrote:
>>>
>>> Ah yes, I owe the world a status report...
>>>
>>> I looked into modeling relaxed memory using Mazurkeiwicz traces, that is
>>> strings
>>> of actions up to appropriate reorderings. My main result here is negative,
>>> in
>>> that you can build a model of memory, and get it to support speculative
>>> write,
>>> in that:
>>>
>>>                 r=x; y=1  ==  y=1; r=x
>>>     if(b){y=1;}else{y=1;} == y=1
>>>
>>> The justification for speculative write is:
>>>
>>>     sum_i a_i . b . P  ==  b . sum_i a_i . P
>>>
>>> when b is independent of every a_i. The problem with this model is that it
>>> only
>>> supports a speculative write w when every branch performs w. In
>>> particular, it
>>> doesn't support causality test case 1:
>>>
>>>     thread 1: r1 = x; if (r1 >= 0) { y = 1; }
>>>     thread 2: r2 = y; x = r2;
>>>
>>> The trace semantics of thread 1 is:
>>>
>>>     P = sum_v (R x=v) . P_v
>>>
>>> where
>>>
>>>     P_+n = (W y=1)
>>>     P_-n = 0
>>>
>>> Since some P_v doesn't perform (W y=1), P can't perform (W y=1) before (R
>>> x=v).
>>>
>>> So, assuming that TC1 (and similar examples) still stands, I don't see how
>>> to
>>> get a Mazurkeiwicz trace model to fly.
>>
>>
>> Where TC1 is from
>> http://www.cs.umd.edu/~pugh/java/memoryModel/unifiedProposal/testcases.html
>>
>> The "human" rationale given for allowing r1 == r2 == 1 is that,
>> via whole program analysis, a compiler could determine that
>> x and y are always non-negative.
>
> Is this an analysis that production compilers actually do, or more hypothetical?
>

JVM JITs do not perform whole program analysis (so surely
not inter-thread whole program analysis) because new classes
may be dynamically loaded at any time.

There may be off-line bytecode optimizers that can perform some
global analysis for "sealed" programs (those for which there is
some extra guarantee about no further dynamic loading).

-Doug


> Peter
>
>
>> Given this, TC1 acts as:
>>    thread 1: r1 = x; y = 1;
>>
>>    thread 2: r2 = y; x = r2;
>> which seems unchallenging.
>>
>> You'd think that any memory model that handled this sort of case
>> would explicitly incorporate/allow the global analysis that led to
>> its rationale. RAO does so. It's surprising that the JSR133
>> model doesn't, but we don't think this generalizes completely.
>>
>> So, it is not clear to me that you've shown a fatal flaw in Mazurkeiwicz
>> trace based mechanics per se.
>>
>> -Doug
>>
>