OK. now for some analysis of the model I proposed. It is intended to be a
very weak model, while still guaranteeing sequential consistency for
correctly synchronized programs and some safety guarantees. The only real
guarantees for incorrectly synchronized programs are:
* A read will produce some value written to that location (giving us type
safety
and not-out-of-thin-air safety).
* If you know that a value has been overwritten, then any code you invoke
cannot discover the overwritten value.
I'll work through the reads kill example: Initially p.x = 0 and p.x and q.x
are aliases for the same variable.
Thread 1 Thread 2
p.x = 42 int i = p.x
int a = p.x int j = q.x
int b = q.x int k = p.x
We'll use v to represent the variable referenced by both p.x and q.x and
two threads T1 and T2.
Initially, we have
write w_0: v=0
allWrites(v) = previous_T1(v) = previous_T2(v) = {w_0}
overwritten_T1(v) = overwritten_T2(v) = {}
Say thread T1 executes its write first. This becomes write w_1: v=42
Now we have:
allWrites(v) = previous_T1(v) = {w_0, w_1}
previous_T2(v) = {w_0}
overwritten_T1(v) = {w_0}
overwritten_T2(v) = {}
Now, any reads done on thread T1 get a value from {w_0, w_1} - {w_0},
which must be w_1, so a and b both get the value 42.
Reads done on thread T2 get a value from {w_0, w_1} - {}. So each read can get
either 0 or 42, and it is perfectly fine for thread 2 to have i = 42, j =
0, k = 0.
OK, so how does my proposed model differ from the one in the JLS:
* The JLS requires coherence, my MM does not
* The JLS has the hair ball (the complicated example in my paper), and I hope
my proposal contains no such situations.
* In my model, a compiler can move reads and writes forward over an acquire,
and backward over a release. I believe that in the JLS, the ability to move
reads and writes forward over a lock operation is very limited.
Consider the following code fragment executed by thread T1 (where
x is a variable on the heap).
x = 17;
lock a
y = x;
Under my scheme, the write x=17 is not in the previous or overwritten set
of any other thread, so the acquire associated with the lock cannot
possibly
cause the write x=17 to be put into the overwritten set for T1. So at
the statement
y=x, we know that x=17 is in the set allWrites, but not in the set
overwritten_T1.
So 17 is a legal value to be read, and a compiler can do constant
propagation
and set y = 17.
Intuitively, the write x = 17 will definitely be one of the available
choices when x is read after the lock is obtained, so doing an optimization
that constrains that choice to be write x=17 is a legal optimization.
In addition to the reordering described above, the compiler is also
allowed to delete acquire/release operations that will have no effect. This
include:
* acquire/release operations on thread-local objects
* acquire/release operations resulting from recursive locks
(e.g., if a thread T1 already holds a lock on X, then if
T1 attempts to lock X a second time, the acquire associated
with the lock can be skipped).
Bill
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