跳转到内容
Jason's Study

FLP 1985 — 一个坏节点就能让异步共识永不终止

是什么

FLP（Fischer-Lynch-Paterson）是一个不可能性定理：在”完全异步 + 至少允许 1 个节点崩溃”的系统里，没有任何确定性算法能保证所有活着的进程在有限步内对一个 bit 达成共识。

日常类比：三个朋友约在山洞会合，每人独立决定去 A 山还是 B 山。规则要求他们必须全去同一座；没有共同手表；不能掷硬币；可能有人路上摔晕了不再动。FLP 说——没有任何沟通规则能保证他们一定能定下来。总存在一种倒霉的消息顺序，让他们永远在”还可能 A、还可能 B”之间徘徊。

注意 FLP 没说共识不可能——它说”确定终止”不可能。共识有三个性质：

  • 协定（agreement）：所有人最后选同一个值
  • 有效（validity）：选的值得是某人提议过的
  • 终止（termination）：所有正确进程在有限步内决定

FLP 牺牲的是第三条。前两条仍然可以保证。

为什么重要

不理解 FLP，下面这些事都没法解释：

  • 为什么 Paxos / Raft 都得加超时（timeout）——超时本质是偷偷换掉了”完全异步”假设
  • 为什么 比特币、以太坊用”概率终止”——区块需要 6 个 / 64 个确认才”基本敲定”，不是数学终止
  • 为什么 PBFT 论文要专门假设”partial synchrony”——这是 Dwork-Lynch-Stockmeyer 1988 为绕开 FLP 造的模型
  • 为什么 Ben-Or 1983 给共识加随机数——随机化是 FLP 的另一条逃生路：放弃”确定性”换回”终止”

FLP 是过去 40 年所有共识协议设计的底线。每一个新协议本质都在回答：“我牺牲了 FLP 三性质里的哪一条，换来了什么？“

核心要点

证明的核心思想可以拆成三步：

  1. 二价配置（bivalent configuration）：系统当前状态如果”还可能定下 0、也还可能定下 1”，叫二价。论文先证明初始一定有个二价配置存在——只要不同进程的初始提议不全相同。

  2. 关键步骤（critical step）：任何二价配置走一步消息后，可能变成”必然定 0”（0-价）或”必然定 1”（1-价）。这一步叫关键步骤。

  3. 永远能避开关键步骤：论文构造性地证明——永远能找到一种 schedule（消息送达顺序），让系统从一个二价配置走到另一个二价配置。也就是说，可以一直拖着不让它”塌缩”。

把这三步串起来：从初始二价开始，每次都能选一条 schedule 让它停留在二价——所以系统永远不会终止。

证明用了一个关键技巧：让一条消息”无限延迟”。完全异步意味着消息延迟没有上界，所以这种 schedule 在模型里合法。

简化版直觉：假设系统已经在二价配置里。要么”接收 A 进程的消息”会让它塌缩成 0-价，那就先送 B 的消息；要么 B 的消息会塌缩成 1-价，那就先送 A 的；要么两条消息无论先后顺序结果都不一样——这种情况论文证明可以让一个进程”看起来”已经崩溃（消息延迟到无穷远），让幸存进程只能靠剩下信息走，永远停在二价。

这就是”对手视角”——证明者扮演网络调度器，永远比协议算法多想一步。

实践案例

案例 1：为什么 Paxos 也可能不终止

paxos 在异步下严格遵守 FLP——它确实可能不终止：两个 proposer 反复抢 leader，每次刚拿到多数承诺就被对方更高的提案号打断，理论上能一直循环。

实际工程不爆炸是因为：

  • 用了 randomized backoff（重试前等随机时间）→ 暗中引入随机化
  • 网络通常是 partial-synchronous（多数时候有上界）→ 暗中加强了模型

FLP 没被违反，是被绕开了。

案例 2：Raft 怎么处理 FLP

raft 把超时（election timeout）放在显眼位置——leader 不发心跳超过 150-300ms 就触发选举。这等于显式声明”我假设网络不是完全异步”。

如果真的网络异步无界（比如分区持续打转），Raft 同样可能反复换 leader 不终止。Raft 的工程优雅在于把不终止的概率压到极小，不在于绕过 FLP。

案例 3：区块链的概率终止

比特币没用传统共识协议——它用 Nakamoto 共识：最长链规则 + PoW。这绕开 FLP 的方式是：

  • 放弃”确定终止”：一个区块上链后，并不是”立刻定下来”，而是”被覆盖的概率随后续块数指数下降”
  • 6 个确认后被回滚的概率小于 0.1%——这是统计意义的终止，不是 FLP 意义的终止

所以你听到”区块链解决了拜占庭将军问题”这种说法时——它解决了，但代价是把 FLP 三性质里的”终止”换成了”概率终止”。

