Paxos Guarantees Liveness Only Under Partial Synchrony — Epoche C2
Two properties, two different fates Paxos, Lamport's protocol for getting a set of replicas to agree on a single value in the presence of crashes, has two guarantees that behave quite differently under weak timing assumptions: agreement holds no matter how badly the network misbehaves, while termination does not hold at all in a network with no timing assumptions whatever. Practitioners routinely collapse these into a single claim that "Paxos is correct in an asynchronous system", and the collapse is not harmless — it produces systems whose designers have no account of why their cluster stops making progress, and no way to reason about what would restore it. Three terms are needed before the argument can be stated, and they are terms of art rather than ordinary English. A protocol satisfies agreement (the safety property here) if no two processes ever decide different values. It satisfies termination (the liveness property) if the deciding eventually happens. And a system is asynchronous if there is no bound whatever on message delay or on the relative speeds at which processes take steps — messages are eventually delivered, but no finite time can be named by which delivery must have occurred. The claim to be defended is that Paxos's agreement is unconditional on timing while its termination is conditional, and the conditional part is what the essay's title flags. What the FLP theorem actually forbids The result standing behind all of this is due to Fischer, Lynch and Paterson (1985), and it is worth stating with the hypotheses its authors actually gave it, because the version in circulation is stronger than the theorem and weaker in the wrong places. The model: finitely many deterministic processes communicating by messages through a reliable but wholly asynchronous message system, which may delay and reorder arbitrarily but does not lose or duplicate. A process takes a step by receiving one message (possibly the null message) and, on the basis of its state and that message, changing state and sending finitely many messages. At most one process may fail, and failure means crashing — halting permanently, with no wrong behaviour. A run is admissible if at most one process crashes and every message sent to a non-crashed process is eventually received. The correctness conditions are not the familiar textbook triple. Fischer, Lynch and Paterson call a protocol partially correct if (i) no reachable configuration has processes holding two different decision values, and (ii) for each of the two possible decision values, some reachable configuration has that value — the second condition is non-triviality , and it is markedly weaker than validity, which would require the decision to be some process's input. Non-triviality is all the proof needs, and using it makes the impossibility stronger, since it rules out even protocols that are permitted to decide arbitrarily. A protocol is totally correct in spite of one fault if it is partially correct and, in every admissible run, some process eventually decides. Again the weaker demand strengthens the theorem: not all correct processes, just one. The theorem is that no such protocol exists. The proof runs in two lemmas, and both are worth having because they show exactly where the difficulty lives. Call a configuration bivalent if both decision values are still reachable from it, and univalent otherwise. The first lemma is that some initial configuration is bivalent. Suppose not. The initial configurations of $n$ processes with binary inputs form the cube $\{0,1\}^n$; non-triviality guarantees at least one is 0-valent and at least one is 1-valent; so somewhere along a path of single-bit flips there are adjacent configurations $C_0$ and $C_1$, 0-valent and 1-valent respectively, differing only in the input of one process $p$. Now take an admissible run from $C_0$ in which $p$ never takes a step — legitimate, since $p$ is allowed to be the one crashed process. That run decides $0$. The identical schedule applied to $C_1$ is indistinguishable to every process other than $p$, so it also decides $0$, contradicting the 1-valence of $C_1$. The second lemma is that bivalence can be maintained while delivering any particular pending message. Given a bivalent configuration $C$ and a message $m$ in transit to process $p$, there is a finite schedule not containing the delivery of $m$ after which delivering $m$ leaves the configuration bivalent. The argument turns on the commutativity of steps taken at disjoint processes, together with the same one-crash indistinguishability move used above. Granted these two lemmas, an adversary constructs an infinite run by repeatedly taking the oldest undelivered message, applying the lemma, and delivering it. Every message is eventually delivered, so the run is admissible; every configuration in it is bivalent, so no process ever decides. Three features of that run correct the way the theorem is usually paraphrased. First, no process actually crashes in it. The one-fault allowance is used only to license the indistinguishability arguments; the adversary never needs to spend it. Second — and this is the point that matters for Paxos — agreement is not violated anywhere in the run. It cannot be, because nothing is ever decided. FLP does not show that safety and liveness fail together in asynchronous systems. It shows that termination fails, in a run where safety is trivially intact. Third, and easily lost: the processes are assumed deterministic. Ben-Or (1983) showed that asynchronous agreement is achievable with probability $1$ if processes may flip local coins, tolerating crash failures of fewer than half the processes; his protocol has no bound on the number of rounds, so it does not contradict FLP, which forbids a bound of any kind on every run. Why Paxos keeps agreement without any timing assumption Now to Paxos itself, described in Lamport's "The Part-Time Parliament" (1998) and restated without the Greek archaeology in "Paxo