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

[Alan Jeffrey]

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