The asker is dissecting the C11 adaptation of the Chase-Lev work-stealing deque from Lê et al.'s "Correct and Efficient Work-Stealing for Weak Memory Models." The paper claims the implementation is optimal: no C11 synchronization can be weakened without breaking correctness. The asker isn't buying it — specifically, they can't see why the initial load of top in push() needs memory_order_acquire rather than memory_order_relaxed.

Recall the shape of push():

void push(Deque *q, void *w) {
    size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed);
    size_t t = atomic_load_explicit(&q->top,    memory_order_acquire); // <-- why acquire?
    Array *a = atomic_load_explicit(&q->array,  memory_order_relaxed);
    if (b - t > a->size - 1) { /* grow */ }
    ...
}

Why it's subtle. Only the owner thread calls push() and take(); stealers race on top. Naively you'd think the owner never reads anything published by stealers — stealers only CAS top forward. So what could an acquire load possibly synchronize with?

The real answer lies in the resize path. The t value determines whether we grow the array. If the load of top is stale, we might grow unnecessarily — annoying, but not incorrect. However, the tricky case is around the interaction with a preceding take(): after a failed CAS in take(), the owner may have written bottom back, and the value of top observed by that CAS establishes a happens-before edge. If the subsequent push() reads a value of top that's older than what the same thread already observed via the CAS in take(), we can violate the invariant bottom ≥ top that the size calculation depends on — leading to a bogus size and either a spurious resize or, worse, an underflow in b - t (unsigned wraparound producing a huge apparent size).

Sketch of a proof direction. The paper's formal model (they mechanized it in Coq/Herd) tracks the "modification order" of top. Relaxed loads by the owner can observe any prior write in that modification order, including ones already superseded by writes the same thread has causally observed. The acquire ensures the owner sees a value at least as new as any it previously read-modify-wrote, closing that window.

Gotchas:

• b - t is unsigned — stale t can wrap catastrophically.
• Single-thread reasoning fools you: even the owner needs synchronization with its own earlier atomic RMWs to preserve modification-order consistency across relaxed reloads.
• x86 hides this bug; only ARM/POWER expose it under stress. Test with TSan + relaxed accesses on weakly-ordered hardware or with a C11 model checker (CDSChecker, GenMC).