一  引言

女媧是飛天分布式系統(tǒng)中提供分布式協(xié)同的基礎(chǔ)服務，支撐著阿里云的計算、網(wǎng)絡(luò)、存儲等幾乎所有云產(chǎn)品。在女媧分布式協(xié)同服務中，一致性引擎是核心基礎(chǔ)模塊，支持了Paxos，Raft，EPaxos等多種一致性協(xié)議，根據(jù)業(yè)務需求支撐不同業(yè)務狀態(tài)機。如何保證一致性庫的正確性是一個很大挑戰(zhàn)，我們引入了TLA+、Jepsen等工具保證一致性庫的正確性。本文即從程序員視角介紹形式化驗證工具TLA+。

從理論上證明一個程序或者算法的正確性往往是困難的，工程中一般使用測試來發(fā)現(xiàn)問題，但再多的測試也無法保證覆蓋到了所有的行為，那些沒覆蓋到的行為就成為潛在的隱患，一旦在線上再暴露出來，往往會帶來不可預期的結(jié)果。形式化驗證正是為了解決這樣的問題，它使用計算機強大的計算能力，暴力的搜索所有可能的行為，檢查是否滿足事先設(shè)定的屬性，任何不符合預期的行為都能被發(fā)現(xiàn)，從根本上保證算法的正確性。

二  TLA+簡介

TLA+(Temporal Logic of Actions) 是Leslie Lamport開發(fā)的一門形式化驗證語言，用于程序的設(shè)計、建模、文檔和驗證等，特別是并發(fā)系統(tǒng)和分布式系統(tǒng)。TLA+的設(shè)計初衷是用簡單的數(shù)學理論和公式精準地對系統(tǒng)進行描述。TLA+及其相關(guān)工具有助于消除程序中很難找到、糾錯成本高的基本錯誤。

使用TLA+對程序進行形式化驗證，首先要用TLA+對程序進行描述，這樣的描述稱為規(guī)范(Specification)。有了Specification以后就可以使用TLC模型檢查器來運行它，運行的過程會遍歷所有可能的行為，檢查Specification中設(shè)定的屬性，發(fā)現(xiàn)非預期的行為。

TLA+基于數(shù)學，使用的是數(shù)學思維，與任何編程語言都不相似。為了降低TLA+的門檻，Lamport又開發(fā)了PlusCal語言，PlusCal與編程語言類似，可以很方便的描述程序邏輯，并且借用TLA+提供的工具可以直接將PlusCal翻譯成TLA+。大多數(shù)工程師會發(fā)現(xiàn)PlusCal是開始使用TLA+的最簡單方法，但簡單帶來的代價就是PlusCal不具備TLA+的一些功能，有時不能像TLA+那樣構(gòu)造復雜的模型，因此PlusCal還不能取代TLA+。先使用PlusCal編程語言完成基本的邏輯，然后進一步基于生成的TLA+代碼再修改，可以簡化TLA+的開發(fā)。

三  TLA+應用

TLA+在學術(shù)界和工業(yè)界都有著廣泛的應用。TLA+ Examples給出了一些使用TLA+驗證過的分布式算法和并發(fā)算法。在分布式算法和并發(fā)算法的研究領(lǐng)域，提出一個新的算法或者改進一個現(xiàn)有的算法，TLA+驗證基本是標配。很多分布式算法論文在非形式化的論證介紹之外, 會附帶TLA+的Specification來證明自己的算法是經(jīng)過形式化驗證的。對TLA+比較熟悉的業(yè)內(nèi)人士來說，直接看TLA+的Specification甚至比看大段的論文理解的更快，對于論文的語言描述沒有看明白，或者覺得有歧義的時候，查看TLA+的Specification對照著理解，有時候是閱讀論文的一把利器，甚至有時候一些算法細節(jié)只能在TLA+的Specification里看到。由于Specification是邏輯嚴密滴水不漏的，可以更好的作為實現(xiàn)的指導。

Lamport的TLA+主頁上列出了一些TLA+在工業(yè)界的應用。以Amazon為例，Amazon AWS的一些系統(tǒng)的核心算法就使用了TLA+來做形式化驗證，如表1列出了TLA+給AWS的一些系統(tǒng)找出的問題，其中涵蓋了一些非常核心的組件，這些核心組件的問題一旦在線上暴露，造成的損失將是不可估量的。正是如此，現(xiàn)在分布式云服務的核心算法使用TLA+來對設(shè)計做驗證已經(jīng)成為行業(yè)標準了，所以作為云服務的從業(yè)者或者對此感興趣的同學，熟悉TLA+絕對是不可或缺的加分項。

表1：TLA+給AWS的系統(tǒng)找出的問題

四  TLA+入門

在VS Code中安裝TLA+插件就可以開始使用TLA+了。這里先以一個簡單的示例入門TLA+。

考慮一個單比特位的時鐘，由于只有一個比特位，只能取值0或者1，其行為只有如下兩種情況：

0 -> 1 -> 0 -> 1 -> 0 -> ...

1 -> 0 -> 1 -> 0 -> 1 -> ...

