RE: JavaMemoryModel: Draft JMM Synopsis

From: Doug Lea (dl@cs.oswego.edu)
Date: Sun Mar 07 2004 - 10:55:49 EST


> I am not sure what "complete strictly" means,

I had tried to avoid the term "happens before" here. It is a crummy
term. It is a good idea to use the term in the spec to clarify
relations to other memory model work; plus it is mainly expressed in
symbols anyway. But it seems needlessly confusing to say things like
"an unlock happens before a subsequent lock".

But my attempt to use "complete" here was completely(!) wrong, and led
to lots of misstatements. The best alternative I can think of for "i
happens before j" is "the effects of i occur before those of j". Which
seems too verbose, and might still have unwanted connotations for some
readers. Does anyone have any better suggestions?

For now, here's a second pass phrased in this way, with other
corrections and some minor reorganization:

...

The Java Memory Model (JMM) may be seen as an extension of the basic
within-thread expression and statement evaluation rules described in
the bulk of the Java Language Specification (JLS). JLS expression
rules state, for example. that a given thread evaluates any expression
left to right.

The JMM provides additional rules governing whether the "memory
actions" in a program may be performed in parallel or out of
order. Memory actions are reads, writes, locks and unlocks, along with
operations on java.util.concurrent.atomic variables. A write
corresponds to the assignment of a variable (i.e., field or array
element) that modifies (only) that variable, and a read obtains a
value from some write that does not happen after this read. Reads and
writes for all kinds of variables except non-volatile longs and
doubles are atomic, that is reads never return the values from
partially completed writes. Lock and unlock actions are entries and
exits of synchronized blocks or methods, or explicit lock() and
unlock() operations on java.util.concurrent.locks.

The JMM is defined in terms in terms of a happens-before relation that
provides ordering rules for the effects of memory actions. If action
A falls under the happens-before relation with respect to action B,
then compilers, processors, and memory subsystems must preserve their
ordering. For example, if A is a write and B is a read of the
variable written, and the pair fall under the happens-before relation,
and there are no other intervening writes, then the read in action B
must return the value written in action A. But if the pair does not
fall under this relation, then the read might or might not return this
value.

The happens-before relation extends the JLS within-thread expression
and statement evaluation rules, so these rules are at all times
honored, consistently across all threads. Rigorously specifying what
is meant by "consistently" in cases that entail apparent circularities
and the like turns out to be challenging. See JLS chapter 17 for these
and other details, many of which describe minimal properties of code
that is not correctly synchronized as well as other corner cases that
are best avoided. More relevantly, the following rules derived from
the specification may be of use when ensuring that code is correctly
synchronized.

Initialization

  * The initial action for any field is a write of its default (zero
    or null) value. The effects of this write occur before those of
    any reads of this field by any thread.

  * The effects of the write to a static final field occur before
    those of any read of this field by any thread. (There are special
    exceptions for setting System.{in,out,err}.)

  * The effects of the write to a nonstatic final field by a thread
    occur before those of any subsequent write of a reference to the
    new object with this field by that thread.

Access

  * The effects of an unlock or volatile write to a variable occur
    before those of any subsequent lock of that lock or volatile read
    of thet variable.

  * The effects of a volatile read or lock by a thread occur before
    those of any subsequent memory action by that thread.

  * The effects of all memory actions by one thread occur before any
    subsequent volatile write or unlock by that thread, with respect
    to any other thread that reads the same volatile variable or locks
    the same lock.

  * The effects of thw first read of a reference to an object by a
    thread occur before those of any subsequent read by that thread of
    any of the object's final fields.

Atomics

  * The effects of a java.util.concurrent.atomic get() operation are
    the same as a volatile read, and those of a set() are the same as
    a volatile write.

  * The effects of a weakCompareAndSet by a thread occur before those
    of any subsequent access to that atomic variable by that thread.

  * The effects of a compareAndSet, along with other atomic
    read-and-update methods, fall under the memory rules for a
    volatile read followed by a write.

Threads

  * The effects of all writes by a thread performed prior to invoking
    Thread.start() for a new Thread occur before those of any reads of
    these written variables by that new Thread.

  * The effects of all writes by a thread occur before termination of
    that thread. (Another thread can only reliably detect termination
    by using Thread.isAlive() or Thread.join().)

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



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