Suspicious transitivity of relaxed CAS

[sbarral]

Hi,

First of all, thanks for this amazing tool.

While testing the acquire-release transitivity example from https://en.cppreference.com/w/cpp/atomic/memory_order, I noticed something peculiar: loom does not trigger the assert when the CAS uses relaxed ordering.

let flag_receiver = Arc::new(AtomicU32::new(0));
let flag_sender = flag_receiver.clone();
let flag_interceptor = flag_receiver.clone();

let data_receiver = Arc::new(UnsafeCell::new(0));
let data_sender = data_receiver.clone();

let th_sender = thread::spawn(move || {
    unsafe { data_sender.with_mut(|p| p.write(42)) };
    flag_sender.store(1, Release);
});

let th_interceptor = thread::spawn(move || {
    // The transitivity example at
    // https://en.cppreference.com/w/cpp/atomic/memory_order
    // uses these orderings:
    //
    // let _ = flag.compare_exchange(1, 2, AcqRel, AcqRel);
    //
    // But the below works too...
    let _ = flag_interceptor.compare_exchange(1, 2, Relaxed, Relaxed);
});

let th_receiver = thread::spawn(move || {
    if flag_receiver.load(Acquire) == 2 {
        assert!(unsafe { data_receiver.with(|p| p.read()) == 42 }); // never fires
    }
});

th_sender.join().unwrap();
th_interceptor.join().unwrap();
th_receiver.join().unwrap();

loom does generate branches where the assert is checked (i.e. where the receiver sees flag_receiver.load(Acquire) == 2), but it never fires. I guess that Relaxed is indeed OK as CAS failure ordering, but I would have expected anything weaker than AcqRel for the CAS success to trigger the assert.

[tomtomjhj]

If flag_receiver.load(Acquire) == 2 then data_receiver.with(|p| p.read()) == 42 must hold regardless of the ordering of flag_interceptor.compare_exchange.

http://open-std.org/jtc1/sc22/wg21/docs/papers/2020/n4868.pdf

• The store and compare_exchange form a release sequence headed by the store.
  • §6.9.2.2.5 A release sequence headed by a release operation A on an atomic object M is a maximal contiguous subsequence of side effects in the modification order of M, where the first operation is A, and every subsequent operation is an atomic read-modify-write operation.
• The store synchronizes with load, because the load takes the value from the release sequence headed by store.
  • §31.4.2 An atomic operation A that performs a release operation on an atomic object M synchronizes with an atomic operation B that performs an acquire operation on M and takes its value from any side effect in the release sequence headed by A.

[sbarral]

@tomtomjhj Thank you very much for looking into this and for the detailed explanation.

Looks like my expectation was wrong then, I can only take solace in the fact that even the C++ reference authors apparently made the same flawed assumption ;-)

I guess we can close this report then?

[tomtomjhj]

Yeah I think this issue can be closed.