I was thinking back on some of the questions Sarita asked. As an
example, why can't we just say "type-safety" and "not-out-of-thin-air
safety" for incorrectly synchronized programs, and leave it at that?
Put aside issues like final fields, longs and doubles, virtual method
invocation and array length for the moment. Consider just reads and
writes of fields. What guarantees do we need other than:
* type safety
* not-out-of-thin-air safety
Consider the following program:
Thread 0:
lock Foo.a
Point tmp = new Point();
tmp.x = 1;
Foo.p = tmp
unlock Foo.a
Thread 1:
lock Foo.a
Point tmp = Foo.p
print "T1: " + tmp.x;
tmp.x = 2;
unlock Foo.a
Thread 2:
Point tmp = Foo.p
tmp.x = 3;
Thread 3:
lock Foo.a
Point tmp = Foo.p;
print "T3: " + tmp.x;
unlock Foo.a
Say further than we know thread 1 acquires Foo.a after it is released
by thread 0, and that thread 3 acquires Foo.a after it is released by
thread 1.
In this case, I think we need the following restrictions:
* When thread 1 prints tmp.x, it must not print 0, the initial value of tmp.x
(i.e., it can print 1 or 3).
* When thread 3 prints tmp.x, it must not print either 0 or 1
(i.e., it can print 2 or 3).
Basically, the requirement is:
* Among a set of threads that are properly synchronized, certain writes
will not be visible to certain reads (of the same variable)
because they have
been overwritten.
Adding additional (perhaps incorrectly synchronized) reads or writes to the
program must not make visible any of the writes previously considered to be
overwritten.
This is enforced by my proposal, and I'm pretty sure it is enforced
by the CRF proposal. I can't imagine any transformation that would
destroy this, but it points out some of the subtle issues we need to
enforce if we try to build a JMM from the bottom-up (e.g., what do we
need more than sequential sequential consistency for correctly
synchronized programs).
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:28 EDT