Commentary: distributed-lock

Five lock servers, majority acquire, TTL leases — Redlock's shape. Not one of them ever lets two clients hold the lock at the same instant, and the audit proves it. The resource is corrupted anyway, and the fix is not in the lock. A study guide for dlock.py.

cd distributed-lock
python3 demo.py       # the aha (§6)
python3 test_dlock.py # pins every number this page claims

1. Orientation

This toy is a lease-based distributed lock and the thing it is supposed to protect. Five independent lock servers, a majority acquire, a token per grant, and a separate storage service that two clients read from and write to. There are no threads, no sockets, no wall clock and no random number generator. Time is an integer tick and the run is a pure function of an explicit event list.

That is the whole trick, and it is what lets this page do something a description of the problem cannot: audit the lock. Every server remembers every lease it ever issued as a half-open interval [start, end), so after the run you can compare all of them pairwise and ask whether mutual exclusion was ever violated. It never is.

You will see one schedule executed twice. The first time, the storage service accepts any write, which is what a storage service normally does. The second time it enforces fencing tokens. Nothing about the lock changes between the two runs — fencing is a flag on Resource, not on LockService.

The first run ends with the resource holding the output of a client whose lease expired six ticks earlier, on top of a completed critical section that held a valid lease at every instant it ran.

By the end you should be able to:

• say why "the lock never granted overlapping leases" and "only one client wrote at a time" are different claims, and point at the gap between them;
• state the condition under which this failure happens, as an inequality, and check it against a grid of 140 runs;
• explain why neither a shorter lease, a longer lease, nor five servers instead of one removes it — and what each of those does instead;
• explain why re-checking the lock immediately before writing does not help, and say what would have to be true for it to help;
• name the one line that fixes it, and say which system it lives in.

2. The problem this mechanism exists to solve

A distributed lock exists because two processes on two machines want to touch one resource — a file, a row, a job — and only one of them should at a time. There is no shared memory to put a mutex in, so the lock becomes a third service they both talk to.

That third service inherits a problem a mutex does not have: its holder can vanish. A thread holding a pthread_mutex cannot silently stop existing; a client holding a distributed lock can be killed, partitioned, or paused, and the lock server has no way to distinguish "still working" from "gone forever." If the lock is held until explicitly released, one dead client wedges the resource permanently.

The universal answer is a lease: the lock is granted with an expiry, and when the clock passes it the server takes it back without asking. That buys liveness. It costs something specific, and the cost is what this toy is about:

• Safety wants the lease long, so a slow-but-alive holder is never overtaken.
• Liveness wants the lease short, so a dead holder blocks the next client for as little time as possible.

Both goals are about the same number, so a real deployment picks one and lives with the trade. That framing is correct and it is also a trap, because it implies the number can be chosen well enough. It cannot, and the reason has nothing to do with the lock:

So the lock has two jobs that look like one. Mutual exclusion at the lock is a property of the lock service, and it is achievable. Mutual exclusion at the resource is a property of the whole system, and no lock service can provide it alone. §6 is the difference between those two, measured.

3. Background you need

4. The mental model

Two clients, one lock service, one storage service. Time runs left to right in ticks. A is paused for the stretch drawn as zzz.

The two intervals [0, 10) and [12, 15) do not touch. That is not a near-miss: there are two whole ticks between them where nobody holds the lock at all. The lock did its job perfectly, and the resource still ended up holding "A".

The reason is the one gap the diagram cannot draw: between the moment A last observed "I hold the lock" and the moment A's write reaches the storage service, A did not execute. Everything the lock knows is from before that gap. Everything the resource sees is from after it.

5. Reading the source

In reading order. Every excerpt is captioned with its provenance so it cannot drift from the file.

5.1 LockServer.acquire — the line that makes it a lease

