Does this CAS operation, which is a pure load with a seq_cst memory order, guarantee the assertion never fires?

Consider this example:

#include <thread> #include <atomic> #include <cassert> int main(){ std::atomic<int> x = 0, y = 0; int result = 0; bool flag = false; auto t1 = std::thread([&](){ x.store(1,std::memory_order::seq_cst); // #1 result = y.load(std::memory_order::seq_cst); // #2 }); auto t2 = std::thread([&](){ y.store(1,std::memory_order::seq_cst); // #3 int expected = 1, new_v = 2; flag = x.compare_exchange_strong(expected,new_v,std::memory_order::seq_cst,std::memory_order::relaxed); // #4 }); t1.join(); t2.join(); if(result == 0){ assert(flag==true); } }

In this example, if result equals 0, this implies that #1, #2, and #3 in the single total order for memory_order::seq_cst operations should be #1 < #2 < #3. However, the memory_order::seq_cst memory order only applies to the success comparison of the CAS operation. This means the CAS operation doesn't participate in the single total order if it fails. #4 can be a pure load to read 0, whose value doesn't match expected; the comparison naturally fails. There is no contradiction in this assumption because neither contradict with single total order nor the comparison.

If expected is set to 0, the comparison can never succeed. If assuming #4 is RMW operation(i.e., the comparison succeeded), this implies the load part of the RMW operation must read 0, which results in a contradictory single total order.

If we only change #4 to flag = x.compare_exchange_strong(expected,new_v,std::memory_order::relaxed,std::memory_order::seq_cst);, the assertion will never fire. The reason is that, assuming the CAS operation fails, this means the operation must read a value that isn't equivalent to 1 because compare_exchange_strong is not a weak version that can fail spuriously. This implies that the CAS that is a pure load read 0 in this program, and the specified memory order seq_cst applies to the pure load, which results in a contradictory single total order; hence, the assumption is false. The specified memory order to the failed branch constraints that the CAS operation cann't fail. Since CAS is a binary operation(i.e., it either succeeds in being an RMW operation or fails in being a pure load), this operation can only succeed. The assertion can never fire.

Is my understanding of these three examples right?