TLA+ 建模技巧

Source: Hacker News

模型极简化

从一个微小的核心开始，并在扩展时始终保持一个可工作的模型。你的默认做法应该是省略。只有在你能解释如果省略会导致不工作时才添加组件。大多数模型关注的是行为的某一切片，而不是完整系统的全部辉煌：例如，领导者选举、修复、重新配置。如果某些层或组件不影响该切片，就将其全部剔除。 抽象是知道该剪掉什么的艺术。删除应当带来喜悦。

模型规范，而非实现

使用声明式写法。说明必须满足的条件，而不是实现方式。如果你的规范复制了控制流、循环或辅助函数，那实际上是在模拟代码。去掉它们。每个变量都必须有其存在的必要性。多余的变量会扩大状态空间（模型检查时间），并隐藏错误。反复自问：我能推导出这个值而不是存储它吗？例如，如果可以将 WholeSet 定义为现有变量的状态函数，就不需要维护 WholeSet 变量：

WholeSet == provisionalItems \cup nonProvisionalItems

审查模型的非法知识

完整阅读你的模型，检查每个进程实际上能够看到什么。TLA+ 使得读取全局状态（或其他进程的状态）变得很容易，而真实的分布式进程根本不可能原子地观察到这些状态。这是最常见的建模错误之一。请专门进行一次检查，以消除非法的全局知识。

检查原子性粒度

将操作推向尽可能细粒度，只要正确性允许。过大的原子操作会隐藏竞争并使并发论证失效。细粒度的操作会暴露出协议必须容忍的真实交错。

用受保护命令思考，而不是过程

每个操作应当表达受保护命令风格中的一个逻辑步骤。守护条件（guard）理想情况下应定义该操作的意义。把所有使能条件都放在守护条件中。如果守护条件成立，操作可以在真实的事件驱动风格中随时触发。这也是我现在更倾向于直接编写 TLA+ 而不是 PlusCal 的原因：TLA+ 强迫你以受保护命令的方式思考，这正是分布式算法应有的设计方式。是的，PlusCal 对开发者更易读，但它也会把你推向顺序实现思维。最近，借助 Spectacle 等工具，分享和可视化探索 TLA+ 规范变得更加容易。

Step back and ask what you forgot to model

没有任何东西可以替代对系统深入思考。TLA+ 建模仅用于帮助你深入思考系统，不能代替对系统的思考。检查是否已经纳入了所有相关方面：故障、消息乱序、修复、重新配置。

编写 TypeOK 不变式

TLA+ 没有类型系统，因此应通过编写 TypeOK 不变式显式且尽早地声明类型。一个好的 TypeOK 不变式为你的模型提供可执行的文档。只需几秒钟即可完成此工作，从而为你节省大量在 TLA+ 反例日志中追踪运行时错误的时间。

尽可能多地写出不变式

如果某个属性很重要，请将其明确为不变式。尽早编写它们。随着时间的推移逐步扩展。尽量让你的不变式保持尽可能严格。记录你对不变式和非不变式的学习体会。TLA+ 规范是一种沟通工具。为读者而写，而不是为 TLC 模型检查器。为清晰起见，要明确且乏味。

编写进度属性

安全不变式本身不足。检查事情最终会发生：请求完成，领导者出现，目标实现。许多“正确”的模型可能会悄悄永远什么也不做。检查进度属性可以捕获停滞的路径。

对成功保持怀疑

一次成功的 TLC 运行并不能证明什么，除非模型探索了有意义的行为。低覆盖率或极小的状态空间通常意味着模型约束过多或有错误。故意破坏规范，以检查你的规范是否真的在做实质工作，而不是以空洞/琐碎的方式放弃。故意注入错误。如果你的不变式没有失败，那它们太弱了。通过破坏来测试规范。

Optimize model‑checking efficiency last

将模型与模型检查器分离。规范应独立存在。使用 .cfg 文件，可以通过适当的配置、约束、计数器的界限以及对称性项来优化模型检查。

您可以在我的博客上找到许多 TLA+ 规范的示例和演练。

在TLA+ 仓库中也有更多示例。