共计 3709 个字符,预计需要花费 10 分钟才能阅读完成。
简介:女娲是飞天分布式系统中提供分布式协同的根底服务,撑持着阿里云的计算、网络、存储等简直所有云产品。在女娲分布式协同服务中,一致性引擎是外围根底模块,反对了 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+》,比拟适宜入门,并且网上有收费的电子版能够间接下载。
原文链接
本文为阿里云原创内容,未经容许不得转载。