一  引言

女媧是飛天分布式系統中提供分布式協同的基礎服務，支撐著阿里云的計算、網絡、存儲等幾乎所有云產品。在女媧分布式協同服務中，一致性引擎是核心基礎模塊，支持了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+》，比較適合入門，并且網上有免費的電子版可以直接下載。