# 08 论断—证据—核验记录

核验日期：2026-09-19。正文与有限调度模型已落盘，本地执行见 verification.txt；此文件不是完整形式化证明。

## 资料登记

| 编号 | 原始资料与日期 | URL | 已核对位置与用途 |
|---|---|---|---|
| F | Michael J. Fischer, Nancy A. Lynch, Michael S. Paterson, *Impossibility of Distributed Consensus with One Faulty Process*, JACM 32(2), April 1985, pp. 374–382；初版会议为 PODS 1983 | https://groups.csail.mit.edu/tds/papers/Lynch/jacm85.pdf | §2 pp. 376–377 的协议与 admissible run；§3 pp. 378–380 的双价性与公平无限执行 |
| D | Cynthia Dwork, Nancy Lynch, Larry Stockmeyer, *Consensus in the Presence of Partial Synchrony*, JACM 35(2), April 1988, pp. 288–323；前期会议版为 PODC 1984 | https://groups.csail.mit.edu/tds/papers/Lynch/jacm88.pdf | 摘要 p. 288、§1.2 pp. 289–290：两种部分同步模型、安全性与终止的不同条件 |
| C | Tushar Deepak Chandra, Sam Toueg, *Unreliable Failure Detectors for Reliable Distributed Systems*, JACM 43(2), March 1996, pp. 225–267 | https://www.cs.cornell.edu/courses/cs734/2000FA/cached%20papers/ct96.pdf | §2.3 pp. 232–233 的检测器性质；§5 p. 239 的共识定义；§6.2 pp. 244–246 的多数正确条件及 uniform agreement |
| CB | Sam Toueg 作者维护的故障检测文献目录，动态页面，读取日期 2026-09-19 | https://www.cs.cornell.edu/info/people/sam/FDpapers.html | 区分 CT96 与 Chandra–Hadzilacos–Toueg 的最弱故障检测器论文 |
| A | James Aspnes, *Randomized Protocols for Asynchronous Consensus*；arXiv cs/0209014 v1 登记于 2002-09-06，当前返回 PDF 页首另印 May 28, 2018 | https://arxiv.org/pdf/cs/0209014 | §1–2、§4：nontriviality 与 validity 的差别；随机化与 adversary 模型、概率 1 终止 |
| M | MIT 6.5840 Spring 2026 schedule 与 Lecture 4 *Fault-Tolerant Agreement, Paxos*，读取日期 2026-09-19 | https://pdos.csail.mit.edu/6.824/schedule.html 和 https://pdos.csail.mit.edu/6.824/notes/l-paxos.txt | 课程结构与教学入口：无法区分崩溃和网络延迟、分裂决策、配置中多数派 |
| S | Stanford CS244b Spring 2024 schedule，读取日期 2026-09-19 | https://www.scs.stanford.edu/24sp-cs244b/sched/ | 开篇安排 FLP 阅读，后续涉及 ZooKeeper、Raft 等系统，作为课程顺序依据 |

访问边界：Stanford 的 FLP handout PDF 本次不可达，原文核验使用作者 MIT 机构镜像。曾尝试的 Cornell `/home/sam/FDpapers/CT96-JACM.pdf` 不可达，改用表中可读的 Cornell 课程缓存。Aspnes 的 arXiv 登记日期与当前 PDF 页首日期不同，应同时保留，不将其误报为 2018 年首次发表。

## 论断—证据—核验状态

| 论断 | 证据 | 状态与写作边界 |
|---|---|---|
| FLP 的确定性异步模型即使只要求容忍至多一个停止执行的进程，也不能保证每个 admissible 执行最终决定 | F §2 pp. 376–377、§3；A §1 | 已交叉核验。不是每次执行都失败，也不是恰好一个进程崩溃 |
| admissible 执行要求给非故障进程的每条消息最终收到 | F p. 377；§3 p. 380 的调度构造 | 已核验。不能永久扣留一条消息来冒充公平坏执行 |
| FLP 最终构造可以让每个进程无限步、所有消息最终交付而仍不决定 | F p. 380 | 已核验。坏执行可以零实际崩溃；协议必须容忍可能的崩溃参与了证明 |
| 原文 nontriviality 弱于现代“决定值来自某个提案”的 validity | F p. 377；A §1 | 已交叉核验。不得直接替换定义 |
| 部分同步有“界始终存在但未知”和“界已知但未知时刻后才成立”两种形式 | D 摘要、§1.2；A §2 | 已交叉核验。不能将 GST 视为算法可直接观察的事件 |
| 安全性与有效性不应依赖已越过 GST；活性才依赖所需稳定条件 | D p. 290 | 已核验。稳定后不能撤销稳定前已经发生的分叉 |
| 超时产生怀疑，不自动产生完美故障检测 | C §2.3；F 的异步不可区分背景；D 的额外时序前提 | 已综合核验。检测器抽象约束输出历史，不等于任意超时实现满足该约束 |
| CT 的 agreement 与 uniform agreement 量化对象不同 | C §5、§6.2 | 已核验。正文必须固定目标，不能混用“正确进程”和“所有已决定进程” |
| 随机化可要求概率 1 终止，但必须明确 adversary 与随机源模型 | A §2、§4 | 已核验。不是所有随机序列都终止，也不自动给出确定时间上界 |

