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

Alan Jeffrey ajeffrey at bell-labs.com
Mon Mar 17 14:28:44 UTC 2014

I thihk test cases 6 and 9 should also be in class C shouldn't they?

Test 9 is particularly interesting. A similar variant of TC1 is to add a 
third thread:

Thread 1: r1 = x; if (r1 >= 0) { y = 1; }
Thread 2: r2 = y; x = r2;
Thread 3: x=-1;

Recall that the rationale for allowing r1==r2==1 is that inter-thread 
analysis could deduce that x is never negative, and so the if 
conditional is always true. Putting thread 3 into the picture 
invalidates this reasoning, but the JMM still supports the execution 

As a tangent... it seems that one of the issues here is that the 
rationale for including an execution is of the form "because of (...) we 
know that (...) cannot happen, and so (...) is allowed," for example 
plug in "inter-thread analysis", "x being negative" and "reordering the 
write y=1". The issue this raises is that such rationales are inherently 
non-monotone: the fact that behavior A cannot happen is enabling 
behavior B. Such non-monotone reasoning is OK if there's another 
induction principle around, e.g. step indexing allows induction on the 
number of execution steps. In the JMM there's no such global order of 
time so the induction principal is candidate execution number.


On 03/17/2014 08:23 AM, Doug Lea wrote:
> On 03/12/2014 10:19 AM, Alan Jeffrey wrote:
>> So, assuming that TC1 (and similar examples) still stands,
> Here are some notes on those test cases at
> http://www.cs.umd.edu/~pugh/java/memoryModel/unifiedProposal/testcases.html
> They can be placed in three categories:
> A. Tests for SC outcomes (including no out-of-thin-air)
>    Cases 4, 5, 10, 12, 13, 14, 15
> B. Tests involving local analysis/reorderings only for rationales:
>    Cases 2, 3, 6, 7, 11, 16
> C. Tests additionally requiring non-local optimizations and/or
>     compiler-directed scheduling:
>    Cases 1, 8, 17, 18, 19, 20, plus those at
>      http://www.saraswat.org/Test-variants.html
> Unless I'm mis-remembering something (very possible), all listed
> outcomes of those in Categories A and B should be uncontroversial.
> The listed outcomes for those in Category C were sometimes a matter of
> whether anyone could come up with a good story for them.  No Java
> conformance test (and surely no existing program) relies on them.
> Some of these cases reflect the realization late in the JSR133 process
> that initial justification rules didn't capture non-local
> optimizations. There was internal debate about whether to tweak them
> versus restart using the constraint-based approach that Vijay Saraswat
> later developed into RAO. Since the JSR133 spec was at that point
> overdue, there wasn't much choice. But I don't see any reason to
> think that any model can handle Category C cases in a uniform way
> (which might not exactly match the listed outcomes) without using a
> RAO-like approach. Which probably holds independently of whether
> expressed via Pomsets, Event Structures, or Mazurkeiwicz traces or
> whatever.
> -Doug

More information about the jmm-dev mailing list