Consider this example:
x = 0; // initially 0
y = 0; // initially 0
-Thread 1-
y.store (20, memory_order_release);
x.store (10, memory_order_release);
-Thread 2-
if (x.load(memory_order_acquire) == 10) {
assert (y.load(memory_order_acquire) == 20);
y.store (10, memory_order_release)
}
-Thread 3-
if (y.load(memory_order_acquire) == 10) {
assert (x.load(memory_order_acquire) == 10);
}
In this example, if the if statement in thread3 does not execute, the assertion in thread3 won't be executed. So, we just need to consider the case when the if statement is executed. This means the store operation on y in thread2 that sets the value 10 should be seen by the load operation of y in thread3, which requires the if statement in thread2 execute, similar, which requires the load operation of x in thread2 see the value stored by the store operation of x in thread1. Hence, if the assertion in the thread3 is executed, we will have these conditions
x-store-in-thread1 synchronizes x-load-in-thread2
y-store-in-thread2 synchronizes y-load-in-thread3
Hence, the complete conditions we will have are:
p1: y-store-in-thread1 is sequenced before x-store-in-thread1
p2: x-store-in-thread1 synchronizes x-load-in-thread2
p3: x-load-in-thread2 is sequenced before y-load-in-assert-in-thread2
p4: y-load-in-assert-in-thread2 is sequenced before y-store-in-thread2
p5: y-store-in-thread2 synchronizes y-load-in-thread3
p6: y-load-in-thread3 is sequenced before x-load-in-thread3
With these conditions, we can further infer these conclusions:
p2 => p2': x-store-in-thread1 inter-thread happens before x-load-in-thread2
p1 + p2' => p7: y-store-in-thread1 inter-thread happens before x-load-in-thread2
p2 + p3 => p8: x-store-in-thread1 inter-thread happens before y-load-in-assert-in-thread2
p1 + p8 => p9: y-store-in-thread1 inter-thread happens before y-load-in-assert-in-thread2
p5 => p5': y-store-in-thread2 inter-thread happens before y-load-in-thread3
p4 + p5' => p10: y-load-in-assert-in-thread2 inter-thread happens before y-load-in-thread3
p5 + p6 => p11: y-store-in-thread2 inter-thread happens before x-load-in-thread3
p4 + p11 => p12: y-load-in-assert-in-thread2 inter-thread happens before x-load-in-thread3
p3 + p12 => p13: x-load-in-thread2 inter-thread happens before x-load-in-thread3
p2' + p13 => p14: x-store-in-thread1 inter-thread happens before x-load-in-thread3
p14 => x-store-in-thread1 happens before x-load-in-thread3
Since [intro.races] p18 says:
If a side effect X on an atomic object M happens before a value computation B of M, then the evaluation B shall take its value from X or from a side effect Y that follows X in the modification order of M.
In this case, we do not have a store operation of x after x-store-in-thread1, in the modification order of x. Hence, x-load-in-thread3 should read the value stored by x-store-in-thread1, hence, the conclusion of my analysis is the assertion in thread3 is guaranteed to be true when it is executed, in any other cases, the assertion won't be executed.
However, the Overall Summary in GCC Atomic Wiki says:
Release/acquire mode only requires the two threads involved to be synchronized. This means that synchronized values are not commutative to other threads. The assert in thread 2 must still be true since thread 1 and 2 synchronize with x.load(). Thread 3 is not involved in this synchronization, so when thread 2 and 3 synchronize with y.load(), thread 3's assert can fail. There has been no synchronization between threads 1 and 3, so no value can be assumed for 'x' there.
But, I do infer that the store operation of x in thread 1 happens before the load operation of x in thread 3.
