Let many read at once — but a writer must be alone. Two classes of process share one datum: readers may pile in together, a writer needs the room to itself. The solution is a read-counter guarded by its own mutex plus one exclusion semaphore. It is runnable, and the exclusion is checked exhaustively over every interleaving of the threads — not asserted, model-checked. Data flows down the center: requests in, the semaphores grant access, the proof comes out. The blue team builds and witnesses; the red team breaks it.
source P. J. Courtois, F. Heymans, D. L. Parnas, Concurrent Control with "Readers" and "Writers", CACM 14(10), 667–668 (1971) — doi:10.1145/362759.362813. Rendered, not quoted.
Nothing is memorised; the guarantee falls out of two semaphores and a counter:
wrt — a binary semaphore that means "the datum is free". The first reader to arrive takes it; the last to leave gives it back. A writer takes it directly. So a writer and any reader can never both hold it.
readcount — how many readers are inside, and mutex — a second binary semaphore that guards readcount itself, so two readers never corrupt the count while incrementing.
Live invariants over every reachable state of the current model:
| invariant | holds? |
|---|
"Many readers or one writer" is not a primitive — it is assembled from Dijkstra's P/V. Every P here blocks a thread until the count is positive; every V wakes it.
Courtois–Heymans–Parnas 1971 is the first to layer a policy (readers preferred) on top of the raw semaphore. That layering is the read/write lock behind every database row and every RwLock you have ever used. Each sphere is the next one's premise.
The blue team's live check: re-model-check the exclusion over four configurations of readers and writers, exploring all interleavings, and confirm the known truth — writers alone, readers together. If red tampers, this badge is where it shows.
Threads arrive wanting the one shared datum. Each is one of two kinds:
| kind | wants | may share? | protocol |
|---|---|---|---|
| reader | to observe | yes — with other readers | P(mutex); rc++; if first P(wrt); V(mutex); READ; P(mutex); rc--; if last V(wrt); V(mutex) |
| writer | to mutate | no — exclusive | P(wrt); WRITE; V(wrt) |
The arrivals interleave in every order the scheduler permits. That whole set of orders is what you feed the panel — and the panel proves the rule survives all of them.
Every interleaving of these threads is enumerated by breadth-first search — a real bounded model-checker.
Change readers or writers — the exclusion is re-proven on the spot by exploring every interleaving, never looked up.
What the machine produces, proven over all interleavings: a writer is never in the critical section while any reader is (nor a second writer); yet up to N readers are there together — readers do not serialise like a plain mutex; a writer waits until the last reader leaves; and readcount never corrupts, because its own mutex guards it. The current config's verdict is above; the guarantee is the output.
The blue team's witness (left) re-checks this live; the red team (right) tries to make a reader see a half-written value.
The 1971 paper knew this: its second algorithm gives writers priority, trading the symmetric starvation the other way. There is no free lunch — a truly fair lock needs a third mechanism (a turnstile / queue). "Correct" here means mutual exclusion, not fairness; the panel proves the first, not the second.
"A reader–writer lock is just a mutex." Cut. A plain mutex serialises readers too — max 1 in the section. The model here reaches N concurrent readers; that concurrency is the whole point, and it is measured live.
"One semaphore is enough." Cut. Without the second mutex guarding readcount, two readers can race the counter — first-reader detection breaks and wrt is double-acquired or leaked. Two semaphores, not one.
"It's fair to both sides." Kept, corrected. It is safe for both, fair to neither by default — readers-preference starves writers (window 1). Safety and fairness are different proofs.
The red team's move: let a writer skip its exclusive P(wrt) and mutate while readers are still inside — so a reader observes a half-written value. The blue team's witness (window 7) is watching.
Skip the writer's acquire and an interleaving appears where writer-in-CS and reader-in-CS coincide — the exclusion invariant fails on that state, the witness recomputes, disagrees, and turns red. Nothing is faked; the attack is real and it is caught.