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
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:20 EDT