网站开发与应用就业方向,网站备案是针对空间还是域名,网页设计代码模板素材,怎么健免费网站吗简介#xff1a; 女娲是飞天分布式系统中提供分布式协同的基础服务#xff0c;支撑着阿里云的计算、网络、存储等几乎所有云产品。在女娲分布式协同服务中#xff0c;一致性引擎是核心基础模块#xff0c;支持了Paxos#xff0c;Raft#xff0c;EPaxos等多种一致性协议 女娲是飞天分布式系统中提供分布式协同的基础服务支撑着阿里云的计算、网络、存储等几乎所有云产品。在女娲分布式协同服务中一致性引擎是核心基础模块支持了PaxosRaftEPaxos等多种一致性协议根据业务需求支撑不同业务状态机。如何保证一致性库的正确性是一个很大挑战我们引入了TLA、Jepsen等工具保证一致性库的正确性。本文即从程序员视角介绍形式化验证工具TLA。 作者 | 祥光 来源 | 阿里技术公众号 一 引言 女娲是飞天分布式系统中提供分布式协同的基础服务支撑着阿里云的计算、网络、存储等几乎所有云产品。在女娲分布式协同服务中一致性引擎是核心基础模块支持了PaxosRaftEPaxos等多种一致性协议根据业务需求支撑不同业务状态机。如何保证一致性库的正确性是一个很大挑战我们引入了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绝对是不可或缺的加分项。 表1TLA给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或1Tick让clock在0和1之间来回跳转Stutter让clock保持不变。TLA运行的过程其实就是在图上做遍历。 图3单比特时钟的行为 要让这段TLA跑起来上述TLA代码需保存至clock.tla文件此外还需要编写一个如图4所示的clock.cfg文件clock.cfg文件内容很简单它注明要运行的Specification是哪个要检查的Invariant是哪个。 图4clock.cfg文件内容 有了这两个文件就可以用TLC来运行了运行结束后得到如图5所示的结果图中展示了一些统计信息。 图5运行结果 五 TLA原理 为了理解TLA的运行原理弄清楚它是怎么遍历的我们可以在运行的时候加上一些参数让TLC输出状态图。比如我们运行图6所示的一段TLA代码图7是运行所需要的cfg文件。这个例子试图找出用面值为1、2和5的钱组合出19块钱的所有组合方式。 图6money.tla 图7money.cfg 运行结束后可以得到如图8所示的状态图图中的顶点为状态共20种状态money0为初始状态money19为终止状态图中的边为动作共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》比较适合入门并且网上有免费的电子版可以直接下载。 原文链接 本文为阿里云原创内容未经允许不得转载。