使用TLA +进行分布式系统的建模与调试设计

这篇文章讲述了为什么要对系统进行建模，并使用TLA +框架详尽地测试这些模型/设计。在第一部分中，我将讨论为什么建模您的设计是重要和有益的，在第二部分我将解释为什么TLA +是一个非常合适的建模框架，特别是对于分布式和并发系统。

建模很重要

如果您已经在大型软件系统上工作，那么您就知道它们容易出现 转弯情况 ， 失败的假设 ， 竞争条件 和 级联故障 。

存在许多极端情况，因为存在许多参数，并且这些参数确实相互干扰了意料之外的方式。极端情况违反了关于系统组件和环境的看似合理的隐含假设，例如，“1跳比2跳更快”，“0跳比1跳更快”，并且“进程以相同的速率工作” ”。由于当今（随着SOA，云和微服务的兴起）所有系统都是分布式系统，因此存在丰富的竞争条件。由于其他进程并发执行，所谓的“原子执行块”代码失败。最后，故障发生并且在部署之前几乎总是低估它们的影响。故障会使您的系统进入意外状态，并从那里开始将恢复操作与正常系统操作交互。

大型软件系统不可避免地是分布式系统，有许多未知数和无数种极不可能的方法可能会出错。人类的大脑和推理无法扩展以处理所有这些可能性。为了缓解这些问题，该行业开发了更好的可观察性工具，甚至 在生产中 进行 测试 以提高可用性。这些 工具 非常重要且不可或缺。但是当你弄清楚你的设计存在一些固有的问题时，解决问题可能会太困难和昂贵。 您认为最后10％的项目最终将90％的时间用于生产和运营。

如果您首先对设计进行建模并详尽地测试和调试这些模型以确保对角落情况，失败的假设，并发性和失败的正确性，您可以在设计时捕获错误并在它们发展成问题之前修复它们并且修复成本很高。

• 建模首先不会延长您的开发时间，相反，它可以通过减少徒劳的开发尝试来节省您的时间。采用有缺陷的设计进行开发几乎总能确保实施存在缺陷。虽然拥有精确和正确的模型并不能保证您的模型实现是正确的，但它可以帮助您避免重大/复杂的问题，并为测试您的实现提供了一个很好的参考。
• 构建一个精确的系统模型可以让您清晰思考并极大地支持您的开发。通过建模，您可以发现问题的固有复杂性; 这有助于您集中注意力并 忽略意外/副产品的复杂性。
• 该模型还可以帮助您与您的团队和其他人精确沟通，因为您可以避免自然语言的模糊性。
• 最后，随着手头的模型，您还有机会逐步介绍设计决策，并看到实现设计的其他方法。 

TLA +非常适合建模

TLA +是用于描述和推理分布式和并发系统的形式语言。它由2013年图灵奖得主Leslie Lamport博士开发。由于他的 逻辑时钟工作 和 Paxos工作 ，Lamport是分布式系统中非常重要的人物。在过去十年中，他非常积极地参与改进TLA +框架，以帮助使分布式系统更易于管理。

TLA +使用基本数学来建模和推理算法：实际逻辑，集合论和时态逻辑用于指定系统。最重要的是，该框架集成了一个模型检查器，可以彻底地测试您的模型，以应对极端情况，失败的假设，并发和失败。模型检查器尝试为您的模型执行所有可能的执行，并告诉您哪些执行，您的 不变量 和 系统保证 中断。

基于不变量的推理

TLA +框架促进了 基于不变量的推理， 以防止因 操作推理 而产生的问题。在操作推理中，你从一条“快乐的道路”开始，然后你试着找出“什么可能出错？” 以及如何防止它们。当然，在问题场景的枚举中，你总是会遇到不足，忽视极端情况，竞争条件和级联故障。相比之下，基于不变量的推理主要关注“需要做什么？” 以及如何在任何时候确保此属性作为系统的不变量。基于不变量的推理采用原则的基于状态而非基于操作/执行的系统视图。

为了获得基于不变的推理，我们为模型指定了安全性和活跃性。安全属性指定“系统允许执行的操作”。例如，在任何时候，所有提交的数据都存在且正确。活动属性指定“系统最终应该做什么”。例如，每当系统收到请求时，它最终必须响应该请求。换句话说，安全属性关注的是“没有什么不好的事情发生”，以及带有“好事最终发生”的活跃属性。

用TLA +建模

TLA +框架支持您构建模型并以两种主要方式确定其不变属性。首先，基于数学的形式语言可以帮助您在使用高级声明性语句的同时实现精确性。其次，集成模型检查器会彻底调试您的模型以面对并发和失败，并生成候选不变量失败的反例。（经过多年与TLA +的合作，我仍然对模型检查员为我的模型吐出的反例感到惊讶：很容易忽略一些情况，但模型检查器会让你直截了当。）你通过改进你的模型来解决这些问题或者有时通过放松你的候选不变量，并在经过多次迭代后收敛到一个详尽调试的模型，保证不变量。

即使对于已经实现和运行的系统，构建TLA +模型也是有益的。通过构建模型，您可以更好地了解您的系统，并找出一些 潜在的故障模式， 并在生产之前纠正它们。最后，维护系统的TLA +模型为持续开发提供了重要的好处。虽然软件系统需要经常使用新功能进行扩展，但这些扩展可能会以意外的方式干扰系统并导致停机。使用TLA +模型，您可以先将这些功能添加到模型中，然后使用模型检查器在设计级别捕获/调试问题。这样您就可以在问题出现之前解决它们。

TLA +很实用

由于使用TLA +实际上节省了构建大型软件系统的时间，因此许多软件公司都采用TLA +建模作为实践。

亚马逊还为他们的一些AWS产品使用了TLA +建模，并 撰写了一篇很好的体验报告。 还有报告称使用TLA +来建模硬件系统。

在过去的4年中，我一直在我的分布式系统类中加入TLA +。 TLA +使学生能够学习并发和基于不变的推理，并为他们提供分布式协议的实践经验。在我对新分布式算法的研究中，我也详尽地使用了TLA +。

根据我的经验，可以在几周内获得TLA +。这首先是因为TLA +采用了一种非常简单的状态机方法来建模系统。系统包括：（1）定义系统状态的一组变量，以及（2）用于将系统从一个状态转换到另一个状态的一组有限的分配/动作。

此外， PlusCal 为TLA +提供了一种糖的语法，它具有长时间的增长趋势（由于其低级状态转换中心语法）并且对某些人来说看起来很神秘。PlusCal是一种用于在更高抽象级别编写算法的伪代码，它被转换为模型检查的基础TLA +规范。

TLA+下载

视频： TLA+是一个状态机建模工具

了解更多

Google网上论坛有一个非常活跃的TLA +论坛。Leslie Lamport在几个主题中发出了声音。

我的博客包含许多分布式算法/系统的TLA + / PlusCal建模示例。

LearnTLA提供了TLA + / PlusCal的用户友好介绍。

Lamport的网站包括TLA + / PlusCal资源（视频/书籍/示例）和下载工具包的链接。