Causality test case 12: behavior allowed?

[Shynar88]

Causality test case 12

Initially, x = y = 0; a[0] = 1, a[1] = 2

Thread 1
r1 = x
a[r1] = 0
r2 = a[0]
y = r2

Thread 2
r3 = y
x = r3

Behavior in question: r1 = r2 = r3 = 1

Decision: Disallowed. Since no other thread accesses the array a,
the code for thread 1 should be equivalent to

r1 = x
a[r1] = 0
if (r1 == 0)
      r2 = 0
    else
      r2 = 1
y = r2


With this code, it is clear that this is the same situation as
test 4.

---

In the answer, it's written that behavior is disallowed. However, it seems that there is the case when r1 = r2 = r3 = 1 can happen(described bellow). Am I missing something?

---

`Thread 1
r2 = a[0]
y = r2
r1 = x
a[r1] = 0

Thread 2
r3 = y
x = r3

Scheduling goes as following:
Thread 1
r2 = a[0]
y = r2
Thread 2
r3 = y
x = r3
Thread 1
r1 = x
a[r1] = 0

In this way r1 = r2 = r3 = 1
`

Thank you!

[Shynar88]

Similar question concerning casuality test kaist-cp/helpdesk#14

Causality test case 14

Initially, a = b = y = 0, y is volatile

Thread 1:
r1 = a
if (r1 == 0)
y = 1
else
b = 1

Thread 2:
do {
r2 = y
r3 = b
} while (r2 + r3 == 0);
a = 1;

Behavior in question: r1 == r3 = 1; r2 = 0

Decision: Disallowed In all sequentially consistent executions, r1 = 0 and
the program is correctly synchronized. Since the program is correctly
synchronized in all SC executions, no non-sc behaviors are allowed.

---

Why can't we reorder Thread 2 in the following way?

Thread 1:
r1 = a
if (r1 == 0)
y = 1
else
b = 1

Thread 2:
a = 1;
do {
r2 = y
r3 = b
} while (r2 + r3 == 0);

Scheduling goes as following:
Thread 2
a = 1;
Thread 1
(all lines executed)
Thread 2
(rest of the lines executed)

In this way r1 == r3 = 1; r2 = 0

[jeehoonkang]

You're reordering instructions beyond what is allowed. For example, in test case 12, you cannot reorder a[r1] = 0 with r2 = a[0]. The promising semantics define which reorderings are allowed and which are not, so I recommend you to execute those test cases in the promising semantics to see what can happen.

[jeehoonkang]

Closing, but feel free to reopen it if you have followup questions.