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

[Doug Lea]

On 03/17/2014 10:28 AM, Alan Jeffrey wrote:
> I thihk test cases 6 and 9 should also be in class C shouldn't they?

Oops. Somehow cases 9 and 9a got dropped from C.
And you are right that Case 6 is not strictly local (relying
on a local analysis in one thread to justify transformation in
another).

Also, if you want yet more, some C++ cases by Brian Demsky and Brian Norris
were in an attachment ("examples.pdf") in pre-list archives (but I
don't see them online anywhere).

>
> 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.

As implied in my reply to Peter, I'm not sure it is
critical that a memory model explicitly address optimizations
based on closed-system empirically-determined invariants.
JVMs never do this because of potential dynamic loading,
and there is no way this will ever change.
On the other hand, there doesn't seem to be a clear
borderline between these cases and other non-local
analyses.

-Doug