def acquire(self, client, now, ttl):
    """Grant a lease, unless a live one is outstanding. The expiry test is
    the only thing that releases a lease from a client that never came
    back -- there is nobody to ask whether A is still alive."""
    if self.holder is not None and now < self.expires:
        return None
    self.token += 1
    self.holder = client
    self.expires = now + ttl
    self.grants.append(dict(server=self.id, client=client, token=self.token,
                            start=now, end=self.expires))
    return self.token

Two clauses, and the second one is the entire difference between a lock and a lease. Without now < self.expires this is an ordinary mutual-exclusion lock: held until released, and safe in the strongest sense. It is also useless, because A is paused and will never release. Dropping that clause and re-running the same schedule:

That is the trade from §2 in its most literal form. The expiry clause is not a concession to practicality; it is the only reason the system makes progress, and it is also the only reason the corruption in §6 is possible. You cannot delete one without deleting the other.

Note also that self.token increments on every grant, before any of the lease logic. The token is not something the fencing feature adds later — it falls out of the fact that the server has to count grants anyway.

5.2 LockService.acquire — the quorum, and where the token comes from

def acquire(self, client, now, ttl):
    """Ask everyone, keep it if a majority said yes, otherwise hand back
    the partial grants immediately. Returns the highest token seen, which
    is the fencing token."""
    toks = [s.acquire(client, now, ttl) for s in self.servers]
    got = [t for t in toks if t is not None]
    if len(got) >= self.quorum:
        return max(got)
    for s, t in zip(self.servers, toks):
        if t is not None:
            s.release(client, now)
    return None

The hand-back loop is not decoration. A client that grabbed two of five and failed must not keep them, or the next acquirer is blocked by a lock nobody holds — test_partial_grant_is_handed_back pins that.

max(got) deserves a flag. In this toy the five servers stay in lockstep, so every grant yields the same token on all five and the maximum is unambiguous. That is a property of the schedule, not of the algorithm: if a client acquires on servers 1–3 and a later one on 3–5, the counters drift and max across a quorum is no longer guaranteed monotonic. This is the real objection to bolting fencing onto Redlock, and §8 says what production systems do instead.

5.3 Resource.write — the fix, and the fact that it is not in the lock

def write(self, client, now, value, token):
    # `<`, not `<=`: tokens are unique per grant, so a stale writer is
    # always strictly lower, and the loose test lets one holder write
    # twice under a single lease. See commentary 7.3.
    ok = not (self.fencing and token < self.max_token)
    if ok:
        self.max_token = max(self.max_token, token)
        self.value = value
    self.log.append(dict(t=now, client=client, value=value,
                         token=token, ok=ok))
    return ok

Read the class this method is on. It is Resource, not LockServer and not LockService. That placement is the argument of the whole toy: the check that makes the system safe cannot live in the lock, because by the time it matters the lock has already answered correctly and the answer has gone stale in the client's hands. Only the party performing the side effect is in a position to reject it.

Notice also what the resource does not do. It never contacts the lock service, never learns the lease boundaries, never asks who the holder is. It compares one integer against one integer it already had. That is what makes fencing deployable: it needs no coordination, only an ordering.

5.4 scenario — how a stop-the-world pause is modelled

sch.at(0, a_acquire)
sch.at(1, a_read)
sch.at(pause_from, a_pause)
sch.at(pause_to, a_write)
sch.at(pause_to + 1, lambda t: lock.release("A", t))
for t in range(b_arrives, pause_to + 200):
    sch.at(t, b_poll)
sch.run()
return lock, res, st, sch.trace

There is no pause() function and no sleeping. A's read is at t=1 and A's write is at t=16, and nothing is scheduled in between. The pause is the absence of events, which is exactly what a stop-the-world pause is from everyone else's point of view: the process is simply not there for a while, and when it comes back it resumes at the next instruction with all of its local state — including st["a_token"] — exactly as it left it.

This is why the toy does not need to model the pause "correctly." There is nothing to model. A cannot check anything during the pause, cannot renew anything, cannot be interrupted, and is never told the pause happened. Any mechanism you imagine adding to A is a line of code, and lines of code are events, and the pause is defined as the interval containing none of A's.

