先定义状态、操作与故障模型
库存只有一件，先说清什么算成功
两个用户同时购买最后一件商品。缓存返回扣减成功，数据库稍后落库，其中一个客户端超时。此时问“系统是否强一致”还太早：如果成功表示“订单已经获得库存”，两个成功就可能超卖；如果只表示“预约意图已受理”，稍后拒绝其中一个可以符合另一份契约。接口里的同一个 SUCCESS，必须先有确定的业务含义。
本页只建模一个 SKU、初始库存为 1、每次预订 1 件、不补货也不取消。抽象状态为 stock 和按请求身份保存的 results，操作为 reserve(request_id, sku, quantity) 与 readStock()。预订结果只有 RESERVED 和 INSUFFICIENT；传输超时记为 UNKNOWN，它表示客户端尚不知道结果，不是对象已经决定的第三种业务结果。
| 规则 | 这份模型里的具体约束 |
|---|---|
| 成功 | 新请求在库存为 1 时原子地把库存改成 0，保存 RESERVED，随后才能承诺成功 |
| 不足 | 库存为 0 时保存 INSUFFICIENT，不再扣库存 |
| 同身份重试 | 相同身份和参数返回原结果，不产生第二次扣减；同身份改变 SKU 或数量要报参数冲突 |
| 读取 | 返回某个合法状态里的库存，不能用负数表示排队人数 |
| 不变量 | stock ∈ {0,1}；成功请求数至多为 1；stock = 1 - 成功请求数 |
保存不足结果是本模型选择的接口语义。以后若加入补货，原请求仍返回原来的不足结果；用户要重新购买就创建新身份。也可以设计允许重新裁决的接口，但那已经不是这里的同一次操作，必须重新定义重试和状态转换。
“库存永不负数”比“绝不超卖”弱。错误实现可能让 A、B 都从 1 算出 0 并覆盖写回，最终库存仍是 0，却发出了两张成功承诺。因此既要检查状态，也要检查已返回给用户的结果。
用调用和返回构造历史
历史记录至少包括对象、客户端、操作身份、参数、调用事件、返回事件和结果。服务端提交日志是辅助证据，不能代替客户端看到了什么。下面是一段可线性化的历史，数字仅表示一个观察者记录的事件次序。
| 事件次序 | A | B | 可解释的抽象状态 |
|---|---|---|---|
| 1 | 调用 reserve(A) | stock=1 | |
| 2 | 调用 reserve(B) | 两次调用重叠 | |
| 3 | 返回 RESERVED | 可以把 A 的生效点放在 1 与 3 之间，库存变为 0 | |
| 4 | 返回 INSUFFICIENT | 可以把 B 的生效点放在 A 之后、4 之前 |
线性化要寻找一个合法的顺序历史，使每个已完成操作仿佛在自己的调用与返回之间瞬间生效，并保留不重叠操作的真实时间关系。上表可以选择 A → B。如果两次都成功，则无论选 A → B 还是 B → A，第二次成功都违反抽象规范，没有合法生效点可找。
更容易漏掉的情况是：A 已返回成功，B 才开始，B 却仍读到 1 并成功。这里不能借“并发时任意排序”解释，因为 A 的返回在 B 的调用之前，合法顺序必须是 A 在 B 前。真实时间先后最好由“收到 A 的响应后才发送 B”这样的因果实验建立；不能假设两台机器的墙钟时间戳足够精确，就据此排出所有事件。
Herlihy 与 Wing 的线性化论文给出了以并发历史和顺序规范判断对象正确性的定义。这个定义不要求客户端知道真正的物理生效时刻，但要求实现能为所有允许的历史提供一致解释。
超时留下待定操作，不能先当作失败
设 A 调用预订后超时，没有拿到业务响应。随后 B 返回 INSUFFICIENT，readStock() 返回 0，而且模型中没有别的写入。可以把 A 补全为成功来解释这段历史；若直接删掉 A，B 的不足和库存 0 就失去了合法来源。
反过来，若 B 返回成功、库存为 0，A 也可能根本没生效。检查未完成调用时，需要尝试合法的完成扩展：为部分待定调用补上响应，再检查完整操作的顺序；没有生效且不影响已完成观察的待定调用可以不纳入最终顺序。关键是保留 UNKNOWN 的可能性，不能预先断言所有超时都失败，也不能断言它们都成功。
落地时把两层状态分开：RPC 等待结束是客户端事件，业务操作的提交或拒绝是对象事件。TimeoutException 只能证明前者。客户端应以原身份查询或重试，让系统返回已保存的结果；换新身份再次购买，会把“恢复一次未知操作”变成“提交第二次操作”。去重身份保留多久、能否查询历史结果，则是这份接口必须补充的恢复约定。
一致性模型约束的是哪些观察
| 模型 | 需要保留的顺序 | 一个能暴露差别的历史 |
|---|---|---|
| 线性化 | 每个客户端程序顺序，以及不重叠操作的真实时间先后 | 写入 1 已成功返回后，另一客户端才发起读，不能返回旧值 0 |
| 顺序一致 | 存在一个保留各客户端程序顺序的全局顺序 | 没有额外同步约束时，可把另一客户端的旧读排在那次写之前，即使实际调用发生得更晚 |
| 因果一致 | 先写后读、读到某写后再写等因果依赖 | B 读到 A 的“建立帖子”后再发评论，观察者不能先看到评论而看不到其因果前提；无因果关系的并发写可有不同顺序 |
| 最终一致 | 在停止新更新、通信恢复且修复过程持续推进等前提下最终收敛 | 可以暂时读旧值；仅说最终收敛没有给出陈旧时长、冲突保留规则或恢复期限 |
顺序一致的定义来自 Lamport 的原始论文。不同模型不是按产品名字自动赋予的：必须问具体对象、读取入口和操作范围。例如主库写是线性化的，不代表从异步只读副本读也满足同样保证。
线性化具有逐对象组合的性质：若各对象的历史都可线性化，它们组合后的对象历史也可线性化。但“两个独立对象都提供线性化操作”不等于“先扣库存、再扣余额”这一个跨对象业务动作具有原子性。中途崩溃仍可能只完成一半。要把整段动作作为一个操作承诺，需要覆盖它的事务或跨资源协议，不能把单键原子性直接扩大到业务边界。
故障模型决定证明能走多远
| 故障 | 模型必须允许的行为 | 容易误用的结论 |
|---|---|---|
| 崩溃停止 | 进程停止且不再执行后续步骤 | 若实际会重启或暂停恢复，就不能假定旧执行者永远消失 |
| 暂停后恢复 | GC、调度或宿主机暂停后，从旧程序位置继续 | 租约过期不等于旧进程已停止；后续资源写需单独裁决 |
| 延迟、丢包、分区 | 消息可能很晚到达、回复可能丢失，两侧可能都活着 | 超时只能触发本地恢复策略，不能证明远端未提交 |
| 时钟偏移或跳变 | 不同墙钟不同步，墙钟可被调整 | 不能靠跨机器时间戳大小证明全局写入顺序 |
| 重启与持久状态丢失 | 明确哪些日志已经耐久、哪些只在内存里 | 内存去重表在重启后消失，原来的重试证明就不再适用 |
| 磁盘损坏或拜占庭行为 | 数据被损坏，或节点任意伪造消息 | 普通崩溃容错复制不自动容忍这些行为，需要另设校验、恢复或协议假设 |
本库存模型假设裁决状态不被恶意修改，原子提交后能按声明的持久化规则恢复；它不证明磁盘控制器的承诺，也不容忍任意恶意节点。旧持有者暂停恢复的资源裁决，统一见租约和 fencing 令牌。复制系统如何在分区中选择可完成的操作，见CAP、quorum 与共识。
把候选方案放回同一份承诺比较
方案 A 将库存条件检查、扣减和请求身份结果放入同一数据库事务，以提交作为裁决点。它把正确性集中在一个权威写域，但热点库存会竞争，事务持久化和跨区往返会进入响应路径；数据库自身的故障切换保证仍要另查。
方案 B 在缓存预扣后异步落库。缓存上的原子减法只保护缓存操作本身，不能消除预扣后崩溃、缓存重启丢状态、落库重放和取消补偿的分支。如果接口仍立即承诺已获库存，就必须证明这些分支也保留成功承诺；仅说“失败后补偿”还不够，因为补偿可能晚到、重复或失败。
若业务允许排队，可以把 B 的响应改为 ACCEPTED，随后查询 RESERVED/REJECTED。这样可能提高接纳能力，但新承诺是“意图已耐久受理且能查终态”，必须有积压期限、失败终态和恢复者。它没有神奇地让原先的立即成功契约更容易满足，而是明确改变了用户可观察的操作。
条件变化后要重新建模。加入取消时，需要让“已成功数”变为当前有效预订，并规定取消与发货的竞争；加入多 SKU 套餐时，要决定能否部分成功；加入异步副本读时，要声明读取是否允许陈旧。不能只在原图上多画一个缓存或队列。
实验：先找反例，再检查实现是否保留原子边界
输入为库存 1、A/B 各扣 1，记录每个调用、返回、身份和最终库存。先做下列纸面事件实验，不需要集群。
- 错误实现拆成“读库存、判断、写库存”。安排
A读1 → B读1 → A写0并成功 → B写0并成功，预期最终库存为 0、成功数为 2，违反成功承诺。若实现采用无条件自减而不是覆盖写，另一种反例会得到 -1。 - 将判断与扣减建模为一个原子操作。重叠调用只有
A成功/B不足或B成功/A不足两类合法结果；若 A 返回后 B 才调用，则只能是前者。 - 在 A 的原子提交之后丢弃响应。以相同身份重试，预期取回原来的成功、库存保持 0；改用新身份，预期不足。若把丢响应误作未提交并再次扣减，就暴露恢复协议的缺口。
- 收集完整历史后再检查不变量。不能只拿最终库存截图：重复扣减后补回，也可能已向用户发出两次成功。
可从仓库根执行现有有限模型：
python3 labs/system-design/model_check.py系统不变量模型说明与脚本使用初始余额 100、两笔 80 的扣减，各身份重复一次，枚举 6 种线性化顺序，并含提交前失败、提交后丢响应和同键改金额。预期合法分支余额为 20、只有一笔成功流水；故意错误的“分别预查再扣”分支展示 -60。金额和库存算例不同，脚本也把完整事务当作一个原子转换，因此它检查的是模型内不变量，不能替代上面拆开的真实并发历史。
本页的事件表是可复核的纸面推演，不是已运行的数据库或多节点结果。实机下一步是在专用测试数据上用双会话安排预查交错、提交前后断连，再用客户端历史与持久记录核对；必须说明隔离级别、SQL 条件、唯一约束和耐久配置。若 SQL 少了模型里的条件，模型通过也不能替它担保。
三轮追问：模型变化后答案是否仍成立
第一轮：A 超时，客服是否可以直接重新创建一个订单？ 不能把新身份当作原请求恢复。先用原身份查询或重试；若无法确认，要暴露待确认状态并指定恢复责任。否则 A 已提交时，新订单可能再次消耗库存。评分看是否保留 UNKNOWN、复用身份并给出查询路径。
第二轮：取消释放库存后，原先不足的请求重试能成功吗？ 按本页契约不能，原身份绑定了原结果；新购买意图使用新身份。若产品选择自动重新竞争，需要把“预约意图”建成可多次尝试的状态机，区分意图身份与尝试身份，并重写取消、重试和终态规则。评分看是否识别契约变化，而非只改一条 SQL。
第三轮：库存和余额服务分别线性化，组合购买还缺什么？ 逐对象读取和更新可以组合成线性化对象历史，但“购买成功意味着两者都完成”的多对象不变量不在任一单对象操作内。需要跨对象原子协议，或明确待确认、补偿和终态的长流程契约；代价是阻塞、协调成本或中间态。评分看是否区分对象组合性质和业务事务原子性。
闭卷验收
本页 3 道闭卷题收进了下方自测面板：先回忆，再展开参考答案与评分点，最后给三档自评。