分布式系统 00：论断—证据—核验状态
核验日期：2026-09-19。本文件为本篇资料索引的唯一维护位置。
CROSS_CHECKED_PRIMARY = 两个独立原始/官方来源交叉核验；MODEL_LOCAL = 本地教学模型；DOC_ONLY = 文档而非实测。

C01 课程范围不限于共识/协调产品。
MIT 6.5840 Schedule: Spring 2026，网页标 tentative。
https://pdos.csail.mit.edu/6.824/schedule.html
Stanford CS244B Schedule: Spring 2024。
https://www.scs.stanford.edu/24sp-cs244b/sched/
状态：CROSS_CHECKED_PRIMARY；只据此安排教学结构，不声称本系列等价课程或学分。

C02 未收到回复不能区分未执行与执行后回复丢失。
MIT 6.5840 2026 Lecture 2: Threads and RPC，RPC problem / failure 段。
https://pdos.csail.mit.edu/6.824/notes/l-rpc.txt
gRPC Status Codes，更新 2024-08-21，DEADLINE_EXCEEDED 条。
https://grpc.io/docs/guides/status-codes/
状态：CROSS_CHECKED_PRIMARY；另有 MODEL_LOCAL 的两条不可区分轨迹。

C03 纯异步模型不能单凭有限等待区分停止与慢速。
Fischer/Lynch/Paterson, Impossibility of Distributed Consensus with One Faulty Process, JACM 32(2), April 1985, pp.374–382，重点 p375–376。
https://www.scs.stanford.edu/24sp-cs244b/sched/readings/flp.pdf
Dwork/Lynch/Stockmeyer, Consensus in the Presence of Partial Synchrony, JACM 35(2), April 1988, pp.288–323，Introduction 的两种部分同步定义。
https://groups.csail.mit.edu/tds/papers/Lynch/jacm88.pdf
状态：CROSS_CHECKED_PRIMARY；FLP 来自子代理原文核验，主代理重开遇 web Internal Error；DLS 主代理已打开原文。未把本文丢包模型称为 FLP 模型，未展开 FLP 证明。

C04 安全性不蕴含活性；有限安全反例不等于活性证明。
Alpern/Schneider, Defining Liveness, Information Processing Letters 21, 1985-10-07, pp.181–185（修订 1985-02-20），§2–3。
https://www.cs.cornell.edu/fbs/publications/DefLiveness.pdf
Leslie Lamport, PlusCal Tutorial Session 9: Liveness，更新 2024-08-19，§1。
https://lamport.azurewebsites.net/tla/tutorial/session9.html
状态：CROSS_CHECKED_PRIMARY。正文使用等待而不成功的模型反例；不借超时观测断言无限运行不终止。

C05 持久性需要指定故障边界，write/close/进程重启不等于断电证明。
fsync(2), Linux man-pages 6.19, 2026-02-08，DESCRIPTION/ERRORS。
https://man7.org/linux/man-pages/man2/fsync.2.html
Atomic Commit In SQLite，滚动文档，访问 2026-09-19，Hardware Assumptions。
https://www.sqlite.org/atomiccommit.html
Rebello et al., Can Applications Recover from fsync Failures?, USENIX ATC 2020，官方论文摘要。
https://www.usenix.org/conference/atc20/presentation/rebello
状态：DOC_ONLY + 反例文献交叉核验。未运行 SQLite、Linux 文件系统或断电实验；不将历史测量外推为当前所有文件系统行为。

C06 线性一致的完成操作可置于调用/响应间，并保留不重叠操作的实时顺序。
Herlihy/Wing, Linearizability: A Correctness Condition for Concurrent Objects, ACM TOPLAS 12(3), July 1990, pp.463–492，§1–2。
https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf
MIT 6.5840 2026 Lecture 8: Consistency and Linearizability。
https://pdos.csail.mit.edu/6.824/notes/l-linearizability.txt
状态：原论文已核验；课程讲义作为独立核验入口（见后续核验补记）。本篇只手算成功写后隔离副本旧读的反例，没有历史检查器。

C07 并发先修参考：A Tour of Go，Goroutines，滚动页面，访问 2026-09-19。
https://go.dev/tour/concurrency/1
状态：官方学习入口；正文纸笔 lost-update 示例独立设计。

C08 同步后确认在本文有限模型中不丢已确认值。
本仓 examples/distributed-systems/model00/main.go；固定一次 Put、A 最多一次恢复、稳定状态不损坏、B/C 无复制消息。
状态：MODEL_LOCAL；不变量推导见正文，本地枚举 10 个环境组合见 verification.txt。
非覆盖项：迟到执行、消息重排/重复、并发写、磁盘撕裂、真实进程重启、Raft、ZooKeeper、etcd。

反向检索与修订记录
- gRPC 官方页面末尾的 2024-08-21 修订专门涉及 DEADLINE_EXCEEDED 描述，已对照现行文字。
- 搜索 fsync failures / crash consistency，找到 ATC20 和 OSDI18 原始研究；正文采用 ATC20 官方摘要的有界结论。
- 查安全性/活性原论文的 revised 日期和 Lamport 停滞反例，避免把“按时完成”混作纯最终性。
- 没有据此声称“没有勘误”；本次检索范围未发现推翻 C02–C04 的原作者修订。

写作流程
blog-editor → anti-ai-tone（tech profile；逐段支撑/推进/节奏/连续性复核）→ anti-persona-fabrication（第一人称/体感/身份/说书腔扫描与连读），均在正文落盘前完成。
脚本：0 error，1 warning；warning 来自 post_link 的文件名中多个“的”，链接标签正常，人工保留。
只读独立审阅对照了模型与正文；补充 sync-missing 重启后无法单凭等待恢复请求的边界。

C06 核验补记：主代理已打开 MIT l-linearizability.txt，核对 definition 段（94–98 行）及实时顺序例子，与 Herlihy/Wing §2 一致。更新为 CROSS_CHECKED_PRIMARY。