The memory order of the store to `weak` in `is_unique` is over-strict

Consider this example:

let arc = Arc::new(0);
let arc2 = arc.clone();
// thread 1:
Arc::is_unique(&arc); // or arc.get_mut();
// thread 2:
let weak = Arc::downgrade(&arc2);
drop(arc2);

For convenient analysis, I cite the snippet of the inner implementations of relevant methods here

    pub fn downgrade(this: &Self) -> Weak<T, A>
    where
        A: Clone,
    {
        // This Relaxed is OK because we're checking the value in the CAS
        // below.
        let mut cur = this.inner().weak.load(Relaxed);

        loop {
            // check if the weak counter is currently "locked"; if so, spin.
            if cur == usize::MAX {
                hint::spin_loop();
                cur = this.inner().weak.load(Relaxed);
                continue;
            }

            // We can't allow the refcount to increase much past `MAX_REFCOUNT`.
            assert!(cur <= MAX_REFCOUNT, "{}", INTERNAL_OVERFLOW_ERROR);

            // NOTE: this code currently ignores the possibility of overflow
            // into usize::MAX; in general both Rc and Arc need to be adjusted
            // to deal with overflow.

            // Unlike with Clone(), we need this to be an Acquire read to
            // synchronize with the write coming from `is_unique`, so that the
            // events prior to that write happen before this read.
            match this.inner().weak.compare_exchange_weak(cur, cur + 1, Acquire, Relaxed) {
                Ok(_) => {
                    // Make sure we do not create a dangling Weak
                    debug_assert!(!is_dangling(this.ptr.as_ptr()));
                    return Weak { ptr: this.ptr, alloc: this.alloc.clone() };
                }
                Err(old) => cur = old,
            }
        }
    }

       pub fn is_unique(this: &Self) -> bool {
        // lock the weak pointer count if we appear to be the sole weak pointer
        // holder.
        //
        // The acquire label here ensures a happens-before relationship with any
        // writes to `strong` (in particular in `Weak::upgrade`) prior to decrements
        // of the `weak` count (via `Weak::drop`, which uses release). If the upgraded
        // weak ref was never dropped, the CAS here will fail so we do not care to synchronize.
        if this.inner().weak.compare_exchange(1, usize::MAX, Acquire, Relaxed).is_ok() {
            // This needs to be an `Acquire` to synchronize with the decrement of the `strong`
            // counter in `drop` -- the only access that happens when any but the last reference
            // is being dropped.
            let unique = this.inner().strong.load(Acquire) == 1;

            // The release write here synchronizes with a read in `downgrade`,
            // effectively preventing the above read of `strong` from happening
            // after the write.
            this.inner().weak.store(1, Release); // release the lock
            unique
        } else {
            false
        }
    }
   

Directly considering the critical case that cas in is_unique is successful. That means the loop in downgrade can exit only if it reads the value written by this.inner().weak.store(1, Release); in is_unique. Assuming the memory order is Relaxed, and we are concerned that this.inner().strong.load(Acquire) in the is_unique reads the value written by the Drop of Arc in thread 2 and returns 1, however, if this.inner().strong.load(Acquire) reads the value written by the release store in Drop, they would form the synchronization, that means, the load parts of weak in downgrade happen before this.inner().weak.store(1, Relaxed) in is_unique.

In this case, according to read-write coherence rule, the load part of weak in downgrade cannot see the value written by this.inner().weak.store(1, Relaxed) in is_unique. The loop won't exit, so the control flow cannot reach drop(arc2). This contradicts the assumption that drop(arc2) is reached. That is, this.inner().strong.load(Acquire) cannot read the value written by Drop of Arc even though this.inner().weak.store(1, Relaxed) has relaxed memory order.

This is the reasoning from the abstract machine sense, and hence, a conforming implementation cannot violate the observable behavior.

More generally speaking, any thread claiming that its RMW operation in drop of Arc would be loaded by this.inner().strong.load(Acquire) is impossible. Because that would result in its load part of CAS/RMW operation on weak(called "current RMW operation on weak", namely, RMW_weak_current) happens before the store to weak that writes 1, which in turn requires that other RMW operations on weak the current RMW operation on weak load should precede RMW_weak_current in the modification order of weak, and the first such RMW operation must read the value 1(this can only be produced by weak_store), which result in an invalid modification order:

1 < MAX < weak_store < RMW_weak_1 < .... < RMW_weak_current< ... < weak_store 

So, this is still true if there are multiple threads doing something like thread 2. The load to strong in is_unique cannot return 1 because that would result in all drops to other Arcs happening before the load.

IIUC, this.inner().weak.store(1, Release); can be changed to this.inner().weak.store(1, Relaxed);, at least.

Start with the Arc::is_unique, Arc::downgrade, and Weak::drop implementations shown in the issue, tracing the weak and strong counter operations and their memory-ordering guarantees. Validate whether the release store in is_unique can be relaxed under the stated execution, then document the conclusion with the relevant concurrency tests or add coverage if the repository has suitable tests.