Initially, there was some question as to whether the behavior in test
case 7 was allowed in SC-1.
Sarita has shown that test case 7 is allowed by SC-1.
However, I have come up with a new causality test case 11, an
extension of test case 7, which I believe is not allowed by either
SC-1 or SC-2. Is is allowed by the Manson/Pugh model. I've not had a
chance to run this by Sarita, but since she's out of email contact
this weekend, I wanted to get it out to the list.
>Causality test case 11:
>
>Initially, x = y = z = 0
>
>Thread 1:
>r1 = z
>w = r1
>r2 = x
>y = r2
>
>Thread 2:
>r4 = w
>r3 = y
>z = r3
>x = 1
>
>Behavior in question: r1 = r2 = r3 = r4 = 1
>
>Decision: Allowed. Reordering of independent statements can transform
> the code to:
>
> Thread 1:
> r2 = x
> y = r2
> r1 = z
> w = r1
>
> Thread 2:
> x = 1
> r3 = y
> z = r3
> r4 = w
>
> after which the behavior in question is SC.
Under SC-1, the first action in the execution order would have to be
r1 = z (1) or r4 = 1 (w).
This behavior is not allowed in SC-1, because in all SC executions,
there is no write of 1 to z or w. So the action r1 = z (1) and r4 = w
(1) can't be performed as the first action in the execution order.
The difference between this example and test case 7 is that in test
case 7, there is a SC execution in which a write of 1 to y is
performed, so r3 = y (1) may be performed presciently.
The behavior is allowed by both the strong Manson/Pugh model (in our
one page summary posted Thursday), and weaker variation suggested by
Sarita.
Test case 11 has been added to the causality test cases web page:
http://www.cs.umd.edu/~pugh/java/memoryModel/CausalityTestCases.html
Other should double check my reasoning that test 11 is not allowed by
SC-1. As we all know too well, all of these memory models can be
tricky to apply.
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:50 EDT