[jmm-dev] Is the JMM spec progressing?

[Doug Lea]

(Henceforth, let's drop jdk-dev and move this to jmm-dev.)

On 8/7/21 5:27 AM, Andrew Haley wrote:
> On 8/6/21 11:32 PM, Hans Boehm wrote:
>
>> Probably even more controversially, I think we've realized that
>> existing compiler technology can compile such racing code in ways
>> that some of us are not 100% sure should really be allowed.
> This implies, does it not, that the problem is not formalization as
> such, but that we don't really understand what the language is
> supposed to mean? That's always been my problem with OOTA: I'm unsure
> whether the problem is due to the inadequacy of formal models, in
> which case the formalists can fix their own problem, or something we
> all have to pay attention to.

Yes. My stance in the less formal account 
(http://gee.cs.oswego.edu/dl/html/j9mm.html) as well as Shuyang Liu et 
al's ongoing formalization (see links from 
http://compilers.cs.ucla.edu/people/) is that the most you want to say 
about racy Java programs is that they are typesafe. As in: you can't see 
a String when expecting an int. Even this looser constraint is 
challenging to specify, prove, and extend. But it is a path for Java 
that might not apply to languages like C that are not guaranteed 
typesafe anyway, and so enter Undefined Behavior territory (as opposed 
to possibly-unexpected but still typesafe behavior).

-Doug



>
>> Demonstrably unexecuted code can affect the semantics in ways that
>> strike me as scary. (See wg21.link/p1217 for a down-to-assembly C++
>> version; IIUC, Lochbihler and others earlier came up with some
>> closely related observations for Java.)
> Looking again at p1217, it seems to me that enforcing load-store
> ordering would have severe effects on compilers, at least without new
> optimization techniques. We hoist loads before loops and sink stores
> after them. When it all works out, there are no memory accesses in the
> loop. A load-store barrier in a loop would have the effect of forcing
> succeeding stores out to memory, and forcing preceding loads to reload
> from memory. It's not hard to imagine that this would cause an
> order-of-margnitude performance reduction in common cases.
>
> I suppose one could argue that such optimizations would continue to be
> valid, so only those stores which would have been emitted anyway would
> be affected. But that's not how compilers work, as far as I know. In
> our IR for C2, memory accesses are not pinned in any way, so the only
> way to make unrelated accesses execute in any particular order is to
> add a dependency between all loads and stores.
>