[jmm-dev] Optimizing external actions in the JMM

[Sanjoy Das]

Hi,

I'm stuck trying to model a certain kind of execution in the JMM, and
was wondering if people here can help.

Let's say we have a program like this:

x == y == 0 initially

ThreadA:
  r1 = x
  r2 = f(r1)
  y = r2

ThreadB:
  r3 = y
  x = r3

where f is some external action that the compiler understands.  If the
compiler knows `f` always returns 42 and has no other effect, can it
optimize ThreadA to

ThreadA:
  r1 = x
  r2 = 42 // f(r1)
  y = r2

and then to

ThreadA:
  r2 = 42 // f(r1)
  y = r2
  r1 = x

thereby introducing a OOTA-like value of 42 into the system?

Given how the JMM is phrased, in cases like say, f(x) == (x - x) + 42,
(i.e. `f` is _not_ a external action) I'd proceed to justify r1 = r2 = r3 = 42
by:

 1. Committing the initial writes of 0 to x and y in E0
 2. Adding the load of r1 as 0 to E1 (but not committing it) and
    committing the write of 42 to y (justified since f(0) = 42) in E1
 3. Nothing in E2
 4. Now the load from y == r3 can see the write committed to y in E1,
    so commit the read r3 and the write of 42 to x in E3
 5. Nothing in E4
 6. In E5, finally commit the read from x == r1, which can see 42 now

However, if `f` is a side-effecting operation, then I don't see how I
can reason about `f(0)` in step 2 inside the memory model.  As far as
the JMM goes, `f` is a black box, and the only thing known about it
given the trace (with the OOTA-like behavior) is that "f(42) == 42".
This is fine for the vast majority of external actions that are black
boxes to the compiler also.  But `f` could be a routine in (say)
DirectByteBuffer that touches native memory under the hood; and the
compiler could very well be in a position to fold loads from native
memory (that aren't modeled in the JMM AFAICT, and thus appear as
"external actions").

Another potentially problematic definition for `f(x)` is:

  f(x) =
    // JNI_GetEnv is the "external action" here but the JIT
    // knows that no loaded class calls `setenv`, so it is safe to assume
    // that JNI_GetEnv is invariant for an invariant argument.
    String EnvVar = "VAR_" + Integer.toString(x);
    if (JNI_GetEnv(EnvVar) == JNI_GetEnv(EnvVar))
      return 42;
    return 90;

It is perhaps not too unreasonable to teach the compiler to fold `f`
above to "return 42", and then optimize ThreadA to enable "r1 = r2 =
r3 = 42".  But justifying this in the JMM is difficult -- I'll end up
having to justify that f(0) is 42, and that is difficult to do just by
considering reads, writes and results of external actions already
present in the trace.

It seems to me that this isn't just a problem with the current JMM,
but is a general issue with a JMM that is phrased as a predicate on a
program trace -- a predicative memory rules out the compiler from
optimizing external actions as first class entities.  Is that
accurate, or am I off base?

Thank you for your time!
-- Sanjoy