The Vyukov MPMC ring's synchronization lives entirely in its acquire/release gate, and the shipped queues over-specify the counter

The bounded Vyukov MPMC queue is one of the most-copied lock-free structures in systems code: it is the design behind Rust crossbeam ArrayQueue, C++ rigtorp MPMCQueue and Folly MPMCQueue, and countless serving-side ring buffers. Its correctness rests on a per-cell monotone sequence gate between producer and consumer, plus two shared position counters that dispense slots. The exact C11 memory orderings on its atomic operations are folklore, copied from one implementation to the next and never checked against a mechanized memory model. This project pins them down: acquire on the gate load and release on the gate store are each necessary and sufficient, no seq_cst is required anywhere including the cross-lap cell-reuse hazard, and the position counters can be relaxed for the payload handoff. The shipped queues confirm the gate exactly and over-specify the counter with seq_cst.

Two engines, each used only where it is sound

Two independent tools, chosen so each carries only the direction it can:

• Loom (Rust, exhaustive operational model checker) is used for the necessity direction. Loom under-approximates the C11 model (its own documentation states a bug can exist even when Loom reports none), so a Loom SAFE verdict is not a proof of race-freedom, but a Loom UNSAFE verdict is a real, witnessed race. We use Loom only for its sound direction: to exhibit the concrete races that weakening the gate produces.
• herd7 on the RC11 axiomatic model (rc11.cat) is used for the sufficiency direction. herd7 is sound and complete for the model it is given, so its verdicts on the ring's synchronization litmus tests are proofs: it decides exactly which outcomes RC11 permits.

The queue's payload handoff is abstracted into small litmus tests that herd7 decides under rc11.cat, and the full parameterized ring is model-checked under Loom for the necessity races. Neither claim leans on Loom's unsound SAFE direction.

The gate is necessary and sufficient (herd7, RC11-exact)

The core handoff is a message-passing pattern: the producer writes the payload, then stores the sequence gate; the consumer loads the gate, then reads the payload. With release on the store and acquire on the load, the outcome where the consumer sees the updated gate but a stale payload is forbidden under RC11; with the gate relaxed, it is permitted:

litmus (rc11.cat)	gate orderings	forbidden stale-read outcome
gate message-passing	store release, load acquire	Never (RC11-forbidden: handoff safe)
gate message-passing	store relaxed, load relaxed	Sometimes (RC11-permitted: a race)

The cross-lap cell-reuse hazard, where a slow producer on lap 2 might overwrite a payload a lap-1 consumer is still reading, is the same mechanism in the other direction: the consumer reads the payload, then releases the gate to free the cell; the next producer acquires the gate, then writes. Modeling the payload as a non-atomic location so herd7's race detector is the oracle:

litmus (rc11.cat)	gate orderings	cross-lap payload access
cross-lap reuse	release / acquire	no data race (read ordered before the reuse write)
cross-lap reuse	relaxed	undefined behavior (a data race)

So acquire/release are exactly what is needed, and they suffice for the cross-lap case with no seq_cst fence, unlike the Chase-Lev deque which was shown to need one. That answers the pre-registered fear directly: there is no hidden SC requirement here.

The counter is not on the payload's synchronization path (herd7)

The position counters dispense slots; the question is whether their ordering carries any of the payload happens-before. It does not. Adding a relaxed counter store on a separate location alongside the release/acquire gate leaves the handoff's stale-read outcome forbidden:

litmus (rc11.cat)	counter ordering	stale-read outcome
gate handoff plus counter	relaxed counter, release/acquire gate	Never (RC11-forbidden)

The payload ordering flows entirely through the gate, so a relaxed counter is off the payload's happens-before path. That litmus establishes only locality (a relaxed store to a location the handoff never reads cannot carry payload ordering); the separate question, whether a relaxed counter CAS under producer contention could misroute two producers to the same cell, is answered operationally by Loom. With two producers racing the enqueue counter at N=2, the canonical config (relaxed counter) is SAFE across the full enumeration, and the integrity check is a strict exactly-once assertion (each popped value was pushed and appears at most once, so a duplicate from a misroute would fail it) alongside the S1 race detector that would fire on two concurrent writes to one cell. Strengthening the counter CAS to acq_rel under the same contention changes nothing. So the relaxed counter is sufficient for the handoff both axiomatically (off the HB path) and operationally (no misroute under contention). The counter still must be atomic to dispense unique slots, which is a property of read-modify-write atomicity and the per-location modification order, not of any ordering above relaxed.

Loom confirms the necessity operationally

