JavaMemoryModel: Update to Java Memory Model spec

From: Bill Pugh (pugh@cs.umd.edu)
Date: Fri Jun 04 2004 - 22:00:47 EDT


OK, we've updated the JMM spec:
        http://www.cs.umd.edu/~pugh/java/memoryModel/jsr133.pdf

There was only one real change, which involved how we handled unbounded
executions.

We don't think anything we did changed the behaviors that are intended
to be allowed. However,
we found that formally describing the behaviors that are allowed is
more subtle that
we had thought.

For example, consider

Non-terminating example 1
thread 1:
while (true)
   print "hello"

Non-terminating example 2
Initially, both v1 and v2 are volatile and equal to 0

Thread 1:
while (v1 == 0) {
   print "hello"
   v2++;
   }

Thread 2:
v1 = 1
r1 = v2

We want to allow example 2 to exhibit the same behavior as example 1.
However, example 1 has only infinite executions, and example 2 has only
finite
(but unbounded) executions. The reason that example 2 has only finite
executions
is that the read of v2 in thread 2 must occur at some point, and only a
finite number of
writes to v2 can occur before it (otherwise, we couldn't say which
write is seen
by the read of v2 in thread 2).

So we found a way to allow example 2 to exhibit the same behavior as
example 1.
(read the spec to see how).

Let me describe just one more example.

Non-terminating example 3:

Initially, v is volatile and v = 0

thread 1:
while (v == 0);
print "1"

thread 2
v = 1
print "2"

This program is allowed to hang (run for an unbounded time without
printing anything
or terminating), and it is allowed to print "1" and "2" and terminate.
It may not print "2" and
then run for an unbounded time.

Hans Boehm provided a lot of useful feedback as did Doug Lea. I'm
hoping that
Sarita and others will be able to take a close look at the new material
on observable
behaviors and nonterminating executions over the next few days.

We always welcome feedback, questions and criticism. Unless something
very surprising
turns up, this is the last revision until the JMM emerges from its
chrysalis as a chapter of
the JLS.

Bill and Jeremy

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



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