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

[Alan Jeffrey]

The rule would be something like the following...

s satisfies constrains whenever, for any valid permutation of s, and an 
action a in that permutation, the previous action is compatible with a.

This depends on a notion of compatibility of actions, which would be 
something like (W x=v) is incompatible with (C x:V) whenever v not in V.

This definition (together with the old one) seems to allow TC1 and TC8 
but not TC9 or TC 18. It doesn't allow thin-air reads.

The main annoyance I've spotted so far is that it doesn't validate an 
optimization which replaces a read by the value last written by the same 
thread, for example:

Thread 1: r1=x; x=2; r3=x; if(r3==2){ y=1; }
Thread 2: r2=y; x=r2;

The execution where r1==r2==1 isn't allowed because the constraint 
action (C x:{2}) isn't compatible with the visible write action (W x=1) 
from thread 2. Really you should be able to optimize (x=2; r3=x; P) to 
(x=2; r3=2; P), which would allow the y to be reordered.

This could probably be patched, but at the cost of extra complexity to 
the model.

A.

On 03/17/2014 12:06 PM, Doug Lea wrote:
> 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
>>>
>>
>