Why casualty test case 16 is wrong? about cs431 HOT 7 CLOSED

FWIW, it is safe to assume a thread exit/join pair is synchronizing like a pair of release/acquire. Yes, you cannot reorder a thread join with later instructions.

from cs431.

Similar question concerning case kaist-cp/helpdesk#19:

Causality test case 19

Initially, x = y = 0

Thread 1:
join thread 3
r1 = x
y = r1

Thread 2:
r2 = y
x = r2

Thread 3:
r3 = x
if (r3 != 42)
x = 42

Behavior in question: r1 == r2 == r3 == 42

Decision: Allowed. This is the same as test case 17, except that thread 1 has been
split into two threads.

Why casualty test case 19 is wrong? I have an assumption that if "joining thread" is allowed to be reordered with later instructions, then case kaist-cp/helpdesk#19 becomes the same as case kaist-cp/helpdesk#17, where behaviour is Allowed. However, if "joining thread" is never reordered with later instructions, then behaviour is Disallowed. So, is my assumption("joining thread" is never reordered) right reason why behaviour is Disallowed?

Thank you!

For reference:
Causality test case 17

Initially, x = y = 0

Thread 1:
r3 = x
if (r3 != 42)
x = 42
r1 = x
y = r1

Thread 2:
r2 = y
x = r2

Behavior in question: r1 == r2 == r3 == 42

Decision: Allowed. A compiler could determine that at r1 = x in thread 1,
is must be legal for to read x and see the value 42. Changing r1 = x
to r1 = 42 would allow y = r1 to be transformed to y = 42 and performed
earlier, resulting in the behavior in question.

from cs431.

Again, you're reordering instructions beyond what's allowed. For example, in test case 16, r1=x and x=1 cannot be reordered because they're accessing the same location.

from cs431.

What about joining the thread? Is it also not allowed to reorder the moment of joining the thread?

from cs431.

Concerning case 16. I tried using the promising semantics, but got "Allowed" result. Where did I go wrong in my reasoning?

1. Initial views:
   
2. Thread 1 makes the promise X = 1, Thread 2 makes the promise X = 2. Both are certified, as those promises can be fulfilled when their threads are executed in isolation.
   
3. After thread 1 is executed, r1 = 2 and promise X = 1 is re-certified and fulfilled.
   
4. After thread 2 is executed, r2 = 1 and promise X = 2 is re-certified and fulfilled.
   

For reference:
Causality test case 16

Initially, x = 0

Thread 1:
r1 = x
x = 1

Thread 2:
r2 = x
x = 2

Behavior in question: r1 == 2; r2 == 1

Decision: Allowed.

from cs431.

3. is wrong. t1's view is pointing to X=2 after reading it, so it cannot fulfill an earlier message X=1.

from cs431.

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

from cs431.