Causality test case 12: behavior allowed? about cs431 HOT 3 CLOSED

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

from cs431.

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.

from cs431.

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

from cs431.