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

[Doug Lea]

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