Should we judge whether programs are functionally equivalent based on identical modification orders?

Consider this example:

#include <atomic> #include <iostream> #include <thread> std::atomic<int> canceller = {0}; int main() { auto t1 = std::thread([]() { auto v = canceller.fetch_add(1, std::memory_order::relaxed); // #0 std::thread([v]() { int current = v + 1; if (canceller.load(std::memory_order::relaxed)==current) { // #1 std::cout<<"invoked, not canceled"; // #2 } }).join(); }); auto t2 = std::thread([]() { int current = 1; while(!canceller.compare_exchange_strong(current, 2, std::memory_order::relaxed,std::memory_order::relaxed)){ // #3 current = 1; } }); t1.join(); t2.join(); }

In this example, we can observe that #3 returns true and exits the loop, and in which case #2 is either printed out or isn't executed. The corresponding modification order is

0 < #0 < #3

According to [intro.races] p14

If a side effect X on an atomic object M happens before a value computation B of M, then the evaluation B takes its value from X or from a side effect Y that follows X in the modification order of M.

#0 happens before #1, so #1 can either read #0 or #3, which are all possible, and reflects that #1 either returns true or false, under this modification order.

If we change #1 to a CAS operation, should we compare whether the changed one is functionally equivalent to the original based on the same modification order?

#include <atomic> #include <iostream> #include <thread> std::atomic<int> canceller = {0}; int main() { auto t1 = std::thread([]() { auto v = canceller.fetch_add(1, std::memory_order::relaxed); // #0 std::thread([v]() { int current = v + 1; if (canceller..compare_exchange_strong( current, current, std::memory_order::relaxed, std::memory_order::relaxed)) { // #1 std::cout<<"invoked, not canceled"; // #2 } }).join(); }); auto t2 = std::thread([]() { int current = 1; while(!canceller.compare_exchange_strong(current, 2, std::memory_order::relaxed,std::memory_order::relaxed)){ // #3 current = 1; } }); t1.join(); t2.join(); }

That is, under the same modification order

0 < #0 < #3

The CAS at #1 must fail; otherwise, it would violate [atomics.order] p10

Atomic read-modify-write operations shall always read the last value (in the modification order) written before the write associated with the read-modify-write operation.

So, given the same modification order, we conclude that changing #1 to CAS breaks the functional equivalence, and a CAS at #1 can provide more stable detection of change than a pure load.

Is this reasoning correct? Is it a valid and reasonable approach to determine functional equivalence between the CAS operation(writing the same value) and the pure load (in #1) by assuming the same modification order?

If not that, why is it not a valid way? What is a reasonable approach?