I think Sarita is on the right track here. I was reading her model
this evening and I find it much easier to understand, both intuitively
and formally, than the "consistency+causality" model. It is even
easier to understand that her model from July 3 (which I read over the
weekend) because it doesn't have the backward slices and some other
stuff that worried me. I was going to suggest that she could go a bit
further and simply allow the program to execute as though with
sequential consistency, except that reads in data races can be
replaced by any value that they are allowed to read (by Jeremy and
Bill's definition) in that execution, which, of course, influences
subsequent instructions that may be executed. (I'm still not entirely
comfortable with the writes, as I'll discuss below.) I hadn't worked
out the details yet, but, I think this is basically what she is
suggesting in the last pair of emails.
I still haven't fully grokked Sarita's model, but the part that most
"tingles my spider-sense" is how competing writes are handled. In
particular,
1. I assume that the model is intended to generalize to more than two
competing writes: in that case, a subsequent read can return any of
the values written by those writes. Is this true? If so, how does
this work for three writes, two of which compete with the third, but
not with each other? For example,
Initially, X == 0
Thread 1 Thread 2
X = 1 X = 2
X = 3 r2 = X
r1 = X
What values may each of r1 and r2 get? Or more to the point, what
"special write" replaces "X = 2" so that we cannot get r1 == 1?
2. Should a value be allowed to "oscillate"? That is, suppose two
competing writes write 1 and 2 into x. Can another thread see 1
and then 2 and then 1 again (assuming 1 and 2 are never written
by any other instruction instance)? Is this allowed even if there
are synchronization operations intervening between the reads?
Consider for example
Initially, X == 0, V == 0 (V is volatile)
Thread 1 Thread 2 Thread 3
X = 1 X = 2 r3 = V; V = r3+1
r1 = V r2 = V ra = X
V = r1+1 V = r2+1 r4 = V; V = r4+1
rb = X
r5 = V; V = r5+1
rc = X
Can we get r1 == 0, r2 == 1, r3 == 2, r4 == 3, r5 == 4 and
ra == 1, rb == 2, rc == 1?
(I could put in while loops before reading V to make sure it
got the right values.)
Victor
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:47 EDT