TLA+ mental models
Author: Murat Buffalo | Source: muratbuffalo.blogspot.com
摘要
TLA+的语法复杂度正在消失（LLM可以帮助），但内在复杂性 remains：知道从哪里开始建模，忽略什么，如何选择正确的抽象。这是建模判断力，是最难教会的技能。
1. 抽象、抽象、抽象
知道忽略什么比知道建模什么更重要。
- 抽象是从复杂系统中切出感兴趣的协议
- omission is the default：只有当忽略某物会破坏推理目标时才添加
- Leslie Lamport推导Paxos：从最抽象的规范开始，定义基于投票的agreement
案例：CosmosDB一致性建模
我们建模的是客户端一致性语义，而不是分布式数据库引擎。如果建模后者会导致状态空间爆炸。
2. 拥抱全局共享内存模型
TLA+的核心fiction：所有进程都可以读写的全局共享内存。
- 程序 = 全局状态空间 + 转换状态的动作集合
- 每个动作遵循Hoare三元组：{state} action {state'}
- guard是状态空间上的谓词，为真时动作"enabled"
关键洞察：不要建模channels、消息序列化或网络拓扑，除非这些是你正在推理的具体内容。
3. 细化到局部guard和效果（慢即是快）
常见建模错误：写一个检查三个不同节点同时做了什么guard——这是"非法知识"，因为真实分布式系统中没有节点能原子观察到这些。
关键洞察：使用单调或局部稳定谓词作为guard
- 稳定谓词：一旦为真，永远为真
- 局部稳定谓词：只有节点自己的动作能使其为假
- 如果guard依赖单调谓词，协议需要更少协调，能优雅容忍通信延迟
Paxos案例：ballot number的单调结构确保acceptor的本地知识永远不会失效。
4. 推导好的不变量
不变量是协议保证的精炼版本：
- 指导你探索协议变体
- 组合组件时的契约
- 直接转化为运行时断言
- 故障恢复的基础
常见失败模式：写"平凡的不变量"——无论协议做什么都为真。
5. 通过逐步细化探索 alternatives
从最抽象的规范开始，逐步添加细节。每一步细化都会使guard更加局部化。
6. 积极细化原子性
允许尽可能多的并发，同时确保实现能负责任地享受这种自由。
总结
TLA+迫使你进入不同模式：数学的、声明式的、全局的。你指定必须保持什么，而不是如何实现它。一旦适应这种转变，它会改变你思考系统的方式。