Replace unverifiable facts with verifiable ones

Why does coordination define checkable substitutes instead of observing liveness or ownership?

CaseConstructed case · Ingrid at Tixora

12 seats sold twice, and the lock worked

The 12 seats sold twice last month have a clear story in the logs. A leader of partition 17 froze for 15 seconds. The lock service had given that leader a lock with a TTL of 10 seconds. The TTL ran out, the lock service granted the lock to a new leader, and the new leader started accepting purchases. Then the old leader woke up, still believed it held the lock, and accepted 12 purchases for seats the new leader had already sold. The lock service did exactly what it was designed to do.

Two weeks later, the team grew the 3-node metadata cluster to 5 nodes in a single step. For a few seconds the cluster briefly had two leaders, although there was no network failure. And Carmen now asks for "two data centres with automatic failover, so we survive losing one building". Ingrid suspects each of these has a root in the same place.

How it ends →

Distribution of data moved bytes. This article moves nothing. Everything here is a few dozen bytes of metadata, and yet it is where the difficulty of this mechanism lives. The facts these bytes assert are facts no machine can check.

The constraint: the properties coordination needs are unobservable:

Is that node alive?
Does it still hold the lock?
Are we all at the same point?
Is this the current configuration?

Not expensive, not approximate, but unobservable in principle. The only evidence available is the arrival or non-arrival of a message, and non-arrival is consistent with both death and delay (FLP is the formal statement).

So the mechanisms in this article do something more radical than approximating. They stop trying to observe the property. They define a new property that is observable, and legislate that the new one is what counts.

A node is not "alive". It is the holder of a lease that has not expired by the issuer's reckoning.
A node is not "the leader". It is the recipient of votes from a majority in term 7.
The system is not "in a consistent global state". It holds a cut that no participant can distinguish from one.

Every safety argument in this article is therefore an argument about a set of messages someone holds, not about the world. That is exactly why quorum intersection works under arbitrary delay while everything built on timeouts does not.

This is why safety and liveness need different tools: in a correct protocol no timeout value can produce two leaders, only zero. When you find a timing assumption sitting inside a safety argument, you have found a lease, and a lease always needs a fence behind it.

Coordination is the replacement of unverifiable facts about the world with verifiable facts about a set of messages, after which safety is a bookkeeping property and only liveness still depends on the network.