B's poll loop is the mirror image: an event on every tick from b_arrives onward, so B retries the lock continuously and takes it the instant it becomes available. B is the well-behaved client in this story.

5.5 overlapping_grants — the assertion that makes the point

def overlapping_grants(lock):
    """THE innocence assertion. Every lease every server ever issued, compared
    pairwise as half-open intervals. Empty means the lock never once let two
    clients hold it at the same instant."""
    bad = []
    for s in lock.servers:
        for i, g in enumerate(s.grants):
            for h in s.grants[i + 1:]:
                if g["start"] < h["end"] and h["start"] < g["end"]:
                    bad.append((s.id, g, h))
    return bad

An O(n²) scan over an audit log, which is fine because it runs once at the end and never in the hot path. What matters is that it is retrospective. It does not ask the live lock state anything; it reads the record of what was granted and checks the intervals. That is a stronger claim than "the lock currently looks consistent" — it is "at no instant in this entire run did two clients both hold it."

release truncates the audit record (g["end"] = now) so the log tells the truth about early releases rather than about intentions. Without that, overlapping_grants would be checking a fiction.

5.6 stale_overwrites — what corruption means here

def stale_overwrites(res):
    """THE corruption. An accepted write carrying a token lower than one the
    resource has already applied: an older lease's work landing on top of a
    newer lease's completed critical section."""
    hi, bad = 0, []
    for w in res.log:
        if not w["ok"]:
            continue
        if w["token"] < hi:
            bad.append(dict(t=w["t"], client=w["client"],
                            token=w["token"], applied=hi))
        hi = max(hi, w["token"])
    return bad

"Corrupted" needs a definition that does not depend on the example, or the result is a story rather than a measurement. This is it: an applied write whose token is lower than one already applied. Equivalently — the resource's state now reflects a critical section that started before another critical section that already finished.

It is worth being clear that this is not the same as unlocked_writes, which counts writes made without holding a quorum. Fencing eliminates the first and not the second, and §6.6 shows a run where the second happens harmlessly. The distinction is the difference between "the lock was bypassed" and "the data is wrong."

6. The demo, and what it proves

6.1 The corrupted run

Read the last twelve lines together with the first twelve. On the left is a resource holding 'A' — the output of a client that had no lock — sitting on top of B's completed, correctly-locked critical section. On the right is the complete grant history of all five servers, and not one pair of leases overlaps. There is no bug to find in the lock. That juxtaposition is the toy.

6.2 The arithmetic

Every number above is forced. A acquires at t=0 with ttl=10, so its lease is [0, 0+10) and dies at t=10 — six ticks before A writes.

B arrives at t=12, by which time all five servers report no holder, so B gets a majority immediately: 5 of 5, against a quorum of ⌊5/2⌋+1 = 3. B's lease is [12, 22); it reads at 13, writes at 14, and releases at 15, which truncates its audit record to [12, 15).

At t=14 the resource applies B's write with token 2, so max_token becomes 2. At t=16 A writes with token 1. Without fencing the resource has no opinion about tokens, so 1 < 2 goes unnoticed and 'A' overwrites 'B'. The lost update is visible in the string: both clients read '' and appended one letter, so a correctly serialised run ends at 'AB', and this one ends at 'A'.

The other half of the arithmetic is what the lock service says at the moment of the crime:

At t=9 A holds it. At t=10 nobody does. At t=14, when B writes, B holds it — B did nothing wrong. At t=16, when A writes, nobody holds the lock at all. The write that corrupts the resource is not made by a rival lease-holder; it is made by a client the lock service would have refused, if only the resource had thought to ask. It didn't, and in a real system it can't — the storage service and the lock service are different systems, and the write arrives with nothing attached to distinguish it.

6.3 The same schedule, fenced

One word changed: ACCEPTED became REJECTED (stale token). Everything before it is identical, including the grant table, which is why test_fencing_changes_nothing_about_the_lock compares the two traces line-by-line and asserts they differ only on the final line.

