[jmm-dev] Is the JMM spec progressing?

[Hans Boehm]

On Sat, Aug 7, 2021 at 4:44 AM Doug Lea <dl at cs.oswego.edu> wrote:

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

But this now breaks some common idioms, right? In particular, I think a
bunch of
code assumes that racing assignments of equivalent primitive values or
immutable
objects to the same field are OK.

If, in 2004, our view of language-based security had been the same as it is
now,
then I completely agree that this would have been the right approach. But I
think
doing it now would require significant user code changes. Which might still
be the best way forward ...

Hans

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