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

[Doug Lea]

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