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

[Doug Lea]

On 03/17/2014 10:59 AM, Alan Jeffrey wrote:
> The way I can imagine rescuing the Mazurkeiwicz trace semantics is by
> introducing something like constraint actions (C x:V) which constrains x to only
> have values from V. The semantics of read would then be:
>
>    sum_V (C x:V) . sum_(v in V) (R x=v) . P
>
> The requirements for a valid execution would then include that for any
> constraint action (C x:V) and any visible write action (W x=w), we have w in V.

Have you thought about the rules for resolving constraints?
On the one hand, you'd like some self-referentialness.
On the other hand: cycles.

-Doug

> Such a model should support TC1 since the semantics of thread 1 would be:
>
>    sum_V (C x:V) . Q_V
>
> where:
>
>    Q_V = sum(v in V) (R x=v) . P_v
>    P_+n = (W y=1)
>    P_-n = 0
>
> In particular:
>
>    Q_{0,1}
>      = sum(v in {0,1}) (R x=v) . P_v
>      = sum(v in {0,1}) (R x=v) . (W y=1)
>      = (W y=1) . sum(v in {0,1}) (R x=v)
>
> which allows the write action to move before the read, and the rest is routine.
>
> James and I sketched out such a model, but abandoned it because it was looking
> pretty cumbersome with its additional constraint actions. It might be worth
> rescuing if the alternatives are looking just as inelegant though.
>
> A.
>
> On 03/15/2014 01:23 PM, Doug Lea 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. 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
>>
>