Causality test case 7:
Initially, x = y = z = 0
Thread 1:
r1 = z
r2 = x
y = r2
Thread 2:
r3 = y
z = r3
x = 1
Behavior in question: r1 = r2 = r3 = 1.
We must allow this behavior, because simple reordering of independent
statements could move the read of z last in thread 1, and the write
to x first in thread 2.
After those movements, SC execution could give us r1 = r2 = r3 = 1.
This execution is not allowed in SC-3.
Say it is allowed. We need to start with either r1 = z (1) or r3 = y
(1) in SC order.
Say we start with r1 = z (1). In order to show that this
discontinuity is legal in SC-3, we need to show that in all SC
extensions of this execution, 1 will be written to z. However, since
we cannot guarantee the ordering of the writes and reads to either x
or y, we cannot make this guarantee. For example, it does not occur in
r1 = z (1)
r3 = y (0)
r2 = x (0)
z = r3
x = 1
y = r2
Alternatively, we could start with r3 = y (1). We need to show that
in all SC extensions of this execution, 1 will be written to y.
Unfortunately, it doesn't occur in this SC extension:
r3 = y (1)
r1 = z (0)
r2 = x (0)
y = r2
z = r3
x = 1
So this behavior is not allowed by SC-3.
-------------------------------
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