简介： 女娲是飞天分布式系统中提供分布式协同的根底服务，撑持着阿里云的计算、网络、存储等简直所有云产品。在女娲分布式协同服务中，一致性引擎是外围根底模块，反对了Paxos，Raft，EPaxos等多种一致性协定，依据业务需要撑持不同业务状态机。如何保障一致性库的正确性是一个很大挑战，咱们引入了TLA+、Jepsen等工具保障一致性库的正确性。本文即从程序员视角介绍形式化验证工具TLA+。
作者 | 祥光
起源 | 阿里技术公众号
一 引言
女娲是飞天分布式系统中提供分布式协同的根底服务，撑持着阿里云的计算、网络、存储等简直所有云产品。在女娲分布式协同服务中，一致性引擎是外围根底模块，反对了Paxos，Raft，EPaxos等多种一致性协定，依据业务需要撑持不同业务状态机。如何保障一致性库的正确性是一个很大挑战，咱们引入了TLA+、Jepsen等工具保障一致性库的正确性。本文即从程序员视角介绍形式化验证工具TLA+。
从实践上证实一个程序或者算法的正确性往往是艰难的，工程中个别应用测试来发现问题，但再多的测试也无奈保障笼罩到了所有的行为，那些没笼罩到的行为就成为潜在的隐患，一旦在线上再裸露进去，往往会带来不可预期的后果。形式化验证正是为了解决这样的问题，它应用计算机弱小的计算能力，暴力的搜寻所有可能的行为，查看是否满足当时设定的属性，任何不合乎预期的行为都能被发现，从根本上保障算法的正确性。
二 TLA+简介
TLA+(Temporal Logic of Actions) 是Leslie Lamport开发的一门形式化验证语言，用于程序的设计、建模、文档和验证等，特地是并发零碎和分布式系统。TLA+的设计初衷是用简略的数学实践和公式精准地对系统进行形容。TLA+及其相干工具有助于打消程序中很难找到、纠错老本高的根本谬误。
应用TLA+对程序进行形式化验证，首先要用TLA+对程序进行形容，这样的形容称为标准(Specification)。有了Specification当前就能够应用TLC模型查看器来运行它，运行的过程会遍历所有可能的行为，查看Specification中设定的属性，发现非预期的行为。
TLA+基于数学，应用的是数学思维，与任何编程语言都不类似。为了升高TLA+的门槛，Lamport又开发了PlusCal语言，PlusCal与编程语言相似，能够很不便的形容程序逻辑，并且借用TLA+提供的工具能够间接将PlusCal翻译成TLA+。大多数工程师会发现PlusCal是开始应用TLA+的最简略办法，但简略带来的代价就是PlusCal不具备TLA+的一些性能，有时不能像TLA+那样结构简单的模型，因而PlusCal还不能取代TLA+。先应用PlusCal编程语言实现根本的逻辑，而后进一步基于生成的TLA+代码再批改，能够简化TLA+的开发。
三 TLA+利用
TLA+在学术界和工业界都有着宽泛的利用。TLA+ Examples给出了一些应用TLA+验证过的分布式算法和并发算法。在分布式算法和并发算法的钻研畛域，提出一个新的算法或者改良一个现有的算法，TLA+验证根本是标配。很多分布式算法论文在非形式化的论证介绍之外, 会附带TLA+的Specification来证实本人的算法是通过形式化验证的。对TLA+比拟相熟的业内人士来说，间接看TLA+的Specification甚至比看大段的论文了解的更快，对于论文的语言形容没有看明确，或者感觉有歧义的时候，查看TLA+的Specification对照着了解，有时候是浏览论文的一把利器，甚至有时候一些算法细节只能在TLA+的Specification里看到。因为Specification是逻辑紧密滴水不漏的，能够更好的作为实现的领导。
Lamport的TLA+主页上列出了一些TLA+在工业界的利用。以Amazon为例，Amazon AWS的一些零碎的外围算法就应用了TLA+来做形式化验证，如表1列出了TLA+给AWS的一些零碎找出的问题，其中涵盖了一些十分外围的组件，这些外围组件的问题一旦在线上裸露，造成的损失将是不可估量的。正是如此，当初分布式云服务的外围算法应用TLA+来对设计做验证曾经成为行业标准了，所以作为云服务的从业者或者对此感兴趣的同学，相熟TLA+相对是不可或缺的加分项。
表1：TLA+给AWS的零碎找出的问题
四 TLA+入门
在VS Code中装置TLA+插件就能够开始应用TLA+了。这里先以一个简略的示例入门TLA+。
思考一个单比特位的时钟，因为只有一个比特位，只能取值0或者1，其行为只有如下两种状况：
0 -> 1 -> 0 -> 1 -> 0 -> ...
1 -> 0 -> 1 -> 0 -> 1 -> ...
咱们如何用TLA+来形容这个时钟呢？为了更容易入门，先用更不便工程师入门的PlusCal来形容：
图1：单比特时钟的PlusCal形容
图1是单比特时钟的PlusCal形容，置信具备编程功底的同学都能轻易看懂。这段PlusCal代码能够间接应用TLA+提供的工具翻译成TLA+代码：
图2：单比特时钟的TLA+形容
有了下面的PlusCal的根底，了解这一段TLA+也不难，重点在于Spec的了解。Spec定义了零碎的行为，如图3形容了单比特时钟的行为，Init将clock初始化为0或1，Tick让clock在0和1之间来回跳转，Stutter让clock放弃不变。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+如何模仿并发算法或者分布式算法呢？
对于串行算法来说，算法中的动作是Totally Ordered，自身就是一个串行的状态机，很容易结构状态图。但并发算法或者分布式算法中的动作是Partially Ordered，不是一个串行的状态机，如何结构出状态图呢？
如果并发算法或者分布式算法中的动作也能变成Totally Ordered，则也能够看作是一个串行的状态机，结构出状态图。
实际上Lamport巨匠一早就钻研了这个问题，在他被援用的最多的论文《Time, Clocks and the Ordering of Events in a Distributed System》中给出了为分布式系统中的事件定序的办法。简略的说就是在保障具备Partially Ordered关系的事件的程序的前提下，将剩下的无序的事件人为定一个程序，能够将所有事件排一个序变为Totally Ordered，并且这种定序不会毁坏因果关系。
事实上TLA+大放异彩的中央正是在并发算法和分布式算法畛域，因为在这些畛域算法的行为多种多样，容易疏漏，因而须要TLA+全面查看算法的所有门路，不漏掉任何一种行为。
七 总结
TLA+应用计算机弱小的算力搜索算法所有可能的行为，以发现非预期的行为。随着计算机算力的晋升，以及软件和硬件零碎越来越简单，TLA+将越来越受到重视，越来越成为工程师的必备技能。
最初如果读者对TLA+感兴趣，这里举荐一本TLA+的入门书籍《Practical TLA+》，比拟适宜入门，并且网上有收费的电子版能够间接下载。
原文链接
本文为阿里云原创内容，未经容许不得转载。