## 定义与证明边界

### FLP

F §2 使用 N≥2 的确定性状态机；决定寄存器从未决定状态变为 0 或 1 后不可修改。部分正确性要求没有可达配置包含两个决定值，且 0、1 各能在某个可达配置被决定。这里的 nontriviality 不是“必须选择某个输入”的完整替代。

正确进程在执行中走无限步；否则属于故障进程。admissible 执行至多有一个故障进程，并满足给正确进程的消息最终被收到。协议即使只需让某个进程最终决定也受到结论约束，通常“所有正确进程最终决定”的要求更强。

证明从双价初态出发，用有限延伸保持双价性，再用轮转进程、优先处理较早消息的调度构造无限执行。故障容忍要求不意味着最终坏执行必须实际发生故障。

原文引言的 atomic broadcast 涉及一次本地动作向全部进程发送并保证对正确接收者的最终交付，不能直接理解为现代总序原子广播服务。

### DLS

部分同步模型中的通信延迟界 Δ、进程相对速度界 Φ 及其已知性需要分别说明。不能用“任何迟到者都被定义为故障”绕开模型。GST 后的稳定假设提供进展条件，不提供算法已经知道稳定期开始的保证。

论文讨论的部分同步通信、fail-stop/omission 场景有 n≥2t+1 条件；不得提升为跨同步性、认证方式和故障模型的普遍阈值。永久稳定是形式化模型；某些算法只需足够长的稳定阶段完成一次决定，具体长度与算法假设相关，不在本文实验中验证。

### CT

Strong completeness：最终，每个崩溃进程都被每个正确进程永久怀疑。

Strong accuracy：进程在崩溃之前不被怀疑；仅说“正确进程永不被怀疑”会漏掉后来崩溃进程在崩溃前的要求。

Weak accuracy：存在一个正确进程永不被怀疑。Eventual weak accuracy：存在某个时刻，此后至少一个正确进程不再被怀疑；其他正确进程仍可能无限次被误判。

P 结合 strong completeness 和 strong accuracy；◇P 结合 strong completeness 和 eventual strong accuracy；◇S 结合 strong completeness 和 eventual weak accuracy。CT §6.2 相关共识算法要求多数进程正确，不应省略。

CT §5 的 termination 要求所有正确进程最终决定；uniform integrity 要求每个进程至多决定一次；agreement 禁止两个正确进程决定不同值；uniform validity 要求任何决定值曾被某个进程提出。Uniform agreement 进一步禁止任何两个已决定进程取不同值，包括随后崩溃者；§6.2 实际证明这一更强性质。

Ω 与最弱检测器的精确归属需另读 Chandra、Hadzilacos、Toueg 的 JACM 43(4), July 1996, pp. 685–722 论文。本次仅用作者目录核对文献归属，不将其定理冒充 CT96 内容。

## 反向检索与交叉核验

本次用论文全名加 errata、correction 检索，并检索作者 MIT、Cornell 机构站点。未取得针对上述论断的作者勘误；这不等于证明没有勘误。检索中出现的课程幻灯片勘误不属于 FLP 原论文勘误。

版本采用最终 JACM 原文，不把 1983/1984/1991 前期会议版本与最终论文日期混用。Aspnes 对 nontriviality、部分同步两类模型的复述用于独立交叉核验；课程讲义用于课程组织，不代替原论文精确前提。

以下不是 FLP 的反例：无故障的一些执行能够结束；同步系统能够解决共识；满足指定模型的随机算法概率 1 终止。它们分别改变了量词、时序前提或终止标准。


独立交叉核验：父代理实际读取 FLP §2/§3、DLS p.290 和 CT §2.3/§6.2，与定义边界一致；父代理完整审读正文，确认有限模型结果不冒充 FLP 证明。