Re: JavaMemoryModel: Questions about the proposed semantics

From: Bill Pugh (pugh@cs.umd.edu)
Date: Wed May 09 2001 - 16:05:44 EDT


>
>I have, however, a problem understanding why Execution 2 is
>permitted. The first operation (x=1 in Ex1, x==1 in Ex2) can be
>placed substantially far away from operations 2 and 3. In this case,
>from the point of view of the compiler, second parts of Exs 1 and 2
>are indistinguishable. If Ex2 is permitted because compiler ignores
>some aliasing, then Ex1 should also be permitted.

Execution 1 is not permitted by the model unless there is an
improperly synchronized write of 1 to x. I am assuming you are
excluding that possibility.

For execution 2:

1. x==1
2. x=2
3. x==1

I assume x==1 means that x was read and found to be equal to 1.

In order for something like this to happen, we have to establish a
larger context. Unless there is an improperly synchronized write to
x, execution 2 cannot happen.

Assume the situation is as follows:
Execution 2:

Initially: x = 0

Thread 1:
x = 1

Thread 2:
x == 1
x = 2
x == 1

OK, I'm not sure what situation would actually cause this to happen,
although I won't rule it out in some DSM implementations. But if you
really want to forbid this situation in general, then you open up a
whole can of worms. For example, is the "knowledge" that x=1 has been
overwritten transitive? In other words, can the following situation
happen:

Execution 3:
Initially: x = 0

Thread 1:
x = 1
unlock B

Thread 2:
x == 1
x = 2
x != 1 // here I mean that x must not be equal to 1 at this point, since
        // we decided that execution 2 is prohibited
unlock A

Thread 3
lock A // obtains the lock after it has been released by thread 2
lock B // obtains the local after it has been released by thread 1
x == 1

Here, I would be much more worried about whether or not a DSM
implementation might allow execution 3 to occur; I suspect it could.

The real point is that the semantics are defined by:
Semantics A:
   * sequentially consistent behavior for correctly synchronized programs
   * the bare minimum of additional constraints needed for safety and security
     (including safe immutable objects)

The semantics are not defined by:
Semantics B
   * Semantics A, plus:
   * Any behavior that could be caused by a (known or conceivable?) compiler
        or architectural optimization is allowed
    * All other reorderings are forbidden.

We went back and forth on this about a year and a half ago, and I
(and others) settled on Semantics A. The problem is that explaining
the additional implementation strategies allowed to Java programmers
by Semantics B would be very, very difficult, and that 98% of the
programmers who tried to make use of the additional freedom offered
by B would get it wrong and would write something that is broken even
according to semantics B. On the other hand, Semantics A is
(relatively) easier to explain, and people who try to write correctly
synchronized programs have a better chance of writing correct
concurrent software. Thus, Semantics A is a better strategy for
encouraging the development of reliable concurrent software.

At 8:21 PM -0700 5/9/01, Alex Gontmakher wrote:
>All I wanted to say is "hey, a programmer can think this and DO
>THIS" (I do not claim *I* would do this).

Java programmers should be informed, over and over again:
   Incorrectly synchronized programs have nonintuitive and even
malicious semantics. They will conspire to make your software fail
just when you are demonstrating it before your most important client,
or just before your IPO. Do not try to reason about what the compiler
might do. Use the mechanisms provided by the language
(synchronization, volatile, perhaps atomic reads/writes of references
to immutable objects?) to communicate between threads.

[The "perhaps" comes from some continuing discussion as to whether
the immutable object trick is a recommended programming idiom, or
simply a fall-back safeguard for security].

For the other program:

Initially: i = NEGINF and k = NEGINF

Thread 1:
while (i < POSINF) i++

Thread 2:
while (true) {
   assert k <= i;
   k = i;
   }

The is essentially the same as the reads-kill example. One thread is
incrementing a variable, another thread is reading that variable over
and over. If you require that the second thread see a monotone
sequence, you are requiring that reads kiil, and we know that isn't
acceptable in the semantics for Java.

>
>The question is "Can this program get to execute the OUCH"?
>The proposed spec permits it.
>Original Java is Coherent, so it forbids that. As far as I
>understand, it is also forbidden in CRF.

No, CRF also allows the assertion failure (i.e., the OUCH). The
compiler can freely reorder the LoadR's of i (across multiple
iterations of the loop in thread 2).

>In other words, the syntactic information from the program gives
>more information than just the order of memory access operations.
>Your definition (admittedly, like any other) chooses to ignore this
>information.

I don't think it is possible to incorporate the idea of "names" into
the semantics, and have one rule for when two references to a
variable have the same "name", and another rule for when two
references to a variable have different "names". This is particularly
true in Java, where so few "names" are static. Almost all references
are going through the "this" pointer or some other pointer, so
defining when two references are the same "name" gets very tricky.

>Either this execution is marked as possible, even though it is
>non-intuitive and looks impossible on any currently imaginable
>system, or the spec must be changed in such a way so as to make it
>forbidden.

The execution is incorrectly synchronized. Well written programs
should never depend on the meaning of incorrect synchronization.

At 8:21 PM -0700 5/9/01, Alex Gontmakher wrote:
> > Our proposed spec (and all of the others) doesn't discuss aliasing, and
> > just deals with the memory model on the level of memory accesses. Aliasing
> > is a syntactic issue, as you say: our spec deals (almost exclusively) with
> > the JVM, not the Java language.
>
>I admit I do not really understand it. Isn't it the programmer who has
>to write the (correct) multithreaded programs? What good is the (supposedly
>multithreaded) language to the programmer if its memory semantics are
>not specified?

This isn't really significant. The problem is that you need to define
a semantics for both JVM's and for Java source programs. Our spec is
written in terms of the JVM, and the spec for Java source programs is:

>Informally, the semantics of Java source programs is understood to be defined
>by their straightforward translation into classfiles, and then by
>interpreting the classfiles using the JVM semantics.

This will have to be cleaned up as part of the JSR process, but
hopefully the intention is fairly clear.



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