本文旨在為沒有接觸過形式化方法的讀者提供一種新的視角看待計算機系統(tǒng)與算法，而非形式化方法或 TLA+ 教程。因此本文的重點是如何從數(shù)學角度思考程序，不會使用大篇幅講解 TLA+ 的語法。

1

我們該如何寫出正確的程序？

程序設計的目標永遠是寫出正確的程序。隨著時間的推移，我們的程序越來越復雜，其中可能存在的錯誤也越來越多。想要寫出正確的程序，首先應該了解程序中可能出現(xiàn)的錯誤有哪些。

程序中會有什么樣錯誤？

我將程序中可能出現(xiàn)的錯誤粗略地分為兩類：簡單錯誤與邏輯錯誤。

簡單錯誤

簡單錯誤包含語義錯誤、內存錯誤等。對于這些容易分析的簡單錯誤，我們已經(jīng)有很多成熟的方法與工具來避免，如編譯器、靜態(tài)分析工具、Garbage Collector 等。由于這類錯誤可以比較容易地被發(fā)現(xiàn)與修復，因此不是我們關注的重點。

邏輯錯誤

邏輯錯誤是程序中最難發(fā)現(xiàn)的錯誤，也是最難修復的錯誤，如死鎖、競態(tài)條件、數(shù)據(jù)不一致等。邏輯錯誤影響了程序的正確性、性能、可靠性等指標，通常是由于程序的設計不夠完善導致的。對于這類錯誤，我們需要從更高的層面來分析與設計程序，而非僅僅從代碼的實現(xiàn)細節(jié)來考慮。

我們通常會使用一些方法來避免邏輯錯誤，如：

• 優(yōu)化軟件架構設計- 在設計階段就考慮程序的正確性，避免設計出不夠完善的程序
• 測試- 使用各種測試方法來減少程序的錯誤，但無法保證程序的完全正確

越有經(jīng)驗的人往往能想到更多的細節(jié)與可能性，設計出的系統(tǒng)通常更穩(wěn)定。但我們不能僅僅依賴于經(jīng)驗：

• 經(jīng)驗有局限性- 人類的經(jīng)驗是有限且不可靠的
• 復雜系統(tǒng)的行為、狀態(tài)太多- 一個復雜的系統(tǒng)，其行為與狀態(tài)太多，很難通過經(jīng)驗來預測
• 特定程序對正確性的要求很高- 有些程序對正確性的要求很高，如金融系統(tǒng)、醫(yī)療系統(tǒng)等，這些程序的正確性很難通過經(jīng)驗來保證
• 無法從理論上驗證正確性- 只能盡量減少錯誤的發(fā)生，但無法從理論上證明程序的正確性

綜上，我們需要一種更加嚴謹?shù)姆椒?，從設計上保證程序的正確性。

如果能夠從數(shù)學角度驗證一個程序的正確性，就可以解決上述的問題，這就是形式化方法的目標。

形式化方法基于數(shù)學，通過為系統(tǒng)建立數(shù)學模型，來定義系統(tǒng)的行為、狀態(tài)等，然后定義系統(tǒng)的約束條件，如安全性、活性，最終證明模型滿足系統(tǒng)形式規(guī)約，來驗證系統(tǒng)的正確性。對于有窮狀態(tài)的系統(tǒng)，可以使用以窮盡搜索為基礎的模型檢測，通過搜索待驗證系統(tǒng)模型的有窮狀態(tài)空間來檢驗該系統(tǒng)的行為是否具備預期屬性。對于有無窮狀態(tài)空間的系統(tǒng)，使用邏輯推理為基礎的演繹驗證，利用歸納法驗證系統(tǒng)的正確性。

本文用 TLA+ 語言作為工具來介紹形式化方法。

2

TLA+

TLA+ 的作者是在并發(fā)和分布式系統(tǒng)領域做出開創(chuàng)性貢獻的 2013 年圖靈獎獲得者，計算機科學家 Leslie Lamport。

TLA+ 是一種用于對程序和系統(tǒng)進行建模的高級語言——尤其是并發(fā)和分布式程序和系統(tǒng)。其核心思想是：精確描述事物的最佳方式是使用簡單的數(shù)學。TLA+ 及其工具可用于消除的設計錯誤，這些錯誤很難在代碼中發(fā)現(xiàn)并且糾正起來代價高昂。

使用 TLA+ 編寫的 specification 并不是真正的工程代碼，無法用在生產(chǎn)環(huán)境中，因為 TLA+ 的目標是在系統(tǒng)設計階段就發(fā)現(xiàn)并解決邏輯錯誤。在 TLA+ 中，我們將程序抽象為有窮狀態(tài)的數(shù)學模型，通常是狀態(tài)機，然后利用 TLC Model Checker 窮盡程序所有可能到達的狀態(tài)并驗證其正確性。

下面通過兩個簡單的例子介紹 TLA+。這兩個例子均來自 TLA+ 作者的 Leslie Lamport's The TLA+ Video Course。本文的目標是為沒有接觸過形式化方法的讀者提供一種新的視角看待計算機系統(tǒng)與算法，而不是 TLA+ 教程，因此不會過多介紹 TLA+ 的語法與工具的使用。

