分布式数据正确性
从契约开始
写下不变量、其作用范围以及它必须承受的故障。“一个订单最多只扣费一次”是有效的；“强一致性”则不够充分。确定权威记录、派生视图、参与者和每个提交/确认边界。询问客户端是否需要读己之写、因果顺序、线性化操作、可序列化事务，还是仅仅最终一致性。
审查流程
- 绘制写入路径，包括数据库提交、代理确认和外部副作用。记录每个成功响应在进程崩溃、机器故障或副本故障转移后保证了什么。超时意味着结果未知，不一定是执行失败。
- 列举每个持久化步骤之前和之后的崩溃窗口。针对每个窗口，重放操作并检查不变量。同时测试并发尝试和顺序重试。使用故障分类账。
- 当业务效果及其去重标记共享一个数据库时，将它们放在同一事务中。对于外部事件，考虑使用事务性发件箱。对于远程效果，要求提供持久化的提供者幂等性契约或协调状态机。代理传递保证在其记录的事务边界处停止。
- 确定排序范围：键、分区、流或全局。选择能维护不变量最窄的范围。分区日志对其分区内的消息排序；它不会自动排序不同分区中的相关事件。
- 对于复制和故障转移，检查选举、隔离、确认策略和恢复。
R + W > N在固定成员关系下提供集合交集；它本身并不建立线性一致性。参见一致性。 - 对于分片，验证事务局部性、热点键、再平衡和唯一性强制执行。衡量最繁忙的分片，而不仅仅是聚合吞吐量。
- 针对可疑的保证，生成最简反例以及一个能执行该反例的测试。区分必需的保证和可接受的陈旧性。
审查输出
返回：不变量 → 假设 → 故障时间线 → 违反的保证 → 最小修复 → 代价 → 验证。包含针对已经不一致数据的恢复路径。指出任何依赖于特定数据库、代理或提供者版本的行为。
推荐前检查
- 重试的请求能否使用不变的参数复用其稳定的操作ID？
- 租约持有者是否需要由资源强制执行的单调递增的隔离令牌？仅靠租约过期无法阻止暂停的进程。
- 副本能否在成功写入后立即提供陈旧值？
- 墓碑记录或去重记录是否在重放视窗之前过期？
- 多记录不变量是否需要事务或显式协调？
范围和参考
部分覆盖范围与数据密集型应用系统设计（第2版，Kleppmann和Riccomini）一致。这些原始程序使用了作者的公开课程笔记和额外的原始文档；完整书籍不可用。请阅读来源以获得准确的归属。本技能不提供共识实现，也不假设拜占庭容错。