踩过的坑

  1. 把 FLP 和拜占庭混为一谈：FLP 假设节点只会干净崩溃（fail-stop），不会作恶。拜占庭容错（BFT）是更强的故障模型，FLP 在 fail-stop 下就已经不可能，BFT 自然继承。

  2. 以为加节点能解决：FLP 对任何 N ≥ 2 都成立。加到 1000 个节点也一样不可能。增加的是”容错数量上限”，不是”绕开 FLP”。

  3. 以为同步系统也不行：完全同步下（消息延迟有上界）共识可以确定终止，比如 Lamport 1978 的同步多数派算法。FLP 的关键词是异步。

  4. 以为 FLP 是”证明数学不可能”：FLP 是构造性证明——它教你怎么构造一条让任何协议卡住的 schedule。这种”对手有无限耐心”的视角是分布式系统证明的标准武器。

  5. 以为超时违反 FLP：超时本质是把”异步”偷偷改成了”同步”或”partial synchrony”。FLP 没被违反，假设被改了。

  6. 混淆”安全性”和”活性”：FLP 牺牲的是活性（liveness——好事终将发生），保留的是安全性（safety——坏事永不发生）。Paxos 在异步下也是这种状态：永远不会出错（safety），但可能永远不收敛（liveness）。

适用 vs 不适用场景

这个不可能性影响的场景：

  • 任何”必须确定终止 + 完全异步 + 容错”的协议设计——做不到，必须放弃一个
  • 设计 fail-stop 模型下的共识——FLP 已是底线
  • 跨地域、跨数据中心的强一致系统——网络更接近异步，FLP 更逼近

可以绕开的场景：

  • 接受随机化 → Ben-Or 1983 风格（期望终止，不保证）
  • 接受 partial synchrony → Paxos / Raft / PBFT
  • 接受概率终止 → Nakamoto 共识、PoS finality gadgets
  • 同步系统 → Lamport 1978 多数派
  • 不需要容错 → 单一 leader 就够

历史小故事（可跳过）

  • 1980 年：Pease-Shostak-Lamport 证明了拜占庭将军在同步下需要 3f+1 节点。共识研究开始热起来。
  • 1983 年：Fischer、Lynch、Paterson 三人在 PODC 提出”异步下确定共识不可能”的初步结果。Ben-Or 同年用随机化算法绕开。
  • 1985 年：JACM 正式发表 FLP 论文，只有 9 页。证明用”二价配置 + 永远存在保持二价的 schedule”两个引理串起来，干净到惊人。
  • 1988 年：Dwork-Lynch-Stockmeyer 引入 partial synchrony 模型，给后来 Paxos / PBFT 全部铺好理论地基。
  • 1998 年：paxos 论文（Lamport）面世，假设 partial synchrony 处理活性，把 FLP 当成默认背景。
  • 2014 年：raft 把同样思路工程化，让一代后端工程师能读懂共识。

之后所有共识协议本质都在 FLP 三性质里挑选放弃哪一条。

学到什么

  1. 不可能性定理是设计的尺子——它告诉你哪条路是死胡同，省下你撞墙的时间。FLP 之前，有人真在尝试设计”异步确定容错共识”。
  2. 三性质必丢一：协定 / 有效 / 终止 三选二。每个共识协议都在这个三角里选位置。
  3. 超时是隐藏的同步假设——你写 setTimeout(election, 200ms) 的那一刻，就已经把模型从异步偷换成了 partial sync。
  4. 构造性证明的力量：不是”我没找到算法”，是”对任何算法我都能给你画出一条让它卡住的 schedule”。这种”对手视角”在分布式证明里是基本功。
  5. 安全性 ≠ 活性：Paxos / Raft 的所有论文都把这两个性质拆开讨论是有原因的——FLP 教会了整个领域必须分别证明。
  6. 理论先于工程 13 年：1985 论文，1998 年 Paxos 才工业落地。理论研究的”提前量”在分布式系统里特别明显。

延伸阅读

关联

  • paxos —— 异步下也可能不终止，工程上靠 randomized backoff + partial synchrony 压低概率
  • raft —— 用显式 election timeout 直接声明”我不打算和完全异步死磕”
  • paxos-simple-2001 —— Paxos 教学版，对 FLP 的处理藏在”phase 2 一直收不到响应”的描述里
  • fast-paxos-2006 —— 通过乐观路径减少消息轮数，但 FLP 仍是天花板
  • lamport-tla-1994 —— TLA+ 让你能形式化地写”在某种活性假设下系统会终止”
  • chandy-lamport-1985 —— 同年异步分布式快照算法，反向证明”有些事异步下能做”
  • lamport-1978 —— 同步多数派共识可终止，FLP 关键词是”异步”

反向链接

  • chandy-lamport-1985 —— Chandy-Lamport 1985 — 分布式系统不停机也能拍一张全家福
  • gilbert-lynch-2002 —— Gilbert-Lynch 2002 — 把 CAP 从口号写成数学定理
  • lamport-1978 —— Lamport 1978 — 分布式系统里没有”绝对的同时”
  • lamport-tla-1994 —— TLA — 把状态机和时序逻辑捏成一个公式
  • paxos —— Paxos — 分布式共识算法
  • paxos-simple-2001 —— Paxos Made Simple — Lamport 用平直英语把共识协议推导一遍
  • raft —— Raft — 易理解的共识算法