Is the acquire load on top necessary in this C11 Chase-Lev Deque implementation?

The acquire on q->top in push() is there to order slot reuse, not to observe payload writes from thieves.

The important interleaving is the full-ring case. A stealer reads the old element and only then publishes that the slot is free by incrementing top:

/ steal() /
x = loadexplicit(&a->buffer[t % a->size], relaxed);
compareexchangestrongexplicit(&q->top, &t, t + 1, seqcst, relaxed);
/* push(), after seeing that incremented top */
storeexplicit(&a->buffer[b % a->size], x, relaxed);

When the deque was full, b % a->size is the same circular-buffer slot as the old t % a->size. So if push() sees the thief's incremented top, it is about to reuse exactly the slot that the thief has just claimed.

The successful seqcst CAS is a release/acquire read-modify-write operation, and an acquire load prevents following reads or writes from being reordered before the load (C atomic memory orders). Therefore, when push()'s acquire load reads the value written by the stealer's CAS, the thief's earlier buffer load is ordered before the owner's later buffer store.