JavaMemoryModel: test case 11; allowed by Manson/Pugh but not by SC-1

From: Bill Pugh (
Date: Sat Aug 02 2003 - 11:48:41 EDT

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

Test case 11 has been added to the causality test cases web page:

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.

JavaMemoryModel mailing list -

This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:50 EDT