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

[Peter Sewell]

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?

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
>