形式化驗證工具TLA+：程式設計師視角的入門之道
簡介：女媧是飛天分散式系統中提供分散式協同的基礎服務，支撐著阿里雲的計算、網路、儲存等幾乎所有云產品。在女媧分散式協同服務中，一致性引擎是核心基礎模組，支援了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+絕對是不可或缺的加分項。
四 TLA+入門
在VS Code中安裝TLA+外掛就可以開始使用TLA+了。這裡先以一個簡單的示例入門TLA+。
考慮一個單位元位的時鐘，由於只有一個位元位，只能取值0或者1，其行為只有如下兩種情況：
0 -> 1 -> 0 -> 1 -> 0 -> ...
1 -> 0 -> 1 -> 0 -> 1 -> ...
我們如何用TLA+來描述這個時鐘呢？為了更容易入門，先用更方便工程師入門的PlusCal來描述：
圖1是單位元時鐘的PlusCal描述，相信具有程式設計功底的同學都能輕易看懂。這段PlusCal程式碼可以直接使用TLA+提供的工具翻譯成TLA+程式碼：
有了上面的PlusCal的基礎，理解這一段TLA+也不難，重點在於Spec的理解。Spec定義了系統的行為，如圖3描述了單位元時鐘的行為，Init將clock初始化為0或1，Tick讓clock在0和1之間來回跳轉，Stutter讓clock保持不變。TLA+執行的過程其實就是在圖上做遍歷。
要讓這段TLA+跑起來，上述TLA+程式碼需儲存至clock.tla檔案，此外還需要編寫一個如圖4所示的clock.cfg檔案，clock.cfg檔案內容很簡單，它註明要執行的Specification是哪個，要檢查的Invariant是哪個。
有了這兩個檔案，就可以用TLC來運行了，執行結束後得到如圖5所示的結果，圖中展示了一些統計資訊。
五 TLA+原理
為了理解TLA+的執行原理，弄清楚它是怎麼遍歷的，我們可以在執行的時候加上一些引數，讓TLC輸出狀態圖。比如我們執行圖6所示的一段TLA+程式碼，圖7是執行所需要的cfg檔案。這個例子試圖找出用面值為1、2和5的錢組合出19塊錢的所有組合方式。
執行結束後可以得到如圖8所示的狀態圖，圖中的頂點為狀態，共20種狀態，money=0為初始狀態，money=19為終止狀態，圖中的邊為動作，共4種動作：Add(1)、Add(2)、Add(5)和Terminating。
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+》，比較適合入門，並且網上有免費的電子版可以直接下載。
原文連結
本文為阿里雲原創內容，未經允許不得轉載。