The choice on test cases 5 and 10 seems to be one of the key issues
for the core memory model.
http://www.cs.umd.edu/~pugh/java/memoryModel/CausalityTestCases.html
Test case 5:
Initially, x = y = z = 0
Thread 1:
r1 = x
y = r1
Thread 2
r2 = y
x = r2
Thread 3
z = 1
Thread 4
r3 = z
x = r3
Behavior in question: r1 == r2 == 1, r3 == 0.
Let me lay out some pro and con.
=== Why we should allow the behavior in test case 5 ===
A compiler or architecture might want to perform the following transformation:
* I predict that I will read 1 from x, so that r1 will be 1.
* I want to speculatively assume that I do read 1 from x,
and speculative perform actions that depend upon that read.
* If, when I read x, I find that I did not read 1, I promise
to unwind and restart all of the speculative actions that
depended upon r1=1. Note that these speculative actions are
scattered across multiple threads.
OK, while this transformation sounds appealing, we can't apply it in
all cases. In particular, it allows test case 4.
To fix this, we need to modify the transformation as follows.
* In order to speculatively assume that I do read 1 from x,
I must show that there exists some non-prescient
execution in which I do read 1 from x.
With this modification, the behavior in test case 4 is prohibited,
while the behavior in test cases 5 and 10 are allowed.
=== Why we should forbid the behavior in test case 5 ===
I think there are lots of reasons, but here is one I feel
particularly compelling:
* In order to understand how a particular execution happened, it should
suffice to examine the code that did happen. You shouldn't have
to examine whether some code that you know didn't execute might
form a race with the code that did execute.
* In particular, look at the code in test case 10. Is the following
behavior reasonable:
Initially, x = y = z = 0
Thread 1:
r1 = x (1)
if (r1 == 1)
y = 1
Thread 2
r2 = y (1)
if (r2 == 1)
x = 1
Thread 3
z = 1
Thread 4
r3 = z (0)
if (r3 == 1)
###### // we know it didn't execute, so we aren't going to look at it
Behavior in question: r1 == r2 == 1, r3 == 0
In the code that (is visible) / (did execute), the accesses to x and y are
correctly synchronized. So it becomes difficult to understand how the system
introduced data races on x and y and got behavior similar to that of
test case 4 which we thought we had ruled out.
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:49 EDT