Is it impossible that the acquire load returns `1` when the loops in other threads exit?

Consider this example:

#include <atomic> #include <cassert> #include <thread> int main() { std::atomic<int> strong = {3}; std::atomic<int> weak = {1}; auto t1 = std::thread([&]() { int expected = 1; if (weak.compare_exchange_strong(expected, 255, std::memory_order::acquire, std::memory_order::relaxed) == true) { bool unique = strong.load(std::memory_order::acquire) == 1; // #0 weak.store(1, std::memory_order::relaxed); // #1 assert(unique == false); } }); auto t2 = std::thread([&]() { auto val = weak.load(std::memory_order::relaxed); while (true) { if (val == 255) { std::this_thread::yield(); val = weak.load(std::memory_order::relaxed); continue; } if (weak.compare_exchange_strong( val, val + 1, std::memory_order::acquire, std::memory_order::relaxed) == true) { break; } } strong.fetch_sub(1, std::memory_order::release); // #2 }); auto t3 = std::thread([&]() { auto val = weak.load(std::memory_order::relaxed); while (true) { if (val == 255) { std::this_thread::yield(); val = weak.load(std::memory_order::relaxed); continue; } if (weak.compare_exchange_strong( val, val + 1, std::memory_order::acquire, std::memory_order::relaxed) == true) { break; } } strong.fetch_sub(1, std::memory_order::release); // #3 }); t1.join(); t2.join(); t3.join(); }

Assuming the CAS operation in t1 succeeds, that means the loops in t2 and t3 cannot exit except that one thereof reads #1 and the other reads the value written by the RMW operation that reads #1. The question is whether #0 can read 1 and the assertion fails. Assume that #0 reads 1, because the initial value of strong is 3, this implies that #2 and #3 both happen before #0, which in turn implies that the load part of weak in t2 and t3 both happen before #1. According to [intro.races] p13

If a value computation A of an atomic object M happens before an operation B that modifies M, then A takes its value from a side effect X on M, where X precedes B in the modification order of M.

#1 is not visible to the load part of weak in t2 and t3, so the loop in t2 and t3 cannot exit; this means, #2 and #3 cannot be reached by the corresponding control flows in their respective threads. This contradicts the assumption that #0 reads 1 because #2 and #3 won't be executed in the lifetime of the program; otherwise, it would violate [intro.races] p10

The value of an atomic object M, as determined by evaluation B, is the value stored by some unspecified side effect A that modifies M, where B does not happen before A.

More generally speaking, any thread claiming that its RMW operation on strong would be read by #0 is impossible, because its CAS operation on weak does not expect 255, and #1 is not visible to the load part, so its loop cannot exit. And no other RMW operation on weak that increases count can precede it; otherwise, the modification order of weak is invalid

1 < 255 < weak_store_1 < RMW_weak_a < ... < RMW_weak_current < ... < weak_store_1

So, #0 cannot read 1 and 2; however, it can only read the initial value 3. Is my analysis right? Actually, this is a simplified question from my research on Rust's implementation of Arc, specifically regarding the is_unique method (line 2585) and the downgrade method (line 1735). If the target is, as described in the comment, to check whether the thread holds the unique strong, I think the memory order used for the case is over-strict, and the memory order of the store to weak that writes 1 can at least be relaxed, IIUC.