A server has not answered. It may have crashed, or its reply may arrive just after the next timeout. In a fully asynchronous model, there is no known delay bound that settles the question.
This uncertainty is the intuition behind FLP. The proof makes a stronger, precise statement: no deterministic consensus protocol can guarantee agreement, non-trivial decisions, and termination in every permitted asynchronous execution when even one process may crash.
It does not say that agreement is never reached. It says that any proposed protocol has a legal execution in which no decision is reached. If you need a refresher on the positive result under synchronous timing assumptions, start with consensus and Paxos.
1. Keep the assumptions visible
| Assumption | What it allows or requires |
|---|---|
| Deterministic processes | The same local state and received message produce the same next action |
| Asynchrony | No known upper bound on communication or process speed |
| Reliable communication | Messages to non-faulty processes eventually arrive; delay is unbounded, not permanent loss |
| At most one crash-stop failure | A process may stop taking steps; no malicious behavior is needed |
| Non-trivial decisions | Both 0 and 1 must be possible outcomes across different initial inputs |
| Irrevocable agreement | A decision cannot be changed, and decisions cannot conflict |
A protocol must tolerate the possibility of a crash; the problematic execution need not actually contain one. No network partition, corrupted packet, or malicious replica is required.
Why a timeout does not settle the model
| What A observes | Possible explanation |
|---|---|
| No reply from B by time T | B crashed |
| No reply from B by time T | B is alive, but has not been scheduled yet |
| No reply from B by time T | B sent its reply, but it is still in transit |
For any finite T, all three are possible. A timeout can trigger a new attempt. It does not turn uncertainty into proof that B is dead. This observation motivates the proof, but is not by itself the whole proof: a clever algorithm might avoid waiting for B. FLP must rule out every deterministic algorithm, including those that try to do exactly that.
2. The proof studies configurations, not individual votes
A configuration contains every process’s local state and all messages in transit. An event e = (p, m) delivers message m to process p, performs its deterministic local computation, and adds any resulting outgoing messages to the network. A no-message step is also possible. A schedule is a sequence of these events.
For a configuration C, consider every decision reachable by a valid continuation:
- 0-valent: only a 0 decision is reachable.
- 1-valent: only a 1 decision is reachable.
- Bivalent: one continuation can decide 0 and another can decide 1.
flowchart TD
C["Bivalent C: no decision fixed yet"] -->|"Schedule S0"| Z["0-valent: only 0 remains possible"]
C -->|"Schedule S1"| O["1-valent: only 1 remains possible"]
Z --> D0["Decide 0"]
O --> D1["Decide 1"]This picture describes possible executions, not two outcomes of the same execution. Bivalence does not mean half the processes voted each way. It describes which future decisions are still possible from the entire global state.
A process can still be locally undecided in a univalent configuration. Conversely, once any irrevocable decision occurs, agreement makes the configuration univalent: the other result is no longer legal.
3. There must be a bivalent starting point
Assume, for contradiction, that every initial configuration is univalent. With three input bits, connect all-0 to all-1 by changing one process’s input at a time:
000 -- change A --> 100 -- change B --> 110 -- change C --> 111These arrows compare different initial inputs; they are not execution steps. With the usual validity condition, 000 must lead to 0 and 111 to 1. Along this chain there must be an adjacent pair labeled 0-valent and 1-valent. The general proof only needs non-triviality and connectivity of the input configurations.
The adjacent pair differs only in one process p’s input. Let p crash before taking a step. Everyone else has identical state in the two cases and sees identical messages under the same schedule. Because the algorithm promises termination despite one crash, the others must eventually decide. Because it is deterministic, they must decide the same value in both cases.
That contradicts the claim that one initial configuration permits only 0 and the other only 1. Therefore at least one initial configuration is bivalent. The two global states are not literally identical: p’s state differs, but no active process can observe that difference.
4. A pending event can be delivered without forcing a decision
The next lemma does more than say “keep postponing an inconvenient message.” Starting from a bivalent C and any applicable event e, there is a finite sequence of other events followed by e that ends in another bivalent configuration.
To see the proof structure, temporarily defer e. Let S contain the configurations reachable without e; apply e to each of them to obtain a set D. Suppose every configuration in D were univalent. Because C is bivalent, D contains both a 0-valent result and a 1-valent result. Along the paths in S, find neighboring configurations C0 and C1, separated by one event e′, whose e-results have different valences.
There are two cases.
Case A: e and e′ run at different processes
If both events are already applicable, and their receiving processes differ, they commute: doing e then e′ produces the same configuration as doing e′ then e. Neither event depends on a message created by the other.
flowchart TD
C0["C0"] -->|"e at p"| D0["D0: assumed 0-valent"]
C0 -->|"e-prime at q"| C1["C1"]
D0 -->|"e-prime at q"| D1["D1: assumed 1-valent"]
C1 -->|"e at p"| D1The left path reaches D1 from D0. But a 0-valent configuration cannot have a 1-valent descendant. That is the contradiction.
Case B: both events run at the same process p
We cannot swap two actions at p. Instead, consider a finite schedule s in which the other processes reach a decision while p takes no steps. Such a schedule must exist under the assumed guarantee of termination despite one crash.
Because s does not run p, it can be moved before or after e, and before or after the pair e′ then e. Moving it past the two branches makes the decided state s(C0) lead to both a 0-valent and a 1-valent state. That would make an already decided configuration bivalent, contradicting irrevocable agreement.
Both cases fail, so D must contain a bivalent configuration. We can deliver the chosen pending event after a finite detour and still keep both outcomes possible. This is the central step of the proof outline; it uses the hypothetical algorithm’s own termination guarantee to derive the contradiction.
5. The infinite execution must still be fair
An execution that simply hides one message forever from a healthy process would violate reliable delivery. FLP does not need that shortcut.
Rotate through processes. For the current process, select its oldest pending message, or a no-message step if its queue is empty. The lemma supplies a finite detour ending with that event while preserving bivalence. Repeat. Every process keeps taking steps, and every message is eventually delivered, yet no stage reaches a decision. These fairness conditions are explicit in the original FLP paper, sections 2–3.
flowchart LR
B0["Bivalent C0"] -->|"Finite detour; deliver e1"| B1["Bivalent C1"]
B1 -->|"Finite detour; deliver e2"| B2["Bivalent C2"]
B2 -->|"Continue fairly"| More["Always undecided"]No single message needs an infinite delay. The schedule repeatedly arranges finite delays so that the next completed stage still leaves both decisions possible. This separates eventual delivery of each message from eventual completion of the whole protocol.
That is the contradiction: we assumed every admissible execution eventually decides, then constructed an admissible execution that never does.
6. What this changes in engineering
| Approach | What changes relative to the theorem |
|---|---|
| Partial synchrony | Progress relies on timing eventually becoming sufficiently well behaved |
| Eventual leader or failure-detector assumptions | Adds useful information or eventual stability beyond pure asynchrony |
| Randomized consensus | Changes determinism; appropriate protocols can provide probabilistic termination under stated scheduler assumptions |
| Preserve safety and wait | Accepts that some executions make no progress |
Paxos protects its decision through promises and quorum evidence. Stable leadership and successful communication allow progress. The theorem is not contradicted by thousands of successful runs, nor does a successful test prove termination for every schedule.
A useful design question is therefore: Which assumptions make this system progress, and what does it do when those assumptions stop holding? Retrying, selecting another leader, or refusing a write can be sensible choices, provided they preserve the safety rule.
Check your understanding
- Does FLP require permanent packet loss? No. The nonterminating execution can still deliver every message.
- Does bivalent mean nobody has proposed a value? No. Values may have been exchanged extensively; both final outcomes remain reachable.
- Must an actual crash happen in the nonterminating execution? No. The protocol’s obligation to tolerate one possible crash is enough for the proof.
- Does a longer timeout defeat FLP? No finite timeout establishes a known delay bound in the fully asynchronous model.
- Does FLP imply Paxos is unsafe? No. The missing universal guarantee is termination, not the safety of its decision rule.
Reading basis
This article develops the supplied 3.4 The FLP Proof slides and transcript from Cloud Computing Concepts, Part 1. The diagrams and small examples are redrawn explanations. The reliable-delivery and admissible-run conditions are checked against Fischer, Lynch, and Paterson’s Impossibility of Distributed Consensus with One Faulty Process (JACM, 1985), linked above. This is a proof walkthrough, not a replacement for the full formal paper.