# 内容与可视化核查记录

核查日期：2026-11-03。范围：执行与性能 8 项、状态与正确性 8 项、分布式协作 11 项，共 27 个主题。

## 结论与适用范围

本轮发现并修正了实际的教学错误与表达歧义：部分异常流程沿用了正常流程的前置状态；复制确认箭头反向；WAL 未清楚区分页面日志与提交记录的持久化；逻辑对象被画成物理设备；代码行高亮与演示步骤没有语义对应。

现在每个主题均有两套独立的四阶段场景，共 54 个场景、216 个阶段。场景可能演示正常执行、安全拒绝、故障恢复或错误实现的反例；切换场景从其第一阶段重新开始。

这些是按经典课程、原始论文、官方文档整理的教学模型，不是完整实现，也不是对协议的形式化正确性证明。数字、任务名和简化流程是本站构造的示例；来源页区分课程背景与具体机制资料，不把整理目录归为某篇文章的原文。

## 逐主题核查

| 部分 | 主题 | 核查重点与修正 |
|---|---|---|
| 执行与性能 | 缓存与局部性 | 缓存行是缓存阵列内部单位，不是独立存储设备；未命中装入、冲突和伪共享有不同含义。 |
| 执行与性能 | 虚拟内存与 TLB | TLB 未命中不等于缺页；缺页也不必然读磁盘；页面准备后重试指令。 |
| 执行与性能 | 流水线与投机执行 | 区分执行和架构状态退休；错误路径被撤销不代表微架构痕迹全部清除。 |
| 执行与性能 | 线程与任务调度 | 就绪、运行、阻塞分别表达；饥饿反例中的任务明确处于就绪状态。 |
| 执行与性能 | 锁、原子操作与内存序 | 区分互斥、原子性和可见性；死锁等待环使用独立锁持有历史。 |
| 执行与性能 | 异步 I/O 与事件循环 | 就绪通知之后仍需非阻塞读取，处理短读、EAGAIN、EOF、错误；不能直接标为完成。 |
| 执行与性能 | 有界队列与背压 | 容量检查和入队在同一同步边界；修正队列计数与拒绝目标。 |
| 执行与性能 | 性能测量与瓶颈 | 只看均值的反例不再预先检查尾延迟；Amdahl 上界说明理想假设。 |
| 状态与正确性 | 事务与原子提交 | 账户是状态对象，事务执行器实施操作；入账失败发生在提交前，回滚不得留下半笔转账。 |
| 状态与正确性 | 隔离级别与两阶段锁 | 2PL 不等于 2PC；低隔离反例不再继承已持有排他锁的历史；READ COMMITTED 示例明确针对 PostgreSQL。 |
| 状态与正确性 | MVCC 与快照 | 版本可见性不等于可串行化；医生值班的写偏差使用独立双事务场景。 |
| 状态与正确性 | 乐观并发控制 | 验证与更新必须有原子边界；单记录版本不自动保护多记录或范围条件。 |
| 状态与正确性 | 预写日志 WAL | 数据页刷盘前满足 durableLSN ≥ pageLSN；同步提交成功确认还要求日志持久到 commitLSN。 |
| 状态与正确性 | 崩溃恢复与检查点 | 检查点不代表全库同一时刻刷盘；区分重做、撤销或可见性排除；恢复本身可重复启动。 |
| 状态与正确性 | B+ 树与 LSM 树 | 两者是替代访问路径，不串接为同一次写入；flush 和 compaction 由条件触发。 |
| 状态与正确性 | 不变量与状态机验证 | 安全属性检查与活性循环检查不同；活性依赖明确环境和公平性假设；模型结果需对应实现。 |
| 分布式协作 | 超时、重试与退避 | 超时仅代表结果未知；有限预算、稳定身份、随机退避与不可重试错误分开处理。 |
| 分布式协作 | 幂等键与结果去重 | 去重身份、参数检查、唯一约束与业务效果处于正确原子边界；说明保留期与外部副作用限制。 |
| 分布式协作 | 消息、确认与重放 | 消费者提交业务后再 ACK；确认前崩溃是独立流程；重复投递不应重复业务效果。 |
| 分布式协作 | 序号、版本与任期 | 在真实提交边界核对目标、执行身份和任务状态；到达时间不能替代版本顺序。 |
| 分布式协作 | Raft 与复制日志 | B 的持久化确认从 B 指向 Leader；当前任期、多数证据与按序应用分开；分区发生在 Follower 存盘之前。 |
| 分布式协作 | 线性一致性与读协议 | 区分写成功确认和调用；旧副本读必须保留真实时间先后；会话保证不等于线性一致性。 |
| 分布式协作 | 分片与数据迁移 | 背景复制之外还需冻结/最终增量与所有权交接；路由更新不能单独撤销旧节点写权限。 |
| 分布式协作 | 租约与隔离令牌 | 资源原子保存并核对最高已见令牌；不能把最高令牌比较说成精确获知租约到期；反例资源自始未实现隔离。 |
| 分布式协作 | 跨系统原子性与 Outbox | 本地业务与发送意图原子提交；等待消息系统确认后才标记；重复发布箭头为转发器到消息系统。 |
| 分布式协作 | 身份、权限与故障隔离 | 认证与按资源授权分开；拒绝结果不能描画为业务写入；资源隔离不能只靠前端按钮。 |
| 分布式协作 | 可观测性与进度检查 | 心跳和业务进展分别观察；恢复执行前需要重复防护和旧执行隔离。 |

