Hi!
This is the second note sent to JMM mailing list from Vivek Sarkar
(IBM Research) and myself. The first email, "Is memory coherence
necessary in the new JMM?" was sent on July 23 where we mentioned
Location Consistency as an example of a memory model which does not
rely on "coherence":
We have been working on the specification of memory models that do not
rely on memory coherence. One such model that we proposed in 1993 is
called Location Consistency (LC). (See www.capsl.udel.edu/LC.shtml
for details.)
We'd like to make a few comments to follow up on Bill Pugh's proposed
memory model (Oct. 22nd, copy included below):
1. We are pleased to see that the LC model is being considered seriously
as input for defining the new Java memory model.
2. Bill's proposed model (Oct. 22 version) is close but not identical to
LC. Here is the example we
discussed with Bill recently by email (Bill's example):
Initially, a=b=0
Thread 1 Thread 2
x = a y = b
b = 1 a = 1
Under LC it is possible in to get x=y=1. Under Bill's model, however,
it is impossible to get this answer. As Bill clarified in his 10/26
reply
to Rick Hudson, the source of the difference lies in the total ordering
assumption in the model proposed by Bill:
The model is that you have a global system that, in each
step, executes one operation from one thread. Thus, there
is a total order over the execution of all operations.
^^^^^^^^^^^^^
The LC model instead allows reordering of instructions within a thread,
so long as no control or data dependence is violated.
3. The flexibility in the LC model demonstrated by the above example
is important for compiler optimizations. Note that compiler writers
already use a dependence model (e.g., a program dependence graph, or
some approximation thereof) to determine what code reordering is
legal in a single-threaded program. What the LC model says is
that the same kind of model can be used for code reordering,
even if the thread might execute in a multithreaded context.
Vivek Sarkar (IBM)
Guang R. Gao (University of Delaware)
------------------------------------------------------------------------------
From: Bill Pugh
To: javaMemoryModel@cs.umd.edu
cc:
Subject: JavaMemoryModel: A new memory model for Java
OK, here is an attempt at a new memory model for Java.
This memo doesn't include anything about safety
of object construction or of final fields (the kinds
of things we need for String) -- those will be added later.
This is an operational semantics. It isn't intended
as a way anybody would actually implement Java, although
you could implement it this way.
The model is that you have a global system that, in each
step, executes one operation from one thread. Thus, there
is a total order over the execution of all operations. However,
process that decide what value is seen by a read is complicated
and nondeterministic, so the end result isn't just sequential
consistency.
An operation corresponds to one JVM opcode. A getfield, getstatic
or array load opcode corresponds to a Read. A putfield, putstatic
or array store opcode corresponds to a Write. A variable corresponds
to a field of an object, a static field, or an element of an array.
The fact that garbage collection moves objects in physical memory
is irrelevant and transparent to the memory model.
For each variable v, there is a set allWrites(v), containing
all writes performed by any thread to that variable.
For each variable v and thread t, overwritten_t(v) is the set
of writes to variable v that thread t knows are overwritten
and previous_t(v) is the set of all writes to variable v that
thread t knows occurred previously. It is an invariant that
for all t and v,
overwritten_t(v) subset previous_t(v) subset allWrites(v)
Furthermore, all of these sets are monotonic: they can only
grow.
When each variable v is created, there is a write w of the default
value to v s.t. allWrites(v) = {w} and for all t,
overwritten_t(v) = {} and previous_t(v) = {w}.
When thread t performs a write w to variable v, the following
updates occur:
overwritten_t(v) = previous_t(v)
previous_t(v) += {w}
allWrites(v) += {w}
When thread t reads a variable v, the value returned is that
of an arbitrary write from the set
allWrites(v) - overwritten_t(v)
For a volatile variable v things are simpler: there is a
global mapping volatileValue(v) which is initialized to
the default value, and read/written by Read/Write operations
on v.
Each lock operation on a monitor m is immediately followed by
an acquire operation on m, and each unlock operation is immediately
preceded by a release operation on m. Similarly, each read of
a volatile variable v is immediately followed by an acquire operation
on v, and each write operation on v is immediately preceded
by a release operation on m.
Each monitor m knows, for each variable, a set of overwritten
and previous writes. When a thread t acquires monitor m,
thread t updates its overwritten and previous information
with that of the monitor. To merge overwritten and previous
information, just use union the appropriate sets:
For each variable v,
overwritten_t(v) = overwritten_t(v) union overwritten_m(v)
previous_t(v) = previous_t(v) union previous_m(v)
When a thread t performs a release on a monitor, the overwritten and
previous information from the thread is merged into the overwritten
and previous information for the monitor:
For each variable v,
overwritten_m(v) = overwritten_m(v) union overwritten_t(v)
previous_m(v) = previous_m(v) union previous_t(v)
Since you can only release a monitor if you previously acquired it (but
see volatile variables), and these sets are monotonic, this is equivalent
to
For each variable v,
overwritten_m(v) = overwritten_t(v)
previous_m(v) = previous_t(v)
Acquire and releases on volatile variables work the same way as for
monitors, except that there is no requirement to read/acquire a volatile
variable before you write/release it, and therefore you need to merge,
rather
than replace, information for a release.
If your program is properly synchronized, then whenever thread t reads
writes
a variable v, you must have done synchronization in a way to ensure that
all previous writes of that variable are known to be previous. In other
words,
allWrites(v) = previous_t(v)
>From that, you can do an induction proof that initially and before and
after
thread t reads or writes a variable v,
|allWrites(v) - overwritten_t(v)| = 1
Thus, the value of v read by thread t is always the most recent write
of v: allWrites(v) - overwritten_t(v), and you have sequential consistency.
This scheme is very similar to the way lazy release consistency is
implemented, and is identical to Sarkar's and Gao's Location Consistency,
except for the fact that in location consistency, an acquire or release
effects only a single memory location. That feature could be incorporated
into this scheme (by making the merge functions for acquire/release effect
only a single variable).
So show the equivalence with Location Consistency, the previous_t(v)
is just the set { e | t in processorset(e) } and everything reachable
from that set by following edges backwards in the poset for v, and
the MRPW set is equal to previous_t(v) - overwritten_t(v).
Although my model is essentially identical to Location Consistency,
I think the description I have provided will be easier for more
people to understand.
Bill
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:21 EDT