Independently, the full parameterized ring under Loom, at the smallest valid ring size N=2 with three items forcing cell-0 reuse at position 2 (N=1 is degenerate: its data-ready and cell-free sequence encodings collide, a real race Loom catches), gives the sound necessity results: the all-relaxed config is UNSAFE (a witnessed race), the mutant that weakens the gate store to relaxed is UNSAFE, and weakening the gate load acquire to relaxed or the gate store release to relaxed is each UNSAFE. Two independent engines therefore agree that both gate operations are load-bearing: herd7 shows the relaxed gate permits the stale read under RC11, and Loom exhibits the concrete race.

The single-op sweep off the canonical config (gate load acquire, gate store release, counters relaxed) finds no safe single-op weakening: the two gate operations are races when weakened, and the counter operations and reloads are already relaxed. This establishes that canonical is the minimal point under single-op moves; a stronger claim of a globally unique minimum would require testing fence-insertion and multi-op trades, which this study does not do, so it is not made.

Auditing the shipped queues

Extracting the orderings from the current sources and placing them on the frontier:

operation	necessary and sufficient	crossbeam ArrayQueue	rigtorp MPMCQueue
gate seq load	acquire	acquire	acquire
gate seq store	release	release	release
position reload	relaxed	relaxed	acquire
position counter update	relaxed	seq_cst CAS + seq_cst fences	seq_cst fetch_add / CAS

Orderings read from the current upstream sources: crossbeam-queue array_queue.rs (gate stamp load Acquire, stamp store Release; tail/head CAS SeqCst success, Relaxed failure; SeqCst fences in the full/empty re-check; tail/head reload Relaxed) and rigtorp MPMCQueue.h (turn load Acquire, turn store Release; head_/tail_ fetch_add and compare_exchange at the default SeqCst; head_/tail_ reload Acquire). Both implementations use exactly the necessary-and-sufficient acquire/release on the sequence gate: the folklore gate orderings are correct and minimal. Both then put seq_cst on the position counter, where the RC11 analysis shows relaxed is sufficient for the payload handoff, and rigtorp additionally uses acquire on the counter reload. Stated honestly: the model proves relaxed counters suffice for the handoff (S1 and S2) of the core enqueue/dequeue. crossbeam's seq_cst fences sit in a full/empty re-check path that returns a precise Full/Empty rather than a spurious one and that this handoff model does not include; rigtorp's fetch_add gets unique tickets from atomicity regardless of ordering. So the counter seq_cst is stronger than the payload handoff requires and is a candidate weakening, with the full/empty semantics being the remaining thing a complete audit of those specific implementations would model. The gate result, acquire/release exactly, is unconditional.

Pre-registration scorecard (PREREG.md, committed before results)

	prediction	outcome
P1	canonical is safe	holds (Loom safe operationally; herd7 forbids the stale read)
P2	both gate ops load-bearing (weakening either is a race)	holds, herd7 (RC11-permitted) and Loom (witnessed race)
P3	relaxed counter suffices	holds for the handoff: off the payload HB path (herd7) and no misroute under 2-producer contention (Loom exhaustive, exactly-once integrity)
P4	monotone, unique minimum	downgraded: canonical is minimal under single-op moves; global uniqueness not tested, not claimed
P5	no seq_cst anywhere, including cross-lap	holds (herd7: cross-lap safe under release/acquire, race under relaxed)

Practical read

If you write or copy a Vyukov MPMC ring, acquire on the gate load and release on the gate store are the only load-bearing orderings, they suffice even for the cross-lap cell-reuse case with no seq_cst, and the position counters can be relaxed for the data handoff. The two most-used implementations already use the minimal gate, and both use a stronger-than-necessary seq_cst on the counter that the payload handoff does not require.

Scope

herd7 7.58 on rc11.cat (sound and complete for RC11, used for the sufficiency proofs) and Loom 0.7.2 (used for the necessity races only, since its SAFE verdicts are not sound under weak memory), CPU only on the M4. The litmus tests abstract the ring's payload handoff and cross-lap reuse; the Loom bound is N in {2, 3} with a cross-lap-forcing item count. The claims are data-race-freedom and integrity of the payload handoff; the counter result is about the handoff and is scoped away from the full/empty machinery of specific implementations.

Reproduce

HERD=~/.opam/herd/bin/herd7; RC11=~/.opam/herd/share/herdtools7/herd/rc11.cat
for f in litmus/*.litmus; do echo "$f"; $HERD -model $RC11 "$f" | grep Observation; done
RUSTFLAGS="--cfg loom" cargo build --release --bin derisk && python run_sweep.py   # Loom necessity races

License

MIT.