06 一致性模型与分区边界：论断—证据—核验状态
研究及访问日期：2026-09-19。原论文模型、教学检查器、本地观测分开记录；无产品API保证或性能结论。

[1] Herlihy/Wing, Linearizability: A Correctness Condition for Concurrent Objects, TOPLAS 12(3), 1990-07.
https://www.cs.cmu.edu/~wing/publications/HerlihyWing90.pdf
定位：§2.1–2.2，尤其印刷页469。
论断：调用/返回历史、合法顺序规格、实时序、扩展与complete。状态：原文阅读，关键定义独立交叉核验[2]；原版L2不能直接用于pending。

[2] Sela/Herlihy/Petrank, Linearizability: A Typo, arXiv2105.06737v2, 2021-07-29.
https://arxiv.org/abs/2105.06737
https://arxiv.org/pdf/2105.06737
定位：§3.1读到未来pending写反例；§4 Definition4.1修订；§6替代修法局限；§7线性化点。
论断：L2约束complete(H′)中的实时序，而非只约束原H中完整操作；pending可选择补全但不可解释其调用以前已经完成的读。状态：已读并与[1]对照；正文采用修订定义。实验明确拒绝pending，没有宣称实现此扩展。

[3] Lamport, How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs, IEEE TC, 1979-09, 690–691.
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/How-to-Make-a-Multiprocessor-Computer-That-Correctly-Executes-Multiprocess-Programs.pdf
定位：印刷页690定义段。
论断：存在共同顺序，保留各处理器程序序，不添加跨进程实时先后。状态：原文已读；客户端历史是本实验的显式建模，不声称原论文研究网络KV。

[4] Ahamad/Neiger/Burns/Kohli/Hutto, Causal memory: definitions, implementation, and programming, Distributed Computing 9, 1995, 37–49.
https://i2docker.moves.rwth-aachen.de/i2/fileadmin/user_upload/documents/Seminar_MCMM11/Causal_memory_1996.pdf
定位：§4，印刷页39–40。
论断：程序序与writes-into生成因果关系；每进程可有遵守因果的合法视图，并发写不必共同总序。状态：原论文已读；文件名1996与正文1995不一致，引用正文年份。重复数值的read-from歧义已注明。

[5] Gilbert/Lynch, Brewer’s Conjecture and the Feasibility of Consistent, Available, Partition-Tolerant Web Services, SIGACT News 33(2), 2002-06.
https://groups.csail.mit.edu/tds/papers/Gilbert/Brewer6.pdf
定位：§2.1–2.3；§3.1 Theorem1与Corollary1.1；§4.2。
论断：C=atomic/linearizable；A=每个非故障节点收到的请求最终完成，无统一时限；任意消息丢失下C与A不可兼得。状态：原文定义、不可区分执行及推论已读。关键A定义与[6]工程解释分开。
检索纠错：同目录Brewer2.pdf是后来的Perspectives on the CAP Theorem，不是2002原文。通过Lynch出版物目录找到Brewer6.pdf。

[6] Brewer, CAP Twelve Years Later: How the “Rules” Have Changed, IEEE Computer 45(2), 2012-02, 23–29; DOI10.1109/MC.2012.37.
https://www.infoq.com/articles/cap-twelve-years-later-how-the-rules-have-changed/
定位：Why 2 of3 is misleading、CAP-latency connection、partition recovery讨论。
论断：按操作/数据/分区阶段细化选择；超时下等待或继续是工程解释；恢复需处理冲突。状态：IEEE直链读取失败；使用明确注明InfoQ & IEEE Computer Society合作的全文转载，转载日期2012-05-30。未把它当2002定理的修订证明。

[7] Bailis/Ghodsi, Eventual Consistency Today: Limitations, Extensions, and Beyond, ACM Queue, 2013-03.
https://www.bailis.org/papers/eventual-queue2013.pdf
定位：开篇定义与安全性/活性讨论。
论断：无新增更新后的最终收敛不限制任意给定时刻读值；一次有限收敛观察不证明所有执行的活性。状态：作者托管原文已读；正文没有将最终一致写成有限history判定算法。

课程结构：MIT 6.5840 Spring2026 https://pdos.csail.mit.edu/6.824/schedule.html 与Stanford CS244B Spring2024 https://www.scs.stanford.edu/24sp-cs244b/sched/ 。仅用课程组织主题，不复制课程作业答案。
反向核验：主动检索linearizability typo/errata找到[2]；CAP误读对照[5]量词及[6]三选二解释；因果与最终模型对照[4][7]。未发现其他修订不代表不存在。
本地实验：五类历史由本文独立设计，独立顺序KV规格与DFS；证明仅限搜索算法和完整有限历史，具体运行见verification.txt。