Lock-free queues and ring buffers

For an illustrative ring with capacity C, let w count published writes and r count completed reads. Treat these as unbounded logical integers while proving the invariant: occupancy stays between zero and C. Logical item i occupies slot i modulo C. Exactly one producer advances w and exactly one consumer advances r, so neither side needs a compare-and-swap to compete with another writer of its own counter. A bounded machine implementation still needs an explicit counter-wrap argument; mathematical integers do not automatically justify overflowing signed arithmetic.

The producer initializes a slot before publishing an updated write counter with release ordering. The consumer uses an appropriate acquire observation of that publication before reading the payload. In the reverse direction, the consumer finishes reading before releasing the updated read counter; the producer acquires that information before overwriting reusable storage. These two handoffs protect ordinary payload accesses. A stale observation can temporarily report full or empty, but must never authorize an unsafe read or overwrite. Padding counters can reduce false sharing without changing the proof.

A Michael–Scott-style linked queue begins with a dummy node. An enqueue prepares a node privately, then tries to link it after the observed last node. The successful link is the enqueue publication and linearization event in that algorithm. Updating the tail hint can happen later: another thread can notice the lag and help advance it. This separation matters when the original enqueuer is descheduled after linking; useful work need not wait for that particular thread to resume.

A successful nonempty dequeue advances the head to the next node; that next node becomes the new dummy. The removed old dummy cannot simply be freed because another operation may still hold its address. A reclamation protocol supplies the missing lifetime guarantee. Read the original pseudocode with its allocator assumptions rather than transplanting a few CAS operations into arbitrary allocation code. The abstract FIFO proof, the language memory-model proof, and the reclamation proof are separate obligations, even when a library packages all three.

A bounded ring needs a defined full-queue policy: reject, retry, shed work, or block through an external mechanism. Reserving a slot with fetch-add does not by itself publish initialized data. In a multiple-producer design, a paused producer may leave a reservation hole that prevents consumers from taking later items. Whether the complete algorithm is lock-free depends on how it handles such holes, allocation, and stalled participants; the mere presence of atomic instructions proves no progress property.

Use the queue lab to separate load imbalance from synchronization correctness. Compare independent fixed-rate experiments: choose Reset, explicitly set both arrival and service rates, predict the slope, then Play or Step. Use arrival four and service three for growth; for draining choose Reset again, explicitly set arrival two and service three, predict, then Play or Step. Editing a control pauses but retains elapsed time and recomputes from the initial backlog; it is not a live rate change preserving queue contents. Its initial backlog is four items and its fluid approximation has no ring capacity, reservations, threads, or CAS failures. The separately displayed M/M/1 residence time additionally assumes Poisson arrivals, exponential service, and a stable single server. Neither picture validates a concurrent queue implementation; use it to ask whether a correct queue will still grow under the offered workload.