A fast producer and a slow consumer share one bounded buffer. Three semaphores keep them in step — empty slots, full slots, and a mutex — so the buffer never overflows, never underflows, and every item is consumed exactly once. Down the center, data flows: items go in, the engine coordinates, results come out. The blue team builds and defends it; the red team tries to break it.
source Dijkstra, Cooperating Sequential Processes (EWD123, 1965), §4 bounded-buffer / producer–consumer — cs.utexas.edu/~EWD/…/EWD123. AMBER: archive transcription, not a paginated journal of record. Rendered, not quoted.
The buffer holds at most N items. Two counting semaphores track how many slots are which way; one binary mutex guards the shared indices:
// init empty=N full=0 mutex=1 producer: consumer: P(empty) P(full) P(mutex) P(mutex) put item take item V(mutex) V(mutex) V(full) V(empty)
P waits then decrements; V increments. A producer that finds empty=0 blocks — that is the back-pressure. Order matters: the slot-count P comes before P(mutex), or the two deadlock.
Live:
This is pipelining with back-pressure. The producer runs ahead until the buffer fills, then the empty semaphore stalls it until the consumer drains a slot — the two auto-throttle to the slower of the pair, no polling, no waste.
It is the semaphore coordinating a bounded buffer — the pattern beneath every queue, pipe, and channel. Each sphere is the next one's premise.
The blue team's live check: re-explore every interleaving of the threads and confirm the buffer never overruns, the mutex never lets two writers in, and consumed = produced. If red drops the back-pressure, this badge is where it shows.
The producer generates a stream of items — A, B, C, … — and offers them to the buffer one at a time. The consumer removes them in order. Neither knows the other's speed; the semaphores are the only contract between them.
Each produce asks for an empty slot; each consume asks for a full one. When the answer is "none", the thread waits. Feed the stream into the panel below.
Every op enforces the real semaphore rule — a full buffer blocks the producer, an empty one blocks the consumer. Nothing is queued past N.
What the machine guarantees, checked by exhaustive enumeration of interleavings — not sampled, not asserted by hand: 1 producer + 1 consumer at N=1 gives 11 reachable states, every one in-bounds; 2 producers + 2 consumers at N=2 gives 171 states with exactly one valid outcome multiset — every item consumed once, none lost, none duplicated, and no interleaving deadlocks.
The blue team's witness (left) re-runs this live; the red team (right) tries to make an item vanish.
Nor is the naming free: this model gives no fairness — one producer can starve another forever, and the consumer sees no priority. "Correct" here means safe, not fair. That is why later work (monitors, channels, lock-free queues) exists — the semaphore is the first solution, not the last.
"The mutex alone makes it safe." Cut. The mutex only stops two threads mangling the indices. It does nothing about overflow — that is the empty semaphore's job. Drop it (window 6) and the mutex happily lets you overwrite.
"A bigger buffer removes the need to block." Cut. Any finite N fills if the producer is faster on average. Back-pressure is not tuning; it is the only thing keeping a bounded buffer bounded.
"empty + full is always N." Kept, corrected. True only when the buffer is quiescent. Mid-operation the exact conserved law is empty + full + in-flight = N — verified at every reachable state.
The red team's move: drop the producer's back-pressure — the empty-slot semaphore that makes a producer wait on a full buffer. Now it writes anyway, over a live item. The witness (window 7) is watching.
With the guard gone, a producer that meets a full buffer overwrites the oldest unconsumed item — it is lost, so consumed ≠ produced. The witness recomputes, disagrees, and turns red. Nothing is faked; the attack is real and it is caught.