介绍：Nuwa是飞天分布式系统中提供分布式协作的基础服务，支持阿里云几乎所有的计算、网络、存储等云产品。在女娲分布式协同服务中，一致性引擎是核心基础模块，支持Paxos、Raft、EPaxos等多种一致性协议，并根据业务需求支持不同的业务状态机。如何保证一致性库的正确性是一个很大的挑战。我们引入了TLA+、Jepsen等工具来保证一致性库的正确性。本文从程序员的角度介绍形式化验证工具TLA+。作者|祥光源|阿里巴巴科技公众号1简介Nuwa是飞天分布式系统中提供分布式协作的基础服务，支持阿里云几乎所有的计算、网络、存储等云产品。在女娲分布式协同服务中，一致性引擎是核心基础模块，支持Paxos、Raft、EPaxos等多种一致性协议，并根据业务需求支持不同的业务状态机。如何保证一致性库的正确性是一个很大的挑战。我们引入了TLA+、Jepsen等工具来保证一致性库的正确性。本文从程序员的角度介绍形式化验证工具TLA+。通常很难从理论上证明程序或算法的正确性。在工程中，一般通过测试来发现问题，但是再多的测试也不能保证覆盖所有的行为，那些没有覆盖的行为就成为潜在的隐患，一旦在网上曝光，往往会带来难以预料的后果。形式化验证就是为了解决这样的问题。它利用计算机强大的计算能力，暴力搜索所有可能的行为，检查是否满足预先设定的属性。任何不符合预期的行为都能被发现，从根本上保证了算法的正确性。2TLA+简介TLA+（TemporalLogicofActions）是由LeslieLamport开发的一种形式化验证语言，用于程序设计、建模、文档化和验证，尤其是并发系统和分布式系统。TLA+的初衷是用简单的数学理论和公式来准确描述系统。TLA+及其相关工具有助于消除程序中难以发现且纠正成本高昂的基本错误。要使用TLA+对程序进行形式化验证，首先要用TLA+对程序进行描述，这样的描述称为规范。获得规范后，您可以使用TLC模型检查器来运行它。运行的进程会遍历所有可能的行为，检查Specification中设置的属性，发现意想不到的行为。TLA+以数学为基础，运用数学思维，与任何编程语言都不相似。为了降低TLA+的门槛，Lamport开发了PlusCal语言，它类似于编程语言，可以方便地描述程序逻辑，并且可以借用TLA+提供的工具直接将PlusCal翻译成TLA+。大多数工程师会发现PlusCal是开始使用TLA+最简单的方式，但简单的代价是PlusCal不具备TLA+的一些功能，有时不能像TLA+那样构建复杂的模型，所以PlusCal无法替代TLA+。使用PlusCal编程语言先完成基本逻辑，然后在生成的TLA+代码的基础上进一步修改，可以简化TLA+的开发。TLA+的三个应用TLA+在学术界和工业界都有广泛的应用。TLA+Examples给出了一些使用TLA+验证的分布式和并发算法。在分布式算法和并发算法的研究领域，提出新的算法或者改进现有的算法，TLA+验证基本是标配。除了引入非正式的演示，很多分布式算法论文都会包含TLA+的Specification，以证明他们的算法已经过正式验证。对于熟悉TLA+的业内人士来说，直接阅读TLA+规范甚至比阅读一大段论文还要快。如果看不懂论文的语言描述，或者觉得有歧义，可以查看TLA+规范进行对比，有时是看论文的利器，有时甚至一些算法细节只能在TLA+的Specification中才能看到。由于规范在逻辑上严密无懈可击，因此可以更好地用作实施指南。Lamport的TLA+主页列出了一些TLA+在行业中的应用。以亚马逊为例，部分亚马逊AWS系统的核心算法使用TLA+进行形式化验证。表1列出了TLA+针对部分AWS系统发现的问题，涵盖了一些非常核心的组件。核心部件的问题一旦暴露在网上，损失将不可估量。正是如此，现在分布式云服务的核心算法采用TLA+验证设计已经成为行业标准，所以作为云服务从业者或者对此感兴趣的学生，熟悉TLA+绝对是不可或缺的加分项。表1：TLA+针对AWS系统发现的问题4TLA+入门在VSCode中安装TLA+插件，开始使用TLA+。这是一个开始使用TLA+的简单示例。考虑一个单比特时钟，由于只有一个比特，它只能取值0或1，其行为仅在以下两种情况下：0->1->0->1->0->...1->0->1->0->1->...我们如何在TLA+中描述这个时钟？为了更容易上手，我们使用PlusCal，这样更方便工程师上手：图1：PlusCaldescriptionofasingle-bitclock图1是PlusCaldescriptionofasingle-bitclock，我相信有编程基础的同学都能轻松看懂。这一段PlusCal代码可以使用TLA+提供的工具直接翻译成TLA+代码：图2：TLA+对单比特时钟的描述有了上面PlusCal的基础，理解这一段TLA+就不难了，重点是关于Spec的理解。规范定义了系统的行为。图3描述了单位时钟的行为。Init将时钟初始化为0或1，Tick使时钟在0和1之间来回跳转，Stutter保持时钟不变。TLA+的运行过程其实就是图上的遍历。图3：单比特时钟的行为要运行此TLA+，需要将上述TLA+代码保存到clock.tla文件中。此外，还需要编写一个如图4所示的clock.cfg文件。clock.cfg文件的内容很简单，就是指明运行哪个Specification，检查哪个Invariant。图4：clock.cfg文件的内容有了这两个文件，就可以用TLC运行了。运行后得到如图5所示的结果，图中显示了一些统计信息。图5：运行结果五TLA+原理为了理解TLA+的运行原理，搞清楚它是如何遍历的，我们可以在运行的时候加入一些参数，让TLC输出状态图。比如我们运行一段图6所示的TLA+代码，图7就是运行需要的cfg文件。此示例试图找到面额为1、2和5的钞票的所有组合以组成19。图6：money.tla图7：运行money.cfg后，可以得到图8所示的状态图，图中的顶点是状态，一共有20个状态。Money=0是初始状态，money=19是终止状态，图中的边是动作，一共有4个动作：Add(1)、Add(2)、Add(5)和Terminating。图8：状态图TLA+的操作是完全串行的。操作过程就是在状态图上遍历状态图。每遍历一个状态，检查当前状态是否满足预先设定的不变量。然后继续遍历，不满足立即报错。TLA+会尝试所有的遍历路径而不会遗漏任何行为。我们知道图的遍历方法有两种：深度优先和广度优先。TLA+默认为广度优先遍历。它还可以配置为深度优先模式或随机行为模式。深度优先模式需要最大深度。现在我们知道TLA+的原理其实就是遍历检查状态图的过程。这个过程看似简单，却可以覆盖算法的所有路径，不遗漏任何行为。事实上，我们经常使用TLA+来检查算法的Safety和Liveness属性。六、TLA+并发相信读者对TLA+的原理已经有了初步的了解，但是细心的读者可能心里还有一个很大的疑问：TLA+的运行过程是完全串行的，那么串行运行的TLA+如何模拟并发算法或者分布式呢？算法？对于串行算法，算法中的动作是完全有序的，本身就是一个串行状态机，很容易构造状态图。但是，并发算法或分布式算法中的操作是部分有序的，而不是串行状态机。如何构建状态图？如果并发算法或分布式算法中的动作也能变成全序的，也可以看成是串行状态机来构造状态图。事实上，Lamport大师很早就研究了这个问题，并在他被引用次数最多的论文《Time, Clocks and the Ordering of Events in a Distributed System》中给出了分布式系统中事件排序的方法。简单来说，就是在保证具有PartiallyOrdered关系的事件顺序的前提下，人为地给剩下的无序事件设置一个顺序，让所有的事件都排序成TotallyOrdered，而且这种排序不会破坏因果关系。其实TLA+大放异彩的地方是在并发算法和分布式算法领域，因为这些领域的算法行为多种多样，容易被忽视，所以要求TLA+全面检查算法的所有路径，不遗漏任何一个行为。7.总结TLA+利用计算机强大的计算能力来搜索算法所有可能的行为，以发现意想不到的行为。随着计算机计算能力的提高和软硬件系统的复杂化，TLA+将越来越受到重视，成为工程师必备的技能。最后，如果读者对TLA+感兴趣，这里有一本关于TLA+的入门书籍《Practical TLA+》，比较适合入门，网上有免费的电子版可以直接下载。原文链接本文为阿里云原创内容，未经许可不得转载。
