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

[Doug Lea]

On 03/17/2014 10:38 AM, Jeremy Manson wrote:
> Doug,
>
> I'm not getting a good read on your responses here - are you arguing that we
> shouldn't support Category C anymore?  They don't really seem *that*
> controversial; just because nothing actually performs these optimizations
> doesn't mean that they aren't reasonable optimizations to perform.  It is just
> that very few optimizers do any sort of whole program analysis.

I'm saying that the JSR133 justification sequence rules
can approximate the effects of an inter-thread whole-program optimizer.
It is apparently a pretty good approximation: most of the outcomes
seem consistent with the results of conceivable actual optimizers.
But sometimes mysteriously so. For example case 18 and its variants.
Or Alan's just-posted TC1 variant.

The only cure I know is to explicitly model non-local
analyses/transformations via constraint satisfaction or
something equivalent.

-Doug


>
> (I'm not sure that there was anything wrong with our treatment of Category C in
> the JSR133 model, either, although that is probably not entirely relevant.)
>
> Jeremy
>
>
> On Mon, Mar 17, 2014 at 6:23 AM, Doug Lea <dl at cs.oswego.edu
> <mailto:dl at cs.oswego.edu>> 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
>     <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
>     <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
>
>
>