The question this answers
What must remain true under every possible interleaving — and how does naming it decide which primitive you need?
A withdrawal handler and a bounded work queue in the same service: account.withdraw(amount) on a balance, and queue.push(job) against a queue with capacity 500.
account.balance and account.ledger (a two-field invariant), and queue.items with queue.size (a size-versus-capacity invariant). Both are reachable from every request-handling task.
Three, stated concretely: balance >= 0 and balance === opening - sum(ledger); queue.items.length <= 500; and *one owner per job* — no job is handed to two workers.
Synchronization exists to preserve this sentence. If a schedule can make it false, the code is wrong no matter which primitive it uses.
The invariant decides the primitive, not the other way round
Engineers reach for a mutex the way they reach for a try/catch: as a general-purpose safety gesture. The result is code that is locked and still wrong, because the lock protects a *variable* while the invariant spans two, or protects one method while the invariant spans a sequence of three calls made by the caller.
Naming the invariant first changes the shape of the answer. "balance >= 0" tells you the region is check-plus-deduct, not just deduct. "items.length <= 500" tells you the region is check-plus-push, and also that a *counting semaphore* with 500 permits expresses it more directly than a mutex does (Semaphores: Counting Permits as a Resource Limit). "One owner per job" tells you the invariant is not about a number at all but about a set partition, which usually wants a claim operation that is atomic against itself — a conditional update, not a lock (Optimistic Concurrency Control).
A good invariant is falsifiable. You should be able to write a function check() that returns a boolean, run it against the live state, and get an answer. "The data is consistent" fails that test and is therefore not an invariant; it is a wish. "balance === opening - sum(ledger.withdrawals)" passes, and it is also — not by coincidence — exactly the reconciliation job you want in production.
| Invariant | Falsifiable check | Region it implies | Primitive it suggests |
|---|---|---|---|
| balance >= 0 | balance >= 0 after every operation | read balance → compare → deduct, as one unit | Mutex over the check-then-act pair, or a conditional UPDATE ... WHERE balance >= ? |
| balance === opening − sum(ledger) | recompute from the ledger and compare | both writes — the balance field and the ledger append — as one unit | Mutex spanning both fields, or a transaction if the state is in a database |
| queue.items.length <= 500 | length <= 500 at any observation point | read length → compare → push, as one unit | Counting semaphore with 500 permits, which encodes the bound in the primitive itself |
| one owner per job | no job id appears in two workers' in-flight sets | select an unclaimed job → mark it claimed, as one unit | Conditional claim: UPDATE jobs SET owner=? WHERE id=? AND owner IS NULL and check the row count |
Watching `balance >= 0` die
The withdrawal below is written by a careful engineer. It checks the balance before deducting. It is still wrong, and the schedule shows why: the check and the deduction are two separate observations of the shared value, and between them the world changed. Task B's check was truthful when it ran and false by the time B acted on it.
This is where the phrase "protect the invariant, not the variable" earns its keep. Both balance reads are correct reads. Both balance writes are correct writes. If you wrapped only the write in a lock, every step would be individually synchronized and the account would still go negative — the lock would be doing real work and preventing nothing. The region that must be indivisible is precisely the span across which the invariant is allowed to be temporarily false, which here is *check through deduct*.
| # | Task A — withdraw(100) | Task B — withdraw(100) | State |
|---|---|---|---|
| 1 | read balance (150) | · | balance=150 |
| 2 | check 150 >= 100 → true | · | balance=150 |
| 3 | · | read balance (150) | balance=150 |
| 4 | · | check 150 >= 100 → true | balance=150 |
| 5 | write balance = 150 - 100 | · | balance=50 |
| 6 | append ledger: -100 | · | balance=50 ledger=[-100] |
| 7 | · | write balance = 150 - 100 | balance=50 ledger=[-100] ✕ B computed from its own stale read of 150, so it also wrote 50 — the second invariant, balance === opening − sum(ledger), is now false: 50 !== 150 − 100 − 100. |
| 8 | · | append ledger: -100 | balance=50 ledger=[-100, -100] ✕ The ledger says 200 was withdrawn from 150. balance >= 0 held throughout, and the account is still 50 short. |
balance >= 0 invariant was never violated at any observable instant — a monitor watching only for a negative balance would report nothing. The *second* invariant, that balance reconciles against the ledger, is violated by 100. This is why you name every invariant: the one you monitored held, and the one you did not was the one that broke.Invariants that span more than one variable
Single-variable invariants are the easy case and the rare one. balance >= 0 is about one field, and an atomic compare-and-subtract could enforce it alone. But the moment a second field must agree with the first — a ledger, a count cached alongside a list, an index alongside the collection it indexes, a size alongside items — no atomic type helps, because atomicity is a property of a single location and the invariant is a property of a relationship.
That is the practical rule to take away: the number of variables in the invariant sets the floor on the mechanism. One variable and one operation, an atomic will do. One variable but check-then-act, you need a CAS loop or a lock. Two or more variables, you need a lock, a transaction, or a design where the two facts are one value — for example storing the list and its size in a single immutable record that is swapped by one reference write (Safe Publication: Handing Over a Finished Object).
The enqueue below shows the two-variable version and the one-value fix side by side, in pseudocode so that the structure rather than any language's syntax is what is visible.
1# --- the two-variable invariant: size must always equal items.length, and both <= 5002 3enqueue(job):4 if size >= 500: # read #1 (shared)5 return REJECTED6 items.append(job) # write #1 (shared)7 size = size + 1 # write #2 (shared) <- invariant is false between #1 and #28 9# Failing schedule: A reads size 499 -> B reads size 499 -> A appends -> B appends10# -> A sets size 500 -> B sets size 50011# items.length is 501, size says 500. Both the capacity bound and the12# size-equals-length invariant are now false, and nothing errored.13 14# --- fix 1: make the region indivisible. The lock's scope is exactly the15# span across which the invariant is allowed to be false.16 17enqueue(job):18 with lock: # region = check + both writes. Not less, not more.19 if size >= 500: return REJECTED20 items.append(job)21 size = size + 122 23# --- fix 2: remove the second variable. One value, one write, no window.24# Readers see either the old snapshot or the new one, never a mix.25 26enqueue(job):27 loop:28 old = state # one reference read29 if old.items.length >= 500: return REJECTED30 new = Snapshot(old.items + [job]) # size is derived, never stored31 if compare_and_swap(state, old, new): return ACCEPTED32 # else: someone else swapped first; our snapshot is stale, retry33 34# fix 2 costs an allocation per enqueue and unbounded retries under heavy35# contention. It buys lock-free reads and one fewer invariant to maintain.36# See [[optimistic-concurrency-control]] and [[copy-on-write-sharing]].Key points
- Synchronization has exactly one purpose: preventing an invariant from being observed false. If you cannot name the invariant, you cannot evaluate the lock.
- A real invariant is falsifiable — you can write
check()and run it. "The data is consistent" is not an invariant. - The invariant determines the region: the critical section is the span across which the invariant is temporarily false.
- The number of variables in the invariant sets the floor on the mechanism: one variable and one op → atomic; one variable, check-then-act → CAS or lock; two or more → lock, transaction, or a single-value redesign.
- The invariant you monitor is not necessarily the one that breaks. Enumerate all of them — the balance-non-negative check passed while the ledger reconciliation failed.
- Some invariants are better expressed by a different primitive entirely: a capacity bound is a semaphore, an ownership claim is a conditional update.
The loop, answered
Every field is required, which is why no lesson here can recommend concurrency without naming the interleaving that breaks it, the complexity it adds, and the simpler thing to consider first.
- • Write the invariant as a boolean expression over the shared state, using only fields you could actually read at runtime.
- • Identify every code path that can make it false — these are the writers, and the set is usually larger than expected.
- • For each writer, mark the first statement after which the invariant is false and the statement at which it is true again. That span is the candidate critical section.
- • For each reader, ask whether it can execute inside any writer's span. If it can, the reader is part of the protected region too.
- • Choose the smallest mechanism that makes the span indivisible with respect to every other participant — and re-derive it if the invariant later grows a variable.
- • A checks 150 >= 100; B checks 150 >= 100; A writes 50; B writes 50.
balance >= 0never fails, and the ledger invariant fails by 100. - • A checks; A writes 50; B checks 50 >= 100 → false; B rejects. Correct, and the schedule that every test produces.
- • Enqueue: A reads size 499; B reads size 499; both append; both set size = 500.
items.lengthis 501 andsizeis 500 — two invariants broken by one window. - • With the region locked: A holds the lock through check-append-increment; B blocks at the check and observes size 500, rejecting correctly. No interleaving breaks either invariant.
- • With the snapshot design: A and B both read the same
old; one CAS succeeds and the other observes a changed reference, retries, sees 500 and rejects. No interleaving breaks it, at the cost of a retry.
- • Naming an invariant guarantees nothing by itself — it is a design act, not a mechanism. What it guarantees is that the mechanism you pick can be evaluated instead of assumed.
- • A lock over the correct region guarantees the invariant holds at every point outside the region. It does not guarantee it holds *inside* — it guarantees nobody can look.
- • An atomic type guarantees indivisibility of one location. It explicitly does not guarantee that two atomic variables agree with each other at any instant.
- • A database transaction guarantees the invariant across the rows it touches, under the configured isolation level, and guarantees nothing about your process-local cache of the same data. See The Database Solves Concurrency For Its Data, Not For Your Memory.
- • The invariant sets the minimum size of the critical section, and therefore the floor on contention. A wide invariant is expensive to hold regardless of which primitive you pick.
- • Splitting one wide invariant into several narrow ones — per-account balances rather than one global ledger lock — is the single most effective contention reduction available, and it is a modelling change, not a tuning change.
- • An invariant spanning an I/O call is the pathological case: the region cannot be shrunk without changing the design, so the lock is held for a network round trip. See Lock Scope: What You Hold It Across.
- • Broken invariant with no error — the defining failure. Balance and ledger disagree; nothing throws.
- • Locked but still wrong — the lock protects a single write while the invariant spans a check-then-act, so every access is synchronized and the outcome is unchanged.
- • Monitored the wrong invariant — the alert watches
balance >= 0, which held, whilebalance === opening − sum(ledger)silently failed. - • Invariant drift — a new field is added to the structure and nobody updates the invariant or the lock's scope, so the region is now too narrow by one write.
- • Lost update on the check-then-act pair, which is the Interleavings: The Schedule Is Part of the Program failure viewed through the invariant lens.
- • Always, before choosing a primitive — the discipline costs a sentence and rules out entire categories of wrong answer.
- • In code review, where "what invariant does this lock protect?" is the highest-yield question you can ask about a concurrency diff.
- • When designing a monitor: a falsifiable invariant is already a reconciliation query, so the design work doubles as observability work.
- • When deciding whether concurrency is worth it at all — an invariant spanning six variables and two services is a signal to keep the operation sequential.
- • When the invariant is stated so broadly that the implied region is the entire request. That is not an invariant, it is a refusal to analyse, and it produces a global lock.
- • When it is used to justify locking state that no second task can reach. Invariants over task-local data need no enforcement.
- • When the invariant genuinely belongs to the database and is re-implemented in application memory, producing two sources of truth that disagree under partial failure.
- • Write the invariant as a query and run it on a schedule: recompute the balance from the ledger, compare
sizeagainstlen(items), count jobs with two owners. Mismatches per hour is the metric. - • Assert the invariant in debug builds at the boundaries of every critical section — cheap, and it catches a region that is one statement too narrow.
- • Count invariants per lock. A lock protecting five unrelated invariants is a lock that will be held too long; a single invariant protected by three different locks is a bug waiting for a schedule.
- • Track how often the reconciliation job corrects something. Zero forever is the goal; a non-zero rate that scales with traffic is the signature of a too-narrow region.
- • Each named invariant becomes a documented obligation on every future writer, and most languages provide no way to attach it to the data, so it lives in a comment and decays.
- • Multi-variable invariants force a lock or transaction where a single atomic would have done, adding a synchronization object, a lock-ordering obligation and a deadlock surface.
- • The single-value redesign removes an invariant but adds allocation, a retry loop and a staleness window that readers must be told about.
- • Every invariant you enforce in application memory is an invariant the database also thinks it owns; keeping the two definitions in step is ongoing work.
- • Let the database own the invariant: a
CHECKconstraint, a unique index, or a conditionalUPDATE ... WHEREis enforced once, correctly, for every writer including the ones you did not write. See The Database Solves Concurrency For Its Data, Not For Your Memory. - • Remove the invariant by removing the second variable — derive
sizefromitemsinstead of storing it, and there is nothing left to keep in agreement. - • Give the invariant a single owner task and send it messages; an invariant touched by exactly one actor cannot be broken by a schedule. See The Actor Model.
- • Express the invariant in the primitive: a capacity bound is exactly what a counting semaphore is for, and using one removes the hand-written check entirely. See Semaphores: Counting Permits as a Resource Limit.
The lost update, step by step
| # | Task A — counter++ | Task B — counter++ | State |
|---|---|---|---|
| 1 | rA ← counter | · | counter=0 rA=0 rB=— |
| 2 | · | rB ← counter | counter=0 rA=0 rB=0 |
| 3 | rA ← rA + 1 | · | counter=0 rA=1 rB=0 |
| 4 | counter ← rA | · | counter=1 rA=1 rB=0 |
| 5 | · | rB ← rB + 1 | counter=1 rA=1 rB=1 |
| 6 | · | counter ← rB | counter=1 rA=1 rB=1 ✕ 2 increments completed, counter = 1 |
if (balance >= 100) withdraw(100) — drive it until it overdraws
balance = 100
withdraw(amount): # both tasks run this concurrently
b = read(balance) # 1
if b >= amount: # 2 <- decided on a value that may already be stale
debit(amount) # 3| # | Withdrawal A (100) | Withdrawal B (100) | State |
|---|---|---|---|
| 1 | rA ← read balance | · | balance=100 paidOut=0 |
| 2 | if rA >= 100 | · | balance=100 paidOut=0 |
| 3 | debit 100 | · | balance=0 paidOut=100 |
What people believe, and what is true
The lock makes it thread-safe.
A lock makes a *region* mutually exclusive. Whether that produces correctness depends entirely on whether the region matches the invariant's span. A lock around the wrong region is fully functional and fully useless.
Each method is synchronized, so the class is safe.
Per-method locking protects each call and nothing about a sequence of calls. if (!map.containsKey(k)) map.put(k, v) on a fully synchronized map is still a race, because the invariant spans both calls.
If I make every field atomic, the object is consistent.
Atomicity is per-location. Two atomic fields can be read at an instant where one has been updated and the other has not — which is exactly the balance-and-ledger failure above.