## 可视化语义

- 矩形是抽象逻辑节点，不宣称是四台机器或实际物理拓扑。
- 请求和数据传递用实线箭头；控制关系与条件检查用虚线，并显示关系名称。
- 请求到达后被拒绝：在接收端显示红色拒绝标记。
- 请求未到达：连线在途中截断，接收节点不高亮；不再画成已送达。
- 节点内部操作不画自我传递箭头；方案对照没有方向箭头。
- 状态表、步骤文字、图中端点与关系类型取自同一个场景阶段。
- 伪代码随主流程/替代场景切换；不再根据步骤序号机械高亮代码行。
- 知识图谱保留全部 27 个主题，仅突出当前主题的直接关联；连线无方向，不代表执行顺序或前置课程。跨越两个部分的连线绕过中间节点。

## 主要依据与整理边界

| 范围 | 具体依据 | 边界 |
|---|---|---|
| 缓存 | [CMU 15-213 Cache Memories](https://www.cs.cmu.edu/~213/lectures/10-cache-memories.pdf) | 缓存访问示例用于解释行、集合及未命中，并非某款 CPU 的完整一致性协议。 |
| 虚拟内存、调度、并发 | [OSTEP](https://pages.cs.wisc.edu/~remzi/OSTEP/) 的 TLB、缺页、进程、调度、条件变量、并发错误章节 | 页面来源页链接到对应章节；具体 OS 与硬件实现有差别。 |
| I/O | [epoll(7)](https://man7.org/linux/man-pages/man7/epoll.7.html)、[read(2)](https://man7.org/linux/man-pages/man2/read.2.html) | 就绪模型不等于所有异步 I/O 都采用同一 API。 |
| 隔离与 MVCC | [PostgreSQL 18 事务隔离](https://www.postgresql.org/docs/18/transaction-iso.html)、[CS186 并发控制](https://cs186berkeley.net/notes/note12/) | 锁和版本是不同实现方法；各产品对隔离级别的实现需单独核对。 |
| WAL、恢复 | [PostgreSQL WAL](https://www.postgresql.org/docs/18/wal-intro.html)、[事务实现说明](https://github.com/postgres/postgres/blob/master/src/backend/access/transam/README)、[CS186 Recovery](https://cs186berkeley.net/notes/note14/) | 不将 ARIES 的物理 UNDO 路径强加给所有数据库；同步提交保证有明确范围。 |
| OCC | [Kung 与 Robinson 原始论文](https://www.eecs.harvard.edu/~htk/publication/1981-tods-kung-robinson.pdf) | 单记录版本示例是缩小模型，不能替代完整读写集与谓词验证。 |
| 索引 | [CS186 B+ Trees](https://cs186berkeley.net/notes/note4/)、[RocksDB Overview](https://github.com/meta/rocksdb/wiki/RocksDB-Overview)、[Write Stalls](https://github.com/meta/rocksdb/wiki/Write-Stalls) | 不保证 LSM 对所有工作负载都有更低总成本。 |
| 状态与正确性 | [Lamport, Specifying Systems](https://lamport.azurewebsites.net/tla/book-21-07-04.pdf) | “状态与正确性”是本站综合组织方式，不是某门课程或文章的原始章节名。 |
| 复制与一致性 | [Raft 原始论文](https://raft.github.io/raft.pdf) | 省略选举、成员变更和完整读协议；多数提交示例明确为当前任期条目。 |
| 重试与幂等 | [AWS 重试资料](https://aws.amazon.com/builders-library/timeouts-retries-and-backoff-with-jitter/)、[幂等 API](https://aws.amazon.com/builders-library/making-retries-safe-with-idempotent-APIs/) | 结果去重不自动涵盖事务外部副作用。 |
| 消息与 Outbox | [RabbitMQ 确认机制](https://www.rabbitmq.com/docs/confirms)、[AWS Transactional Outbox](https://docs.aws.amazon.com/prescriptive-guidance/latest/cloud-design-patterns/transactional-outbox.html) | ACK、发布确认和下游业务完成是不同事件；仍需处理重复。 |
| 分片迁移 | [MIT 分片实验](https://pdos.csail.mit.edu/6.824/labs/lab-shard1.html) | 本站背景复制、最终冻结及交接组合是综合示例，不声称照搬实验实现。 |
| 租约与隔离 | [Chubby 原始论文](https://www.usenix.org/legacy/event/osdi06/tech/full_papers/burrows/burrows_html/) | 本站使用简化单调令牌模型；原文 sequencer 的锁代次验证不等于此处全部伪代码。 |
| 授权 | [OWASP Authorization Cheat Sheet](https://cheatsheetseries.owasp.org/cheatsheets/Authorization_Cheat_Sheet.html) | 教学示例不能替代产品级威胁建模和权限审计。 |

## 验证记录

- JavaScript 语法检查与内容契约检查：27 个唯一主题、三部分数量 8/8/11、54 个独立场景、216 个有效关系阶段、来源与关联引用均通过。
- 针对历史错误增加回归检查：Raft 确认方向及未送达类型、WAL 提交持久化说明、MVCC 独立参与者、索引替代路径、缓存行建模。
- 浏览器逐帧遍历全部 27 个主题、54 个场景、216 个阶段：每阶段检查四个节点、图示关系与轨迹表匹配、状态文字一致、内部操作无传递箭头、方案对照无箭头、标签边界；未发现检查项失败。完整逐帧记录位于 `docs/browser-audit.json`。
- 额外实测：Raft 的 B → Leader 确认；未送达消息在中途截断且目标不高亮；跨部分知识图谱保留 27 个节点和正确关联端点；主流程/替代场景的伪代码独立切换；播放时出现传递动画、暂停后移除；速度切换；来源类型显示。
- 移动端抽查使用 390 px 宽预览框（滚动条占用后内容宽 375 px），验证租约、版本主题的导航、场景切换、节点标签和说明区域；未出现页面横向溢出。英文节点标签已改为按词换行。
- 留存修正后 Raft 确认与未送达场景截图。
- 内容契约检查只验证数据与渲染约定，不穷举所有协议执行；没有声称通过模型检查器证明这 27 种技术实现正确。


## IsoKit 绘图层更新（2026-11-03）

机制演示已接入真实的 `react-isokit@0.5.0`，内容数据未改变。`Plate`、`Box`、`Glow` 与 `Signal` 负责等轴测图形和传递动画，协议关系仍由已核查的场景决定。数据与控制关系、拒绝、丢包、内部操作、方案对照的语义保留。上文逐帧浏览器记录对应前一次内容核查；本次新绘图层已通过全部 216 阶段的实际组件渲染回归，以及暂停、减少动画、端点投影、独立标签与中途截断检查。初版桌面预览已目视确认；最终版本的交互、手机和深色模式浏览器复查因自动审批服务容量错误及超时未完成。

## 连线圆点动画修正（2026-11-03）

后续根据“连线上的点没有动起来”的反馈，将请求/数据传递的 `Signal` 短线动画替换为沿相同 IsoKit 路径坐标移动的实心圆点；节点端口仍保持静止。手动切换步骤会预览一次传递，暂停保留当前位置，继续播放沿原位置前进，末步拥有完整播放时间。减少动画偏好仍受到尊重。内容数据不变。

已补充轨迹插值、暂停/继续、速度、掉帧、清理和最后一步停留的回归检查，并通过全部 216 阶段的真实组件渲染检查。浏览器定向实测了圆点坐标变化、手动切步、暂停及继续；没有将本次定向检查表述为全部场景的浏览器复查。详见源码中的 `docs/motion-fix.md`。