A counter with two atomic moves guards a pool of permits. P takes one — and waits if none are left; V gives one back. That single integer, and the rule that it never goes negative, is enough to admit exactly k holders and not one more. It is runnable: this page enumerates every interleaving of the competing threads and proves the count stays sound over all of them. Down the center, data flows — permits and threads go in, the model runs every schedule, the proof comes out. The blue team builds and defends it; the red team tries to break it.
source Dijkstra, Cooperating Sequential Processes (1965), EWD123 — cs.utexas.edu/~EWD/…/EWD123.html. Rendered, not quoted.
Safety is not asserted; it falls out of one integer and two atomic rules:
count = permits currently free. P (wait): if count > 0 decrement, else block until a V raises it. V (signal): increment, waking a waiter. The held units = k − count, so the sole invariant count ≥ 0 is exactly "no more than k are held at once."
For the current config, exhaustive over all interleavings:
| fact | value |
|---|
Dijkstra's 1965 semaphore is the primitive beneath the primitives. A binary semaphore (count in {0,1}) is a lock — the door to the-mutex. A counting one with a full/empty pair is the bounded buffer of the-producer-consumer; a permit-counted reader gate is the-readers-writers.
Each of those spheres takes this one as its premise — they add ownership, buffering, or role-fairness on top of the same P/V and the same "count never negative" law proven here.
The blue team's live check: re-enumerate the canonical cases — a binary semaphore over two threads, a k=2 pool over three — and confirm the caps against known truth. If red tampers, this badge is where it shows.
A semaphore starts with k permits. Some number of threads each run the same short program: P (acquire) · critical section · V (release). The two operations are atomic and their names are Dutch:
| op | Dijkstra | means | effect |
|---|---|---|---|
| P | Prolaag | try-to-lower | wait, then count−1 |
| V | Verhogen | raise | count+1 |
Feed a permit count k and a thread count N into the panel below. When N > k there is contention: some P must block.
Every thread runs P · critical-section · V. The engine explores all interleavings.
Change k or N — the cap is recomputed by exhaustive enumeration on the spot, never looked up.
What the machine produces, proven over every interleaving: the count never goes negative, at most k threads hold at once, and when N > k the surplus threads block on P until a V arrives. At k=1 that cap is exactly mutual exclusion — the semaphore is a lock.
The blue team's witness (left) confirms the caps live; the red team (right) tries to over-admit.
Because any thread may V — not only the one that did P — a semaphore is not a mutex in the strict sense (a mutex has an owner). Modern code prefers monitors, condition variables, and scoped lock-guards that bind acquire to release. The semaphore is not the answer; it is the first proof that a single counter can make interleavings safe.
"A semaphore is just a mutex." Cut. A mutex has ownership (only the locker unlocks) and count ∈ {0,1}. A counting semaphore admits k>1 holders and any thread may signal it.
"Semaphores prevent deadlock." Cut. They are the classic source of it — acquire two in opposite orders and both hang. Order discipline, not the primitive, is the fix. AMBER
"P and V are arbitrary letters." Kept, corrected. P = Prolaag (try-to-lower), V = Verhogen (raise) — Dutch, from Dijkstra's own EWD123.
The red team's move: make P non-blocking — let the count fall below zero and never wait. Now more than k threads acquire k permits at once. The blue team's witness (window 7) is watching.
Strip the wait from P and the pool cap breaks: an interleaving where every thread does P before any V drives the count negative and admits N holders into k permits. The witness recomputes, disagrees with the known cap, and turns red. Nothing is faked; the attack is real and it is caught.