Two things are worth not glossing over. First, A is now told it lost — it gets a False back and can go and re-acquire, which is the behaviour you want and the behaviour the unfenced run cannot provide. Second, the final value is 'B', not 'AB'. Fencing did not recover A's work; it discarded it. That is correct: A's work was computed from a snapshot taken before B's critical section, so applying it in any form would be wrong. Fencing converts silent corruption into a visible, retryable failure. It does not make the pause harmless.

6.4 Does adding lock servers help? No, and here is the table

The first objection to any single-lock-server demonstration is that Redlock uses five. So N is a parameter, and the sweep runs the identical schedule at six different cluster sizes:

Identical in every column, from one server to fifty-one. This is not a surprise once you see why: a quorum protects against lock servers failing or disagreeing, and in this run no lock server fails or disagrees. The failure is on the client side of the RPC, after the answer has already been received correctly by everyone. Adding servers makes the answer more available. It cannot make the answer stay true while the client is not running.

6.5 Does a different lease length help? Also no — and the boundary is an inequality

Shortening the lease does nothing at all — ttl=1 is exactly as corrupt as ttl=10, because B's arrival at t=12 is what gates it, not the expiry. Lengthening it works, and read the last column to see what it costs: from ttl=13 upward, every tick added to the lease is a tick B spends blocked, one for one, until ttl reaches 17 and B is simply waiting for A to finish. The "fix" at ttl≥15 is not a fix. It is the lock declining to expire until after the pause is over, which is the same thing as not having a lease — §5.1's deadlock, rationed.

And it only holds because the pause is 14 ticks. Vary both:

The staircase is not a shape, it is an inequality. A writes at pause_from + pause_len. B is blocked until A's lease expires (t = ttl) or A releases, and cannot start before it arrives, so it acquires at max(b_arrives, min(ttl, release)) and writes two ticks later. Corruption is exactly "B's write lands first," which with b_arrives = 12 reduces to:

test_boundary_formula evaluates that expression against all 140 cells of the grid and asserts it matches every one. Check a few by hand: at ttl=10 the threshold is max(10, 12) = 12, so pause 11 is clean and pause 14 is corrupt. At ttl=25 the threshold is 25, so pause 23 is clean and pause 26 is corrupt. At ttl=1000 the threshold is 1000 and the grid never reaches it, which is why that row is empty of failures rather than safe.

Read the inequality as an instruction and it says: choose a lease longer than your longest possible pause. You do not know your longest possible pause. That is the entire point — the bound does not exist, so the row of dots at ttl=1000 is not a safe configuration, it is a grid that stopped too early.

6.6 Where the effect vanishes

Two boundary conditions, both run.

The first is fencing, on the same 140 cells:

No tuning, no threshold, no assumption about pause length. The token check does not care how long A was gone.

The second is more interesting, because it is the case most systems are actually in. Move B's arrival from t=12 to t=100 — nobody else wants the lock while A is paused — and leave everything else alone:

The data is perfect: 'AB', exactly what a correct serial execution produces. And the last line is the one to sit with. A still wrote without holding the lock — at t=16 its lease had been dead for six ticks, precisely as before. Nothing about the danger changed; the only thing that changed is that no one was there to be hurt by it.

That is where the effect vanishes, and it explains why this bug is rare in production and catastrophic when it is not: contention during a pause is the witness, not the cause. A system that has run this way for two years without incident has not demonstrated that its locking is sound. It has demonstrated that its pauses have not yet coincided with its contention.

7. Design decisions and roads not taken

7.1 A hand-written schedule rather than a randomised search

