日志里写出的顺序,只有在说明它应当保留哪些关系之后才有意义。
建立 happens-before 关系,区分逻辑时间与墙钟时间,把请求记录转换为操作区间。
前置:系统与故障假设。
同一进程内先执行的步骤先于后执行的步骤;发送消息先于收到这条消息。再加上传递关系,就是 happens-before。如果不存在从任一事件到另一事件的关系链,它们在该模型中就是并发事件,即使墙钟标签不同。
A: a1 ── send(m) ───────────────── a3
╲
B: b1 ───────── receive(m) ──────── b3
C: c1 ──────────────────────────── c2
C 没有消息边:时间戳本身不能补出因果关系。Lamport 时钟在本地事件时递增,收到消息时推进到超过收到的时间戳。若 a → b,则 L(a) < L(b);反过来不成立,计数较小不证明存在因果关系。以进程 ID 打破平局能构造方便的全序,却不能发现不存在的因果边。向量时钟能保留更多因果信息,同时增加元数据;首版不实现向量时钟。
调用开始和响应结束界定客户端操作。成功请求的服务端提交一般位于区间内,但客户端并不直接观察该事件。超时后请求仍可能继续;不能把客户端截止时间冒充检查器中的成功响应。
| 记录 | 能支持什么 | 单独不能证明什么 |
|---|---|---|
| 客户端单调时钟起止 | 同一记录者上的操作区间 | 未同步主机间的全局先后 |
| 服务端 revision | 同一 etcd 集群谱系内的变更顺序 | UTC 时间或跨集群顺序 |
| 超时 | 截止前未收到成功响应 | 没有副作用 |
真实运行只有一台主机和一个编排者,耗时使用它的单调时钟。导出的 JSON 是选定的机制证据,不是抓包记录。交互检查器只接受已完成读写,并要求输入区间处于可比较的同一时间轴。
打开历史检查台,加载“并发”。写跨越 0–4,第一次读跨越 1–3 并返回初值 0。把这次读放在写前,就存在合法解释。第二次读从 5 开始;在线性一致模型中,它应反映已完成的写。
w1: write(1) [0,4]
r1: read()→0 [1,3]
r2: read()→1 [5,7]
一个可能的顺序:r1 → w1 → r2把 r1.start 改成 4.5,r1.end 改成 4.8,再运行。真实时间关系迫使写在这次旧值读之前,因此不再存在合法的寄存器顺序。
不能。逻辑时钟单向保留因果顺序;两个独立事件也可能有不同的 Lamport 时间戳。
一般不行,它可能已生效。完整检查需考虑未完成操作的可能补全或省略。本检查台拒绝未完成操作,不对这种历史作结论。