我們?nèi)绾斡肨LA+來描述這個時鐘呢？為了更容易入門，先用更方便工程師入門的PlusCal來描述：

圖1：單比特時鐘的PlusCal描述

圖1是單比特時鐘的PlusCal描述，相信具有編程功底的同學都能輕易看懂。這段PlusCal代碼可以直接使用TLA+提供的工具翻譯成TLA+代碼：

圖2：單比特時鐘的TLA+描述

有了上面的PlusCal的基礎(chǔ)，理解這一段TLA+也不難，重點在于Spec的理解。Spec定義了系統(tǒng)的行為，如圖3描述了單比特時鐘的行為，Init將clock初始化為0或1，Tick讓clock在0和1之間來回跳轉(zhuǎn)，Stutter讓clock保持不變。TLA+運行的過程其實就是在圖上做遍歷。

圖3：單比特時鐘的行為

要讓這段TLA+跑起來，上述TLA+代碼需保存至clock.tla文件，此外還需要編寫一個如圖4所示的clock.cfg文件，clock.cfg文件內(nèi)容很簡單，它注明要運行的Specification是哪個，要檢查的Invariant是哪個。

圖4：clock.cfg文件內(nèi)容

有了這兩個文件，就可以用TLC來運行了，運行結(jié)束后得到如圖5所示的結(jié)果，圖中展示了一些統(tǒng)計信息。

圖5：運行結(jié)果 

五  TLA+原理

為了理解TLA+的運行原理，弄清楚它是怎么遍歷的，我們可以在運行的時候加上一些參數(shù)，讓TLC輸出狀態(tài)圖。比如我們運行圖6所示的一段TLA+代碼，圖7是運行所需要的cfg文件。這個例子試圖找出用面值為1、2和5的錢組合出19塊錢的所有組合方式。

圖6：money.tla

圖7：money.cfg

運行結(jié)束后可以得到如圖8所示的狀態(tài)圖，圖中的頂點為狀態(tài)，共20種狀態(tài)，money=0為初始狀態(tài)，money=19為終止狀態(tài)，圖中的邊為動作，共4種動作：Add(1)、Add(2)、Add(5)和Terminating。

圖8：狀態(tài)圖

TLA+的運行是完全串行的，運行的的過程即在狀態(tài)圖上做圖的遍歷，每遍歷到一個狀態(tài)，就檢查一下當前狀態(tài)是否滿足事先設(shè)定的不變式，滿足則繼續(xù)遍歷，不滿足則立即報錯。TLA+會嘗試所有的遍歷路徑，不錯過任何一種行為。我們知道圖的遍歷方式有深度優(yōu)先和廣度優(yōu)先兩種，TLA+默認廣度優(yōu)先遍歷，也可配置成深度優(yōu)先模式或者隨機行為模式，深度優(yōu)先模式需要給定一個最大深度。

現(xiàn)在我們知道了TLA+的原理實際上就是狀態(tài)圖的遍歷并檢查的過程，這樣的過程看似簡單，卻能覆蓋到算法所有的路徑，不漏掉任何一種行為。實際我們經(jīng)常使用TLA+檢查算法的Safety和Liveness屬性。

六  TLA+并發(fā)

到這里相信讀者對TLA+的原理已經(jīng)有了初步的了解，但細心的讀者可能心中還有一個很大的疑問：TLA+運行過程是完全串行的，那么串行運行的TLA+如何模擬并發(fā)算法或者分布式算法呢？

對于串行算法來說，算法中的動作是Totally Ordered，本身就是一個串行的狀態(tài)機，很容易構(gòu)造狀態(tài)圖。但并發(fā)算法或者分布式算法中的動作是Partially Ordered，不是一個串行的狀態(tài)機，如何構(gòu)造出狀態(tài)圖呢？

如果并發(fā)算法或者分布式算法中的動作也能變成Totally Ordered，則也可以看作是一個串行的狀態(tài)機，構(gòu)造出狀態(tài)圖。

實際上Lamport大師一早就研究了這個問題，在他被引用的最多的論文《Time, Clocks and the Ordering of Events in a Distributed System》中給出了為分布式系統(tǒng)中的事件定序的方法。簡單的說就是在保證具有Partially Ordered關(guān)系的事件的順序的前提下，將剩下的無序的事件人為定一個順序，可以將所有事件排一個序變?yōu)門otally Ordered，并且這種定序不會破壞因果關(guān)系。

事實上TLA+大放異彩的地方正是在并發(fā)算法和分布式算法領(lǐng)域，因為在這些領(lǐng)域算法的行為多種多樣，容易疏漏，因此需要TLA+全面檢查算法的所有路徑，不漏掉任何一種行為。

七  總結(jié)

TLA+使用計算機強大的算力搜索算法所有可能的行為，以發(fā)現(xiàn)非預期的行為。隨著計算機算力的提升，以及軟件和硬件系統(tǒng)越來越復雜，TLA+將越來越受到重視，越來越成為工程師的必備技能。

最后如果讀者對TLA+感興趣，這里推薦一本TLA+的入門書籍《Practical TLA+》，比較適合入門，并且網(wǎng)上有免費的電子版可以直接下載。