Gilbert-Lynch 2002 — 把 CAP 从口号写成数学定理

是什么

Gilbert-Lynch 2002 是一篇 9 页的形式化证明，把 Brewer 2000 PODC keynote 上的”CAP 三选二”猜想变成有数学证明的定理：在异步网络模型里，不存在任何算法能同时提供原子一致（C）+ 可用（A）+ 分区容忍（P）。

日常类比：Brewer 在台上说”三家分店共享一本账本，电话线断的时候只能在’账目一致’和’继续营业’之间挑一个”——这是工程师的经验之谈。Gilbert 和 Lynch 做的事，是用对手论证（adversary argument）证明：不管你设计多聪明的协议，只要网络真的能丢消息，某种倒霉顺序必然出现，让你两个目标无法同时达成。

为什么需要这篇？工程口号容易被滥用——CAP 在 2000-2002 年被很多人解释成”我们家系统是 CA”。Gilbert-Lynch 给出严格定义后，“CA 系统”这个说法暴露为自相矛盾：跨网络系统不可能不容忍分区。

这篇也是”定理论文”在分布式领域的一个写作范本：先精确定义三个属性、再构造执行序列、再走反证。整个过程不到 2 页就把核心讲完，剩下篇幅讨论部分同步模型（定理 2）和宽松一致性（如 t-eventual consistency）。

为什么重要

不理解这篇形式化，下面这些事都会停留在直觉层面：

• 为什么”P 不是可选项”是分布式存储的第一条铁律
• 为什么 Dynamo / Cassandra 一开口就承认”我是 AP”——它们读懂了定理的含义
• 为什么 Spanner 的设计需要 GPS + 原子钟那么复杂——它在拼命压缩”分区窗口”以接近 C+A
• 为什么”最终一致”不是耍赖，而是定理 2 留出的合法空间

核心要点

论文证了两个定理，第二个常被忽略但更指导工程：

1. 定理 1（异步模型）：在异步网络里，没有算法能同时提供 C+A+P。证明只用半页：把节点切成 G1、G2 两组，外部客户端先在 G1 写新值 v_new（A 要求必须成功），再在 G2 读（A 要求必须返回）；但 G2 与 G1 无任何消息往来，唯一能返回的是旧值 v_old——违反原子一致。矛盾。

2. 定理 2（部分同步模型）：哪怕每个节点都有本地时钟可量超时，分区期间仍然不能同时 C+A+P；但分区结束后系统可以恢复一致。这给”最终一致性”提供了形式背书——你不是放弃 C，是在分区窗口内暂停 C，分区结束再补。

证明的关键技巧叫对手论证：证明者扮演网络调度器，永远比协议多想一步。你说有响应？我让消息永远不送达。你说有超时兜底？我让超时之前消息正好到一半。算法跑不赢一个永远能调度的对手。

三个名词的精确定义（这是论文最重要的贡献之一，比 Brewer keynote 严格得多）：

• C = Atomic / Linearizable：每个读返回某次写完成后的最新值；所有操作存在一个全局线性顺序，且这个顺序与”现实先后”兼容
• A = Available：每个收到请求的非故障节点必须有限时间内返回响应——不能阻塞等共识、不能拒绝
• P = Partition Tolerance：网络可以丢失任意数量的节点间消息（不是某个节点崩了，是消息没送到）

注意 C 和 ACID 里那个 C 不一样：ACID 的 C 偏”完整性约束”（外键、唯一）；CAP 的 C 偏”外部可观察的强一致性”——同名不同义，是 CAP 讨论里最常见的混淆来源。

实践案例

案例 1：定理 1 的”两节点反证”

初始: 节点 G1 和 G2 都存 x = v_old
步骤 1: 网络断开（分区发生）
步骤 2: 客户端 c1 写 G1: x = v_new
        → 由 Availability，G1 必须返回成功
步骤 3: 客户端 c2 读 G2 的 x
        → 由 Availability，G2 必须有限时间内返回
        → G2 与 G1 没任何消息，只能返回 v_old
        → 但 v_new 已经"提交"过，违反 atomic
矛盾 → 三者不可同时拥有

这个反证短得像段子，但严谨——对手在 G1 写完后立刻让网络断到天荒地老。

案例 2：定理 2 让”最终一致”合法

分区期间: G1 / G2 各自接收写入，互不通信
         （C 暂时放弃，A 保留 = AP 模式）
分区结束: G1 G2 重连，比对版本，合并冲突
         → 例：用 vector clock 找因果，CRDT 合并
         → 最终所有节点收敛到同一份数据

Dynamo / Cassandra 走的就是这条路。Gilbert-Lynch 没批评这种设计，相反——定理 2 严格论证了它在分区结束后能恢复一致，是 BASE 哲学的形式背书。

定理 2 还隐含一个前提：分区会结束。如果网络分区永远不愈合，那两半永远各执一词、永远不一致——这是为什么所有 AP 系统都假设”分区是临时的”。在地理上彻底失联（卫星永远丢失）的极端场景里，这条假设也会破。

案例 3：Spanner 不是反例

很多人误以为 Spanner 推翻了 CAP——其实没有。Spanner 通过 GPS + 原子钟（TrueTime）把”网络分区”压缩到极小概率事件，分区真发生时仍然停服（少数派副本拒绝写）。它是把”不可能三角”里 P 那一面挤得很窄，不是消灭。

Google 自己在 Spanner 论文里诚实写：“we are not really CA, we are CP with very high availability”——分区时仍然牺牲 A，只是 P 的概率极小所以工程上感觉像 CA。这正是定理 1 的工程含义。

踩过的坑

