[jmm-dev] State of play with modeling relaxed memory
dl at cs.oswego.edu
Mon Mar 17 15:05:33 UTC 2014
On 03/17/2014 10:38 AM, Jeremy Manson wrote:
> 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
> (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.)
> 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
> 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
> 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
More information about the jmm-dev