TLA+ 可以讓我們使用簡單的數(shù)學抽象系統(tǒng)模型，主要是集合論與布爾邏輯。在抽象的過程中，我們要舍棄很多實現(xiàn)細節(jié)，僅關注程序的邏輯本身。

下面是一個簡單的 C 語言程序，我們嘗試將其抽象為一個 TLA+ 程序：

inti;
voidmain(){
i=someNumber();//someNumber()用來得到一個0到1000之間的數(shù)字
i=i+1;
}

我們需要將這個程序抽象為一個個獨立的狀態(tài)。很顯然，對于這個簡單的程序，各狀態(tài)之間的不同點只有i的值。假設i在初始化后的默認值是 0，且某次運行這個程序時someNumber()返回了 42，那么這個程序存在的狀態(tài)轉換關系就是：

[i : 0] -> [i : 42] -> [i : 43]

這之中有三個狀態(tài)，每個狀態(tài)間的區(qū)別均為i的值不同。

這樣看似完成了抽象，但是這個抽象還是有問題的。假設在另一次運行中，someNumber()返回了 43，那么這個程序的狀態(tài)轉換關系就是：

[i : 0] -> [i : 43] -> [i : 44]

這與之前的抽象不符，因為兩次運行的狀態(tài)轉換關系不同。這是因為我們沒有考慮到someNumber()的返回值。

程序的"狀態(tài)"是指程序運行完成各個階段后的時間點，而不是程序運行的過程。因此，每個狀態(tài)都是獨立的，且狀態(tài)之間的轉換都是原子的。這與傳統(tǒng)的編程有很大的區(qū)別，因為傳統(tǒng)的編程是面向過程的，而 TLA+ 是面向狀態(tài)的。我們只在乎目前程序運行到了什么狀態(tài)，因此可以引入一個變量pc來表示程序運行到了哪個階段，這樣我們就可以清晰地表示程序的次態(tài)關系：

inti;
voidmain(){
i=someNumber();//pc="start"
i=i+1;//pc="middle"
}//pc="done"

[pc : start] -> [pc : middle] -> [pc : done]

i的初始值為 0，pc的初始值為start，我們可以把次態(tài)關系寫成：

其中，對于變量i，它的下一個狀態(tài)表示為i'，這是 TLA+ 中定義變量狀態(tài)轉換的方式。i' ∈ 0..1000代表i在下一個狀態(tài)的值是 0 到 1000 之間的一個數(shù)，也就是someNumber()，0..1000代表集合{0,1,...,1000}。∧是布爾邏輯中的邏輯與，可以認為意為"并且"。最終程序運行完成，不會再有下一個狀態(tài)，因此表示為FALSE。

在 TLA+ 中，我們編寫的是一個個狀態(tài)。因此，并非是"因為pc = start所以i' ∈ 0..1000"，事實上兩者的關系是并列的：**在這個狀態(tài)中，pc的值是start并且i下一個狀態(tài)的值∈ 0..1000**。有了這樣的思想，我們可以將上面的抽象改寫為：

• EXTENDS用于引入其他 specification 中定義的 module，這里引入了標準庫中的Integers，主要用在i' ∈ 0..1000上。
• VARIABLES用于定義變量，這里定義了i和pc。
• Init用于定義初始狀態(tài)，這里定義了i = 0和pc = "start"。
• Next用于定義狀態(tài)轉換關系。

二階段提交（英語：Two-phase Commit）是指在計算機網(wǎng)絡以及數(shù)據(jù)庫領域內，為了使基于分布式系統(tǒng)架構下的所有節(jié)點在進行事務提交時保持一致性而設計的一種算法。通常，二階段提交也被稱為是一種協(xié)議（Protocol）。在分布式系統(tǒng)中，每個節(jié)點雖然可以知曉自己的操作時成功或者失敗，卻無法知道其他節(jié)點的操作的成功或失敗。當一個事務跨越多個節(jié)點時，為了保持事務的ACID特性，需要引入一個作為協(xié)調者的組件來統(tǒng)一掌控所有節(jié)點（稱作參與者）的操作結果并最終指示這些節(jié)點是否要把操作結果進行真正的提交（比如將更新后的數(shù)據(jù)寫入磁盤等等）。因此，二階段提交的算法思路可以概括為：參與者將操作成敗通知協(xié)調者，再由協(xié)調者根據(jù)所有參與者的反饋情報決定各參與者是否要提交操作還是中止操作?！?/span>Two-Phase Commit (Wikipedia)

在Leslie Lamport's The TLA+ Video Course中，Lamport 以這樣的方式類比解釋 Two-Phase Commit：

在婚禮上，牧師是協(xié)調者，新郎和新娘是參與者。當新郎和新娘都同意婚事時，牧師才會正式宣布婚事。如果有一方不同意，牧師就會中止婚事：