The schedule is a written adversary (§6.1's disclosure). The alternative — randomise pause lengths and arrival times, run thousands of seeds, report a failure rate — was rejected for a reason specific to this toy: the failure rate would be a function of the parameter ranges chosen, and would therefore mean nothing. §6.5's grid does the honest version of the same job. It is exhaustive over a stated rectangle, it reports a closed-form boundary rather than a percentage, and the boundary is asserted cell-by-cell in the tests.

7.2 The re-check before writing, and why it does not work

This is the fix every reader proposes, and it is the best objection to the toy, so it gets a run rather than a paragraph. Give A a re-check: immediately before writing, ask the lock service whether A still holds a quorum, and write only if the answer is yes. Vary when the check happens relative to the pause:

Checks at t=2, t=5 and t=9 all get a truthful answer — A really did hold the lock at those instants, the lock service is not lying — and the resource is corrupted anyway. Only the check at t=16, after the pause, saves it.

So the re-check works exactly when it is placed after the pause. A cannot place it after the pause, because A does not know a pause is coming, and would not be running if it did. Any check A writes has some amount of A's own execution after it before the write reaches the network, and the pause can land in that gap. Shrinking the gap shrinks the probability and cannot reach zero: this is TOCTOU, and it is unfixable on the checking side by construction.

The important part is that this is not an argument about how small the window is. Even a check on the instruction immediately preceding the write is a check whose answer can be invalidated before the packet leaves. The only party who can evaluate the condition at the moment it matters is the party applying the write.

7.3 token < max_token rather than <=

The comparison in Resource.write looks like a coin-flip judgement call, so it got the variant treatment. Case (a) is the demo's own write; case (b) is a client that wants to write twice under a single lease:

Case (a) is identical under both — 1 is strictly less than 2, so both tests reject it, and the aha does not depend on this character at all. That is worth knowing before writing a paragraph claiming it does; most judgement-call characters turn out to be like this one, and the only way to find out is to run the variant.

Case (b) is where it decides something. With <=, a lease is good for exactly one write, and a holder that wants to write twice under one lock is locked out by its own first write. < is the correct test because tokens are unique per grant, so a genuinely stale writer is always strictly lower and is still caught. This is why real fencing schemes compare epochs with "reject anything older" rather than "require strictly newer" — a leader must be able to keep writing under one epoch.

7.4 N as a parameter, defaulting to 5

Modelling a single lock server would have been ~20 lines cheaper and would have proved the same thing, since §6.4 shows the result is identical from N=1 to N=51. The parameter is there because "you only modelled one server, Redlock uses five" is the first thing a reader thinks, and a table beats an assurance. Keeping N means the reader can also see the quorum sizes — 3 of 5, 26 of 51 — and confirm that a majority really is being demanded.

7.5 No clock drift, and why its absence is not a cheat

Real Redlock's safety argument involves clock drift: the client subtracts elapsed time and a drift factor from the validity period before deciding it holds the lock. None of that is modelled here — every server shares one integer clock and there is no drift at all.

That is a deliberate gift to Redlock, not a simplification against it. Clock drift is a way for the lock to grant overlapping leases, and this toy's claim is that the resource is corrupted even when it doesn't. Adding drift would create a second, independent failure mode and muddy the point: a reader could then say "well, fix the clocks." Here the clocks are perfect, the leases are provably disjoint, and the data is still wrong.

7.6 A read-modify-write critical section rather than a counter

Both clients append their own letter to whatever they read, so the final string is a record of which critical sections were applied and in what order: 'AB' is correct, 'A' is a lost update, 'B' is A's work correctly discarded. A numeric counter would have collapsed those three outcomes into overlapping values and made the transcripts unreadable.

8. What's simplified vs. the real thing

One process, one tick counter, no concurrency. Every client and server is a function call on one thread. Real clients race genuinely, and the interleaving is chosen by kernels and networks rather than by an event list. The toy trades that for reproducibility: the interesting interleaving here is a one-in-many accident in production, and the only way to study it is to schedule it.

No network. RPCs are direct method calls that always succeed instantly. Real acquire calls time out, retry, and — critically — can succeed at the server while the client never hears the reply, which produces a client that does not know it holds the lock, the mirror image of this toy's client that does not know it lost one.

No clock drift or per-server clocks. See §7.5. Redlock's real algorithm has the client measure elapsed time across the acquire round-trip and subtract it, plus a drift allowance, from the lease validity. Redis's own distributed-locks page carries that arithmetic and Kleppmann's critique of it.

No crash-recovery of lock servers. A real Redis node that restarts having lost its state can hand out a lease that is already held, breaking mutual exclusion at the lock itself. That is a genuine second failure mode, and it is excluded here on purpose so that "the lock is innocent" stays literally true.

The token is invented. LockService.acquire returns max(got) across a quorum, and §5.2 flags that this is not monotonic in general. Redlock genuinely cannot produce a fencing token; a consensus-backed service can, because it has a single ordered log to number things with. ZooKeeper's zxid and sequential znodes, etcd's revision, Kafka's leader epoch and HDFS's QJM epoch numbers are all the real version of LockServer.token.

The resource is one variable. A real storage service enforcing fencing needs the check on every write path, needs the token durably stored beside the data, and needs to decide what happens to writes already in flight through a proxy, a cache or a batch. "The resource must check the token" is one line here and a design programme there — which is exactly why so many systems ship the lock and skip the fencing.

9. Check yourself

Every answer is derivable from dlock.py and the transcripts above, and every one was verified by running it.

1. At t=16, when A's write corrupts the resource, which client held the lock according to the lock service — and what does the answer imply about fixes that live in the lock?

2. overlapping_grants returns [] for every run in this page, including the corrupted one. What exactly is it asserting, and why is the half-open interval load-bearing?

3. Sweep 2 shows ttl=1 is exactly as corrupt as ttl=10. Why doesn't shortening the lease change anything at all?

4. A colleague proposes: before writing, re-read the lease from the lock service and abort if it has expired. Under what precise condition does this work, and why can't the client arrange that condition?

5. Fencing turns the corrupted run's final value from 'A' into 'B' — not into 'AB'. Is that a bug in the fix?

6. You run this design with 5 Redis nodes, and someone points out that a Redis node restarting from an empty state could hand out a lease that is already held. Fix that — say, by enabling fsync on every write, or switching to a consensus-backed lock service. Does the failure in §6.1 go away?

7. Reach past the toy: you have a batch job that takes a distributed lock and then writes to S3. S3 has no fencing-token API. What can you actually do?

10. Further reading

• How to do distributed locking — Martin Kleppmann, 2016. The source of this toy's argument, and the origin of the fencing-token diagram §4 is a redrawing of. Read it for the efficiency-versus-correctness distinction in §9's last answer, which is the part most people miss.
• Is Redlock safe? — antirez's reply, the same week. Worth reading immediately after, and not only for balance: the disagreement is partly about what a lock is for, and seeing two competent people talk past each other on that point is more instructive than either argument alone.
• Distributed locks with Redis — the Redlock algorithm as specified, including the clock-drift arithmetic this toy deliberately omits (§7.5) and a section acknowledging the critique.
• The Chubby lock service — Burrows, OSDI 2006. Section 2.4 is about sequencers, which is fencing under another name, and the paper is unusually candid about clients misusing locks. The "it is a lock service, but people use it as a name service" material is a bonus.
• ZooKeeper: wait-free coordination — the paper. zxid is the real version of LockServer.token: monotonic because it comes from a single ordered log, which is the property §5.2 says a quorum of independent counters does not have.
• ZooKeeper recipes: locks — the canonical sequential-znode lock recipe, and its own explicit warning that a client can lose the lock without noticing.
• KIP-320: allow fetchers to detect and handle log truncation — Kafka's leader epoch, which is a fencing token at production scale. Good for seeing what §8's "the check is one line here and a design programme there" means concretely.
• HDFS HA with the Quorum Journal Manager — epoch numbers rejecting writes from a superseded NameNode. The clearest production example of the resource, not the lock, doing the rejecting.
• Jepsen: redis-raft — what it looks like when someone tests these properties adversarially against a real system rather than a 253-line simulation.