[jmm-dev] Optimizing external actions in the JMM

[Sanjoy Das]

Hi Nitsan,

Nitsan Wakart wrote:
 >>> The thing is you define:
 >
 >>> "external action that... always returns 42 and has no other effect"
 >> I didn't mean to say that it "always returns 42 and has no other
 >> effect" by the spec, but that the compiler knows it "always returns 42
 >> and has no other effect" by some external knowledge it has about `f`
 >> (and perhaps the environment).
 >
 >
 > If the JIT compiler KNOWS, then it knows, job done. Same way it knows Math.pow is not external.

I'm trying to justify precisely the "job done" bit. :) Specifically,
can it replace f(x) with 42 even if it knows that given the current
environment the "external action" f(x) always returns 42 and has no
other effect?

Math.pow(a, b) is fundamentally different than f(x) =
Unix_open("/home/foo" + x) -- it can be evaluated for any a, b
independent of the environment.  This isn't true for f(x) as defined:
in the previous example the JIT knows that f(x) returns -1 and has no
other effect _because_ it knows that the process is being run as user
"bar".  This information is not present in the execution trace, so we
can't "evaluate" f(0) to justify the write of -1 to y.

 >>> - Unsafe.get*(long address)/Unsafe.get*(null, long address): don't fullfil 1
 >> Under this interpretation the Unsafe.get*() intrinsics have a corner
 >> case -- if they're being called on a mmapped file (or uninitialized
 >> memory, even) then the value returned by them is not specified by the
 >> memory model (to be precise: whether a certain value returned by the
 >> call is correct is not decidable in the JMM).  This hints that they
 >> need to be modeled as external actions; moreover, I think that (1)
 >> really means "*may* be observable" and not "*has to be* observable".
 >
 >
 > Where behaviour is undefined, it is down to precedent and sensibility...

That's fine (especially given that s.m.Unsafe is an internal API), but
how do you "plug in" the precedent and sensibility into the rest of
the memory model?  IOW, in (say)

Thread1:
   addr = mmap_file();
   r1 = unsafe.getByte(addr);
   this.y = r1
   this.volatileF = r1

Thread2:
   r2 = this.volatileF;
   r3 = this.y

when trying to prove things about the r3 + r2 (say) how do you model
r1?  Given that r1's value cannot be described by the JMM, it seems
reasonable to me to give it a sensible value intuitively, but in the
JMM model it as an external action that happens to return that
sensible value.

 > How is a 'read' "observable outside the execution"?

Its usually not, it sounded like you were interpreting "observable
outside of execution" as a necessary condition for an action to be a
side effect, when I think observability is sufficient but not
necessary for an action to be considered an external action.  That is
likely the reason for saying "may be observable outside of an
execution" and not "has to be observable outside of an execution".

 > Consider the following code:
 > ----
 > long address = Unsafe.allocate(1024);
 > int i = 1;
 > Unsafe.putInt(address,i);
 > return Unsafe.getInt(address) == i; // might as well return true;
 > -----