1. 牧師問新郎：你是否同意這件婚事？
2. 新郎回答：我同意（prepared）。
3. 牧師問新娘：你是否同意這件婚事？
4. 新娘回答：我同意（prepared）。
5. 牧師宣布：婚事正式成立（committed）。

如果其中有一方不同意，牧師就會中止（abort）婚事。

在數(shù)據(jù)庫中，Transaction Manager 是協(xié)調者（牧師）。當 Transaction Manager 詢問所有參與者 Resource Managers （新郎 / 新娘）時，如果所有 Resource Managers 都同意提交事務，Transaction Manager 就會把事務提交。如果有一方不同意，Transaction Manager 就會中止事務。

Two-Phase Commit 的詳細介紹與流程可以在Wikipedia上找到。

首先我們來定義一些常量與變量以及其初始狀態(tài)：

• 常量RM是所有 Resource Manager 標識的集合，例如可以設為集合{"r1", "r2", "r3"}。
• 變量rmState用于記錄每個 Resource Manager 的狀態(tài)，用rmState[r]表示r的狀態(tài)，有working、prepared、committed、aborted四種狀態(tài)，每個RM的初始狀態(tài)均為working。
• 變量tmState用于記錄 Transaction Manager 的狀態(tài)，有init、committed、aborted三種狀態(tài)，初始狀態(tài)為init。
• 變量tmPrepared用于記錄已經(jīng)準備好（處于prepared狀態(tài)）的 Resource Manager，初始值是一個空集。
• 變量msgs作為消息池，用于記錄所有正在傳輸?shù)南?，初始值是一個空集。

下面我們來定義系統(tǒng)做可能發(fā)生的動作。

• TLA+ 中可以用上述方式定義類似于其它編程語言中"函數(shù)"概念的表達式，這樣就無需對每一個 Resource Manager 都定義一個表達式了。
• [type → "prepare", rm → r]是一個 TLA+ 中的 record，類似于其它編程語言中的 struct。
• UNCHANGED ?rmState, tmState, msgs?表示這個動作不會改變rmState、tmState、msgs這三個變量的值。在 TLA+ 中，每一個變量的值是否改變都需要顯式地聲明。

當TM的狀態(tài)為init，且在消息池中存在來自r的Prepared消息，tmPrepared在下一個狀態(tài)的值會是tmPrepared和{r}的并集。

上述 4 個 Resource Manager 動作分別是 Resource Manager 選擇 Prepare 與 Abort，以及處理由 Transaction Manager 決定的 Commit 與 Abort。

其中，存在語法如rmState' = [rmState except ![r] = "prepared"]，意為"在下一個狀態(tài)中，rmState[r]的值變?yōu)?/span>prepared，其它部分不變"。

如果我們用形如rmState[r]' = "prepared"的形式來表示，我們并沒有顯式地說明rmState的其它部分在下一個狀態(tài)的值，因此是不正確的。

TLA+ 與我們通常編寫的程序不同，是數(shù)學。在編程中，我們會使用到數(shù)組，而在 TLA+ 中，我們使用函數(shù)來表達類似的概念，數(shù)組的下標組成的集合就是函數(shù)的定義域。

編寫完系統(tǒng)可能存在的所有動作后，我們就可以開始歸納系統(tǒng)的狀態(tài)轉換了：

其中，我們使用存在量詞?r ∈ RM來表示"對于集合RM的任意元素r，都存在這種行為"。TLA+ 的狀態(tài)轉換是原子的，因此在一個狀態(tài)中這個"或"分支內只會有一個r被選擇，這可以類比為編程語言中的for r in RM，但在本質上不同。

至此，對系統(tǒng)的建模就完成了。下面我們需要編寫系統(tǒng)的約束條件：

{
[r1|->"working",r2|->"working"],
[r1|->"working",r2|->"prepared"],
[r1|->"working",r2|->"committed"],
...
[r1|->"aborted",r2|->"committed"],
[r1|->"aborted",r2|->"aborted"]
}

{
[type|->"Prepared",rm|->r1],
[type|->"Prepared",rm|->r2],
...
}最

最后的約束條件Consistent用于保證系統(tǒng)的一致性：在任意時刻，系統(tǒng)中不可能存在兩個 Resource Managers 分別處于committed和abort狀態(tài)。

最終，我們將約束條件作為不變量，與系統(tǒng)模型一起交給 TLC Model Checker 進行驗證，就可以證明系統(tǒng)的正確性。

3

總結

4

我們的項目：Xline

TLA+被廣泛用于分布式系統(tǒng)算法的研究和開發(fā)中。在我們的項目Xline中，TLA+被用來在設計階段驗證共識算法的正確性。

Xline是一個用于元數(shù)據(jù)管理的分布式KV存儲。我們在Xline中使用CURP協(xié)議（https://www.usenix.org/system/files/nsdi19-park.pdf)的修改版作為共識協(xié)議，TLA+將被用于其正確性驗證中。

如果你想了解更多關于Xline的信息，請參考我們的Github：https://github.com/datenlord/Xline