1. 以为定理证伪了 CAP：恰恰相反，它把 Brewer 的工程口号升级成了能严格引用的定理。但前提模型（atomic + 必须有限响应 + 异步）很严格，比”实际系统”更苛刻。

2. 只看定理 1，忘了定理 2：定理 2 的”分区结束后能恢复”是最终一致性的合法依据。只引定理 1 容易给人”分布式没希望”的错觉。

3. 混淆 atomic 一致性和 ACID 的 C：论文里 C = linearizability（一种外部可观察的强一致），不是数据库 ACID 里那个偏完整性约束的 C。两个 C 含义不同，常见误用。

4. 把”必须有限时间响应”当生活常识：定理里的 Availability 是数学版——不能阻塞、不能装死。实际系统经常用”超时拒绝”绕开，这本质把 A 弱化了，所以”绕过 CAP”的报道大多在偷换定义。

5. 把 P 当成”网络要不要支持丢包”：P 不是 feature flag，它是事实判定——网络一定会丢消息，问题是你的算法在丢消息时如何表现。否定 P 等价于声称”我们家网络永远 100% 可靠”，跨地域系统里这是空头支票。

适用 vs 不适用场景

适用：

• 设计跨地域复制的存储系统，需要明确”分区窗口的行为”
• 评估某产品宣传”我又 C 又 A”时——大概率它把 P 假设走了
• 给团队解释”为什么我们选 AP 后还能恢复”——直接引定理 2
• 写 RFC 或设计文档时锁定术语——“我们这块在分区时是 CP”比”系统稳”清楚得多

不适用：

• 需要精细化 latency 权衡 → 用 Abadi 2010 PACELC（分区时 PC/PA，平时 EL/EC）
• 单机或单数据中心系统 → 没有分区可言
• 想用它论证某具体一致性模型（顺序一致 / 因果一致 / RYW）→ 太粗，需要更细的层级
• 想推导”具体超时值应该多大”→ 定理是定性的，不给数字
• 想证明某 NoSQL 比 SQL 更可用 → 这是误用，可用性是设计选择不是技术派别属性

历史小故事（可跳过）

• 2000-07：Brewer 在 PODC keynote 提 CAP 三角，幻灯片 24 页，无证明
• 2002 春：Gilbert（MIT 博士生）和 Lynch（FLP 1985 的 L）合作，9 页 SIGACT News 文章把猜想变定理
• 2007–2010：Dynamo / Cassandra / Riak / CouchDB 一波 AP 路线 NoSQL，全部以 CAP 为旗帜
• 2010：Abadi 提 PACELC，把 CAP 没覆盖的”平时延迟”补上
• 2012：Brewer 写 “CAP Twelve Years Later”，自我澄清”三选二”是简化口号
• 2015：Kleppmann 写 “Please stop calling databases CP or AP”，批评原模型对 C 和 A 都定义太严
• 2017 后：CRDT、因果一致、TLA+ 等更细粒度模型成为新的研究主线——CAP 退居为”入门第一课”

学到什么

1. 工程口号 → 形式定理 → 自我澄清：CAP 走完这三步用了 12 年，是健康的工程理论演化样本
2. 对手论证是不可能性证明的通用兵器：FLP / CAP / 分布式拜占庭下界都用同一招——你扮演网络，永远比算法多走一步
3. P 不是选项：跨网络系统里”CA”等于”假装无分区”。真实选择是 CP 还是 AP
4. 定理 2 比定理 1 重要：它告诉你分区结束后能恢复一致，给最终一致留出形式空间
5. 原模型很严：C=linearizability、A=有限时间必应——比大多数实际系统的需求都强，所以”绕过 CAP”的报道往往在弱化定义
6. 9 页能撑起一代 NoSQL：定理写得短，但严格定义本身就是产品决策的”裁判规则”——没有它，工程师吵不清”我家是不是真的 CA”

延伸阅读

• 论文 9 页 PDF：Gilbert-Lynch 2002（密度极高但读得动，半页就到核心反证）
• Brewer 自我澄清：CAP Twelve Years Later（2012 IEEE Computer）
• 反思：Martin Kleppmann — A Critique of the CAP Theorem（论证原模型对 C/A 定义太严）
• brewer-cap-2000 —— 这篇形式化的源头
• flp-1985 —— 姐妹不可能性定理，同样的对手论证

关联

• brewer-cap-2000 —— 上游：把口号变定理就是这篇做的事
• flp-1985 —— 异步 + 故障的不可能性鼻祖；Lynch 是共同作者
• dynamo —— AP 路线代表，定理 2 给它形式背书
• cassandra-2010 —— AP 路线，可调一致性
• spanner-2012 —— 用 TrueTime 压缩分区窗口，不是推翻定理
• bigtable-2006 —— CP 路线代表
• paxos-1998 —— CP 系统的共识引擎
• bayou-1995 —— 早期 AP + 冲突合并样本

反向链接

• bayou-1995 —— Bayou — 离线先改本地，再回来和别人合并
• bigtable-2006 —— Bigtable 2006 — Google 把行级随机读写做到 PB 级的存储系统
• brewer-cap-2000 —— Brewer CAP — 网络一断电，一致性和可用性只能留一个
• cassandra-2010 —— Cassandra 2010 — 把 Dynamo 的 P2P 骨架和 Bigtable 的列族数据模型拼成一个东西
• dynamo —— Dynamo — 让购物车永远能写入的分布式存储
• flp-1985 —— FLP 1985 — 一个坏节点就能让异步共识永不终止
• helland-2007 —— Life Beyond Distributed Transactions — 大规模系统下放弃跨机事务的宣言
• paxos-1998 —— Paxos 1998 — 古希腊议会寓言里藏的共识协议
• spanner-2012 —— Spanner 2012 — 用原子钟和 GPS 给全球数据库发时间戳