RE: JavaMemoryModel: Ordering of volatile and monitor actions

From: Jeremy Manson (jmanson@cs.umd.edu)
Date: Mon Jul 02 2001 - 14:04:10 EDT


> >
> > Reordering a monitorexit and a finite number of volatile reads may
> > fall into the category of something that is illegal in the semantics,
> > but can't be observed so is legal in the implementation.
>
> This really should not be an issue. The *semantics* should be specified in a
> way that all implementations are legal. (Hence the previous suggestion of
> giving up on per-process orderings as a way to specify the semantics.)
>

I would like to clarify this a tad, if I may, because I think it is an
important-ish issue. In our semantics, we say :

A JVM implementation is legal iff for any execution observed on the JVM,
there is an execution under these semantics that is observationally
equivalent.

This means that the possible results of a program on a "real" JVM have
to be a subset of the possible results of a program executed under our
semantics. I think this is the right way to go.

For example, if our semantics doesn't explicitly mention, say, removal
of thread-local synchronization, that doesn't mean it is "illegal".
The same is true for reordering a monitorexit and a finite number of
volatile reads. What it does mean is that an implementation must
perform that reordering in such a way as to obtain a result that would
be obtainable on our semantics.

In horrible pedant mode, I think I should also point out that not all
implementations are going to end up legal. For example, if you have the
code:

Initially, i = 0

thread 1: thread 2:

for (i = 0; i < array.length; i++) i = 4;
  array[i] = 2;

Here, i can be modified by another thread. We assume your
implementation doesn't prevent i from being modified by another thread
for the duration of the loop by doing something like sticking it in a
register. An implementation would not be free to optimize away the
bounds check on the read of array.

                                        Jeremy
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:32 EDT