Writing is nature's way of letting you know how sloppy your thinking is - Guindon

在2024年6月份舉辦的GopherCon Europe Berlin 2024[1]上，一個叫Raghav Roy的印度程序員(聽口音判斷的)分享了Using Formal Reasoning to Build Concurrent Go Systems[2]，介紹了如何使用形式化驗證工具TLA+[3]來驗證Go并發(fā)程序的設(shè)計正確性。

TLA+是2013年圖靈獎獲得者、美國計算機(jī)科學(xué)家和數(shù)學(xué)家、分布式系統(tǒng)奠基性大神、Paxos算法[4]和Latex[5]的締造者Leslie B. Lamport[6]設(shè)計的一種針對數(shù)字系統(tǒng)(Digital Systems)的高級(high-level)建模語言，TLA+誕生于1999年，一直低調(diào)演進(jìn)至今。

TLA+不僅可以對系統(tǒng)建模，還可以與模型驗證工具，比如：TLC model checker，結(jié)合使用，對被建模系統(tǒng)的行為進(jìn)行全面的驗證。我們可以將TLA+看成一種專門用于數(shù)字系統(tǒng)建模和驗證的DSL語言[7]。

注：TLA是Temporal Logic of Actions的首字母縮寫，Temporal Logic[8]，即時序邏輯，是一種用于描述和推理系統(tǒng)行為隨時間變化的邏輯框架，由Arthur Prior在1950年代后期引入邏輯學(xué)。在后面對TLA+的進(jìn)一步介紹中，大家可能就會逐漸理解為什么Lamport給這門語言命名為TLA+了。

這不是我第一次接觸TLA+，去年就花過一些時間了解過TLA+的資料，可能是因為姿勢不夠正確，沒有在本博客留下只言片語，而這次我打算寫點(diǎn)有關(guān)TLA+的東西。

1. 為什么需要TLA+

從1999年Lamport發(fā)表的論文“Specifying Concurrent Systems with TLA+[9]”以及他2014年在微軟的演講“Thinking Above the Code[10]”中 ，我們大致可以得到Lamport在20多年前設(shè)計TLA+的樸素的動機(jī)：**期望程序員能像科學(xué)家一樣思考，在編碼之前用一種精確的形式化的語言寫出目標(biāo)系統(tǒng)的spec，這個過程類似于建筑架構(gòu)師在建筑施工之前編制建筑的藍(lán)圖(blueprint)**。

為什么要編寫目標(biāo)系統(tǒng)的spec呢？

綜合來自Lamport的相關(guān)資料，大致可以梳理出以下兩點(diǎn)：

• 從程序員的角度來看，在開始編碼之前，先在抽象的層面思考系統(tǒng)行為，而不是過早地陷入編程語言的具體語法中。并且先寫下規(guī)格說明，可以幫助程序員明確需求，認(rèn)知系統(tǒng)，發(fā)現(xiàn)潛在問題，并為后續(xù)的編碼和維護(hù)提供指導(dǎo)。
• 從系統(tǒng)復(fù)雜性的角度來看，對于日益復(fù)雜的并發(fā)和分布式系統(tǒng)，僅靠直覺思考很難保證正確性，傳統(tǒng)的測試方法也已經(jīng)不足以發(fā)現(xiàn)所有問題。這時候?qū)憇pec(規(guī)格說明)并用配套的檢查工具進(jìn)行驗證就變得非常必要。

那為什么要新設(shè)計TLA+來寫spec呢，而不是使用像C++這類編程語言，或是其他已存在的形式化語言來編寫spec呢？

Lamport給出的理由有以下幾個：

• 編程語言的局限性：像C++這樣的編程語言主要是為了實現(xiàn)而設(shè)計的，而不是為了spec。它們往往過于關(guān)注實現(xiàn)細(xì)節(jié)，而不是高層次的系統(tǒng)行為，缺乏描述并發(fā)和分布式系統(tǒng)所需的抽象能力，不適合表達(dá)系統(tǒng)的時序性質(zhì)和不變量。
• 已有形式化語言的不足：當(dāng)時存在的其他形式化語言大多存在要么過于學(xué)術(shù)化，難以在實際工程中應(yīng)用，要么難以自然地表達(dá)并發(fā)和分布式系統(tǒng)的特性等問題；并且缺少工具支持，不具備spec驗證功能。
• 數(shù)學(xué)建模的局限：純粹的數(shù)學(xué)公式雖然精確，但對非數(shù)學(xué)背景的工程師來說難以理解和使用，缺乏工具支持，難以自動化驗證，難以直接映射到系統(tǒng)設(shè)計和實現(xiàn)。

Lamport設(shè)計的TLA+是建立在堅實的數(shù)學(xué)基礎(chǔ)之上，這使得它能夠支持嚴(yán)格的數(shù)學(xué)推理和證明與自動化驗證工具（如TLC模型檢查器）無縫集成。TLA+被設(shè)計為在高度抽象的層面描述系統(tǒng)，不會像編程語言那樣受實現(xiàn)細(xì)節(jié)的束縛。此外，結(jié)合時序邏輯和狀態(tài)機(jī)，TLA+可以描述并發(fā)和分布式系統(tǒng)，并在設(shè)計層面驗證系統(tǒng)的正確性。

根據(jù)Lamport的不完全統(tǒng)計[11]，TLA+在Intel、Amazon、Microsoft等大廠都有應(yīng)用，一些知名的算法以及開源項目也使用TLA+進(jìn)行了形式化驗證，比如Raft算法的作者就給出了Raft算法的TLA+ spec[12]，國內(nèi)分布式數(shù)據(jù)庫廠商pingcap也在項目中使用TLA+對raft算法以及分布式事務(wù)做了形式化的驗證[13]。

在這些應(yīng)用案例中，AWS的案例是典型代表。AWS也將應(yīng)用TLA+過程中積累的經(jīng)驗以paper的形式發(fā)表了，其論文集合[14]也被Lamport放置在其個人主頁上了。從這些論文內(nèi)容來看，AWS對TLA+的評價是很正面的：AWS使用TLA+對10個大型復(fù)雜的真實系統(tǒng)進(jìn)行建模和驗證，的確發(fā)現(xiàn)了多個難以通過其他方法發(fā)現(xiàn)的微妙錯誤。同時，通過精確描述設(shè)計，TLA+迫使工程師更清晰地思考，消除了“看似合理的含糊之處”。此外，AWS工程師認(rèn)為TLA+ spec也是一種很好的文檔形式，可以提供精確、簡潔、可測試的設(shè)計描述，有助于新人快速理解系統(tǒng)。

鋪墊了這么多，TLA+究竟是什么？它是如何在高級抽象層面對分布式系統(tǒng)和并發(fā)系統(tǒng)進(jìn)行描述和驗證的？接下來，我們就來看一下。

2. Lamport對TLA+的定義

在Lamport的論文、書籍以及一些演講資料中，他是這么定義TLA+的：A language for high-level modeling digital systems。對于這個定義，我們可以“分段”來理解一下。

• Digital System

什么是TLA+眼中的數(shù)字系統(tǒng)(Digital System)？Lamport認(rèn)為數(shù)字系統(tǒng)包括算法(Algorithms)、程序(Programs)和計算機(jī)系統(tǒng)(Computer system)，它們有一個共同特點(diǎn)，那就是可以抽象為一個按離散事件序列(sequence of discrete events)進(jìn)行持續(xù)執(zhí)行和演進(jìn)的物理系統(tǒng)，這是TLA+后續(xù)描述(specify)數(shù)字系統(tǒng)的基礎(chǔ)。隨著多核和云計算的興起，并發(fā)程序和分布式的關(guān)鍵(critical)系統(tǒng)成為了TLA+的主要描述對象，這樣的系統(tǒng)最復(fù)雜，最難正確實現(xiàn)，價值也最高，值得使用TLA+對其進(jìn)行形式化的驗證。

• High Level

TLA+面向設(shè)計層面，在代碼實現(xiàn)層面之上，實施于編寫任何實現(xiàn)代碼之前。此外，High Level也意味著可以忽略那些系統(tǒng)中不是很關(guān)鍵(less-critical)的部分以及低層次的實現(xiàn)細(xì)節(jié)。

去除細(xì)節(jié)進(jìn)行簡化的過程就是抽象（Abstraction），它是工程領(lǐng)域最重要的環(huán)節(jié)。抽象可以讓我們理解復(fù)雜的系統(tǒng)，如果不了解系統(tǒng)，我們就無法對系統(tǒng)進(jìn)行正確的建模并實現(xiàn)它。

而使用TLA+編寫系統(tǒng)spec其實就是一個學(xué)習(xí)對系統(tǒng)進(jìn)行抽象的過程，學(xué)會抽象思考，可以幫助工程師提高設(shè)計能力。

• Modeling

TLA+是通過描述系統(tǒng)的行為(behavior)來對數(shù)字系統(tǒng)進(jìn)行建模的。那么什么是系統(tǒng)的行為呢？如下圖所示：

此圖由claude sonnet 3.5根據(jù)我的prompt生成

行為被Lamport定義為一系列的狀態(tài)（Sequence of States），這些狀態(tài)仍然按順序排列，表示系統(tǒng)隨時間的演變。而狀態(tài)本身則是對變量的賦值。狀態(tài)之間的轉(zhuǎn)換由動作(action)描述，而系統(tǒng)的正確性由屬性(properties)指定。

這種方法特別適合建模并發(fā)和分布式系統(tǒng)，因為它允許我們精確地描述系統(tǒng)的所有可能行為，包括不同組件之間的交互和可能的競爭條件，如下圖所示：

圖片

在TLA+中，屬性(properties)是用來描述系統(tǒng)應(yīng)該滿足的條件或特性，它們在驗證系統(tǒng)行為的正確性方面起著關(guān)鍵作用。我們所說的系統(tǒng)工作正常就是指這些在執(zhí)行過程中的屬性都得到了滿足。

在TLA+中，有兩類屬性是我們特別需要關(guān)注的，一類是安全屬性（Safety Properties），一類則是活性屬性（Liveness Properties）。前者確?！皦氖掠肋h(yuǎn)不會發(fā)生”，比如使用不變量在并發(fā)系統(tǒng)中確保兩個進(jìn)程不會同時進(jìn)入臨界區(qū)；后者則是確保“好事最終會發(fā)生”，在分布式系統(tǒng)中的最終一致性（eventual consistency）是一個活性屬性，它保證系統(tǒng)最終會達(dá)到一致的狀態(tài)。TLA+允許我們精確地指定這些屬性，然后使用TLC模型檢查器來驗證系統(tǒng)是否滿足這些屬性。這種方法特別適合于復(fù)雜的并發(fā)和分布式系統(tǒng)，因為它能夠發(fā)現(xiàn)在傳統(tǒng)測試中難以發(fā)現(xiàn)的微妙錯誤。

注：關(guān)于TLA+可以用來形式化描述(specify)和驗證(check)數(shù)字系統(tǒng)的底層數(shù)學(xué)理論，可以參考Lamport老爺子那本最新尚未完成的書籍A Science of Concurrent Programs(2024.6.7版)[15]。

接下來，我們就來看看TLA+究竟如何編寫。不過直接介紹TLA+語法比較抽象和枯燥，在我讀過的TLA+語法資料中，Lamport在The TLA+ Video Course[16]第二講中將一個C示例程序一步一步像數(shù)學(xué)推導(dǎo)一樣轉(zhuǎn)換為TLA+語法的講解對我?guī)椭浅４?，我覺得有必要將這個示例放到這篇文章中。

3. 從C代碼到TLA+：轉(zhuǎn)換步驟詳解

Lamport的這個過程展示了如何從一個具體的編程語言實現(xiàn)(以C代碼為例)逐步抽象到一個數(shù)學(xué)化的、更加通用的系統(tǒng)描述。每一步都增加了抽象級別，最終得到一個可以用于形式化驗證的TLA+規(guī)范(spec)。以下是這個演進(jìn)過程的主要階段：

3.1 初始C程序分析

下面是這個示例的原始C代碼：

int i;
void main() {
    i = someNumber();
    i = i + 1;
}

這不是一個并發(fā)程序，它只有一個執(zhí)行路線(execution)，前面說過，一個行為(execution)是一個狀態(tài)序列，我們就來定義這個狀態(tài)序列以及它們之間的轉(zhuǎn)換關(guān)系。

我們先識別出程序的狀態(tài)變量：i以及引入的控制狀態(tài)變量（PC），PC變量來表示程序的執(zhí)行位置。接下來我們就來描述一個可以代碼該程序所有狀態(tài)的“狀態(tài)機(jī)”。

3.2 狀態(tài)機(jī)描述

該程序可以劃分為三個狀態(tài)：

• 初始狀態(tài)：i = 0, PC = "start"
• 中間狀態(tài)：i in {0, 1, ..., 1000}(這里限定了someNumber函數(shù)返回的數(shù)值范圍), PC = "middle"
• 結(jié)束狀態(tài)：i = i + 1, PC = "done"

下面用自然語言描述一下上述狀態(tài)的轉(zhuǎn)換關(guān)系：

if current value of pc equals "start"
    then next value of i in {0, 1, ..., 1000}
         next value of pc equals "middle"
    else if current value of pc equals "middle"
            then next value of i equals current value of i + 1 
                 next value of pc equals "done"
            else no next values

接下來，我們就來將上述對于狀態(tài)轉(zhuǎn)換的描述變換一下，盡量用數(shù)學(xué)來表示。

3.3 轉(zhuǎn)換為數(shù)學(xué)表示

這里的轉(zhuǎn)換分為幾步，我們逐一來看。

• 換掉"current value of"

if pc equals "start"
    then next value of i in {0, 1, ..., 1000}
         next value of pc equals "middle"
    else if pc equals "middle"
            then next value of i equals i + 1 
                 next value of pc equals "done"
            else no next values

替換后，pc即the current value of pc，i即current value of i。

• 換掉"next value of"

我們用i'換掉"next value of i", 用pc'換掉"next value of pc"，結(jié)果如下：

if pc equals "start"
    then i' in {0, 1, ..., 1000}
         pc' equals "middle"
    else if pc equals "middle"
            then i' equals i + 1 
                 pc' equals "done"
            else no next values

• 用"="符號換掉equals

替換的結(jié)果如下：

if pc = "start"
    then i' in {0, 1, ..., 1000}
         pc' = "middle"
    else if pc = "middle"
            then i' = i + 1 
                 pc' = "done"
            else no next values

• 將in換為數(shù)學(xué)符號∈

if pc = "start"
    then i' ∈ {0, 1, ..., 1000}
         pc' = "middle"
    else if pc = "middle"
            then i' = i + 1
                 pc' = "done"
            else no next values

3.4 TLA+語法轉(zhuǎn)換

• 將集合表示換為正式的數(shù)學(xué)符號

{0, 1, ..., 1000}并非數(shù)學(xué)表示集合的方式，替換后，結(jié)果如下：

if pc = "start"
    then i' ∈ 0..1000
         pc' = "middle"
    else if pc = "middle"
            then i' = i + 1
                 pc' = "done"
            else no next values

這里0..1000使用了TLA+的集合表示語法。

• 轉(zhuǎn)換為單一公式(formula)

將C代碼轉(zhuǎn)換為上面的最新代碼后，你不要再按照C的語義去理解上述轉(zhuǎn)換后的代碼了。新代碼并非是像C那樣為了進(jìn)行好一些計算而編寫的一些指令，新代碼是一個關(guān)于i、pc、i'和pc'的公式(formula)，這是理解從C帶TLA+的最為關(guān)鍵的環(huán)節(jié)，即上述這段代碼整體就是一個公式！

上述代碼的意思并非if pc = "start"為真，然后執(zhí)行then部分，否則執(zhí)行else部分。其真正含義是如果pc = "start"為真，那么上述整個公式將等于then這個公式的值，否則整個公式將等于else公式的值。

不過我們看到在上面的then子句中存在兩個獨(dú)立的公式，以第一個then為例，兩個獨(dú)立公式分別為i' ∈ 0..1000和pc' = "middle"。這兩個獨(dú)立的公式之間是and的關(guān)系，我們需要將其轉(zhuǎn)換為一個公式。TLA+中使用"/"表示and連接，下面是使用"/"將公式連接后的結(jié)果：

if pc = "start"
    then (i' ∈ 0..1000) /\
         (pc' = "middle")
    else if pc = "middle"
            then (i' = i + 1) /\
                 (pc' = "done")
            else no next values

• 改造else公式

問題來了! 當(dāng)存在某個狀態(tài)，使得整個公式等于最后一個else公式的值時，我們發(fā)現(xiàn)這個值為"no next values"，而前面的then、else if then公式的值都為布爾值TRUE或FALSE。這里最后的ELSE公式，它的值應(yīng)該為FALSE，無論i、pc、i'和pc'的值為什么，因此這里直接將其改造為FALSE：

if pc = "start"
    then (i' ∈ 0..1000) /\
         (pc' = "middle")
    else if pc = "middle"
            then (i' = i + 1) /\
                 (pc' = "done")
            else FALSE

• TLA+的關(guān)鍵字為大寫且TLA+源碼為ASCII碼

if、then、else 這些都是TLA+的關(guān)鍵字，而TLA+的關(guān)鍵字通常為大寫，并且TLA+源碼為ASCII碼，∈需換成\in。這樣改變后的結(jié)果如下：

IF pc = "start"
    THEN (i' \in 0..1000) /\
         (pc' = "middle")
    ELSE IF pc = "middle"
            THEN (i' = i + 1) /\
                 (pc' = "done")
            ELSE FALSE

到這里，我們就得到了一個美化后的的TLA+公式了!

3.5 干掉if else

前面說過，我們將C代碼改造為了一個公式，但公式中依然有if else總是感覺有些格格不入，是不是可以干掉if else呢！我們來試一下！

我們先用A、B替換掉then語句中的兩個公式:

IF pc = "start"
    THEN A
    ELSE IF pc = "middle"
            THEN B
            ELSE FALSE

如果整個公式為TRUE，需要(pc = "start")和A都為TRUE，或(pc = "middle")和B都為TRUE。TLA+引入一個操作符/表示or，這樣整個公式為TRUE的邏輯就可以表示為：

((pc = "start") /\ A) 
\/ ((pc = "middle") /\ B)

好了，現(xiàn)在我們再把A和B換回到原先的公式：

((pc = "start") /\  
    (i' \in 0..1000) /\
    (pc' = "middle"))
\/ ((pc = "middle") /\ 
    (i' = i+1 ) /\
    (pc' = "done"))

你是不是感覺不夠美觀??！TLA+提供了下面等價的、更美觀的形式：

\/ /\ pc = "start"
   /\ i' \in 0..1000
   /\ pc' = "middle"
\/ /\ pc = "middle"
   /\ i' = i+1 
   /\ pc' = "done"

這種形式完全去掉了括號，并可以像列表一樣表達(dá)公式！并且無論是/\還是/都是可交換的(commutative)，順序不影響公式的最終結(jié)果。

3.6 完整的TLA+ spec

從數(shù)學(xué)層面，上面C代碼將被拆分為兩個公式，一個是初始狀態(tài)公式，一個是下個狀態(tài)的公式：

初始狀態(tài)公式：(i = 0) /\ (pc = "start")
下一狀態(tài)公式：
              \/ /\ pc = "start"
                 /\ i' \in 0..1000
                 /\ pc' = "middle"
              \/ /\ pc = "middle"
                 /\ i' = i+1 
                 /\ pc' = "done"

但對于一個完整的TLA+ spec來說，還需要額外補(bǔ)充些內(nèi)容：

---- MODULE SimpleProgram ----

EXTENDS Integers
VARIABLES i, pc

Init == (pc = "start") /\ (i = 0)
Next == \/ /\ pc = "start"
           /\ i' \in 0..1000
           /\ pc' = "middle"
        \/ /\ pc = "middle"
           /\ i' = i + 1
           /\ pc' = "done"
====

一個完整的TLA+ spec是放在一個module中的，上面例子中module為SimpleProgram。TLA toolkit要求tla文件名要與module名相同，這樣上面代碼對應(yīng)的tla文件應(yīng)為SimpleProgram.tla。

EXTENDS會導(dǎo)入TLA+內(nèi)置的標(biāo)準(zhǔn)module，這里的Integers就提供了基礎(chǔ)的算術(shù)運(yùn)算符，比如+和..。

VARIABLES聲明了狀態(tài)變量，比如這里的i和pc。變量加上'即表示該變量的下一個狀態(tài)的值。

接下來便是公式的定義。Init和Next并非固定公式名字，你可以選擇任意名字，但使用Init和Next是慣用法。

"===="用于標(biāo)識一個module的Body內(nèi)容的結(jié)束。

對于上面簡單的C程序，這樣的spec是可以的。但在實際使用中，spec中的Next一般會很長，一個好的實踐是對其進(jìn)行拆分。比如這里我們就將Next拆分為兩個子公式：Pick和Add1：

---- MODULE SimpleProgram ----

EXTENDS Integers
VARIABLES i, pc

Init == (pc = "start") /\ (i = 0)
Pick == /\ pc = "start"
        /\ i' \in 0..1000
        /\ pc' = "middle"
Add1 == /\ pc = "middle"
        /\ i' = i + 1
        /\ pc' = "done"
Next == Pick \/ Add1
====

4. 使用TLA+ Toolkit驗證spec

Lamport提供了TLA+的Module Checker，我們可以從其主頁提供的工具包下載鏈接[17]下載TLA+ Toolkit。

先將上面的TLA+ spec存入一個名為SimpleProgram.tla的文件。然后打開TLA+ Toolkit，選擇File -> Open spec -> Add New Spec...，然后選擇你本地的SimpleProgram.tla即可加載該spec：

圖片

之后，我們可以點(diǎn)擊菜單項“TLC Model Checker” -> New Model，便可以為該tla建立一個model配置(去掉deadlock)，運(yùn)行check后，你能看到下面結(jié)果：

圖片

我們看到model check一共檢查了2003個不同的狀態(tài)。

注：TLA+還提供了一個Visual Studio Code的擴(kuò)展[18]，也可以用來specify和check model。

5. 使用TLA+驗證Go并發(fā)程序

Go語言因其強(qiáng)大的并發(fā)編程能力而備受青睞。然而，Go的并發(fā)方案雖然簡單，但也并非銀彈。隨著并發(fā)程序復(fù)雜性的增加，開發(fā)者常常面臨著難以發(fā)現(xiàn)和調(diào)試的錯誤，如死鎖和競態(tài)條件。這些問題不僅影響程序的正確性，還可能導(dǎo)致嚴(yán)重的系統(tǒng)故障。對于Go開發(fā)的并發(fā)系統(tǒng)的關(guān)鍵部分，采用TLA+進(jìn)行形式化的驗證是一個不錯的提高系統(tǒng)正確性和可靠性的方法。

接下來，我們就建立一個生產(chǎn)者和消費(fèi)者的Go示例，然后使用TLA+為其建模并check。理論上應(yīng)該是先有設(shè)計思路，再TLA+驗證設(shè)計，再進(jìn)行代碼實現(xiàn)，這里的Go代碼主要是為了“描述”該并發(fā)程序的需求和行為邏輯。

// go-and-tla-plus/producer-consumer/main.go
package main

import (
 "fmt"
 "sync"
)

func producer(ch chan<- int, wg *sync.WaitGroup) {
 defer wg.Done()
 for i := 0; i < 5; i++ {
  ch <- i
 }
 close(ch)
}

func consumer(ch <-chan int, wg *sync.WaitGroup) {
 defer wg.Done()
 for num := range ch {
  fmt.Println("Consumed:", num)
 }
}

func main() {
 ch := make(chan int)
 var wg sync.WaitGroup
 wg.Add(2)

 go producer(ch, &wg)
 go consumer(ch, &wg)

 wg.Wait()
}

任何Go初學(xué)者都可以很容易讀懂上面的程序邏輯：Producer生產(chǎn)0到4四個數(shù)，每生成一個就通過unbuffered channel發(fā)出，consumer從channel接收數(shù)字并消費(fèi)。Producer生產(chǎn)完畢后，關(guān)閉channel。Consumer消費(fèi)完所有數(shù)字后，退出，程序終止。

下面是使用TLA+編寫的ProducerConsumer的完整Spec：

// go-and-tla-plus/producer-consumer/ProducerConsumer.tla

---- MODULE ProducerConsumer ----
EXTENDS Integers, Sequences

VARIABLES 
    ch,           \* 通道內(nèi)容
    produced,     \* 已生產(chǎn)的消息數(shù)
    consumed,     \* 已消費(fèi)的消息數(shù)
    closed        \* 通道是否關(guān)閉

TypeOK ==
    /\ ch \in Seq(0..4)
    /\ produced \in 0..5
    /\ consumed \in 0..5
    /\ closed \in BOOLEAN

Init ==
    /\ ch = <<>>
    /\ produced = 0
    /\ consumed = 0
    /\ closed = FALSE

Produce ==
    /\ produced < 5
    /\ ch = <<>>
    /\ ~closed
    /\ ch' = Append(ch, produced)
    /\ produced' = produced + 1
    /\ UNCHANGED <<consumed, closed>>

Close ==
    /\ produced = 5
    /\ ch = <<>>
    /\ ~closed
    /\ closed' = TRUE
    /\ UNCHANGED <<ch, produced, consumed>>

Consume ==
    /\ ch /= <<>>
    /\ ch' = Tail(ch)
    /\ consumed' = consumed + 1
    /\ UNCHANGED <<produced, closed>>

Next ==
    \/ Produce
    \/ Close
    \/ Consume

Fairness ==
    /\ SF_<<ch, produced, closed>>(Produce)
    /\ SF_<<produced, closed>>(Close)
    /\ SF_<<ch>>(Consume)

Spec == Init /\ [][Next]_<<ch, produced, consumed, closed>> /\ Fairness

THEOREM Spec => []TypeOK

ChannelEventuallyEmpty == <>(ch = <<>>)
AllMessagesProduced == <>(produced = 5)
ChannelEventuallyClosed == <>(closed = TRUE)
AllMessagesConsumed == <>(consumed = 5)

====

這個Spec不算長，但也不短，你可能看不大懂，沒關(guān)系，接下來我們就來說說從main.go到ProducerConsumer.tla的建模過程，并重點(diǎn)解釋一下上述TLA+代碼中的重要語法。

針對main.go中體現(xiàn)出來的Producer和Consumer的邏輯，我們首先需要識別關(guān)鍵組件：生產(chǎn)者、消費(fèi)者和一個通道(channel)，然后我們需要確定狀態(tài)變量，包括：通道內(nèi)容(ch)、已生產(chǎn)消息數(shù)(produced)、已消費(fèi)消息數(shù)(consumed)、通道是否關(guān)閉(closed)。

接下來，我們就要定義action，即導(dǎo)致狀態(tài)變化的step，包括Produce、Consume和Close。

最后，我們需要設(shè)置初始狀態(tài)Init和下一個狀態(tài)Next，并定義安全屬性(TypeOK)和一些活性屬性(如AllMessagesConsumed等)

現(xiàn)在，我們結(jié)合上述TLA+的代碼，來說一下上述這些邏輯是如何在TLA+中實現(xiàn)的：

---- MODULE ProducerConsumer ----

這一行定義了模塊名稱，模塊名稱與文件名字(ProducerConsumer.tla)要一致，否則TLA+ Toolkit在Open Spec時會報錯。

EXTENDS Integers, Sequences

這行會導(dǎo)入整數(shù)和序列模塊，以使用相關(guān)運(yùn)算符。

VARIABLES 
    ch,           \* 通道內(nèi)容
    produced,     \* 已生產(chǎn)的消息數(shù)
    consumed,     \* 已消費(fèi)的消息數(shù)
    closed        \* 通道是否關(guān)閉

這里使用VARIBALES關(guān)鍵字定義了四個狀態(tài)變量，整個TLA+程序的函數(shù)邏輯就圍繞這四個變量進(jìn)行，TLC Model check也是基于這些狀態(tài)變量對TLA+ module進(jìn)行驗證。

TypeOK ==
    /\ ch \in Seq(0..4)
    /\ produced \in 0..5
    /\ consumed \in 0..5
    /\ closed \in BOOLEAN

定義不變量，確保變量狀態(tài)在系統(tǒng)的所有行為過程中始終保持在合理范圍內(nèi)，該TypeOK不變量即是整個程序的安全屬性。

Init ==
    /\ ch = <<>>
    /\ produced = 0
    /\ consumed = 0
    /\ closed = FALSE

這是初始狀態(tài)的公式，對應(yīng)了四個變量的初始值。

Produce ==
    /\ produced < 5
    /\ ch = <<>>
    /\ ~closed
    /\ ch' = Append(ch, produced)
    /\ produced' = produced + 1
    /\ UNCHANGED <<consumed, closed>>

這里定義了生產(chǎn)操作的公式，只有在produced < 5，ch為空且closed不為true時，才會生產(chǎn)下一個數(shù)字。這里設(shè)定ch為空作為前提條件，主要是為了體現(xiàn)Channel的unbuffered的性質(zhì)。

Close ==
    /\ produced = 5
    /\ ch = <<>>
    /\ ~closed
    /\ closed' = TRUE
    /\ UNCHANGED <<ch, produced, consumed>>

這里定義了關(guān)閉操作的公式，這里的ch = <<>>子公式的目的是等消費(fèi)完之后再關(guān)閉channel，當(dāng)然這里與Go的機(jī)制略有差異。

Consume ==
    /\ ch /= <<>>
    /\ ch' = Tail(ch)
    /\ consumed' = consumed + 1
    /\ UNCHANGED <<produced, closed>>

這里定義了消費(fèi)操作的公式，只有channel不為空，才進(jìn)行消費(fèi)。

Next ==
    \/ Produce
    \/ Close
    \/ Consume

這里基于三個操作公式定義了下一個狀態(tài)(Next)的公式，使用/運(yùn)算符將這三個操作連接起來，表示下一步可以執(zhí)行其中任意一個操作。

Fairness ==
    /\ SF_<<ch, produced, closed>>(Produce)
    /\ SF_<<produced, closed>>(Close)
    /\ SF_<<ch>>(Consume)

這里定義了公平性條件，確保各操作最終會被執(zhí)行。

Spec == Init /\ [][Next]_<<ch, produced, consumed, closed>> /\ Fairness

這里定義了整個并發(fā)程序的規(guī)范，包括初始條件Init和下一步動作約束以及Fairness條件。/\連接的第二段Next表示系統(tǒng)的每一步都必須符合Next定義的可能動作，并且不會改變 <<ch, produced, consumed, closed>> 元組中變量之外的其他變量。Fairness 表示系統(tǒng)必須滿足前面定義的 Fairness 條件。

THEOREM Spec => []TypeOK

這是一個定理，表示如果系統(tǒng)滿足Spec規(guī)范，則一定會滿足TypeOK這個不變量。其中的"=>"是蘊(yùn)含的意思，A => B表示如果A為真，那么B必然為真。用一個例子可以解釋這點(diǎn)，如果x > 3為真，那么 x > 1 必為真，我們可以將其寫為：x > 3 => x > 1。

ChannelEventuallyEmpty == <>(ch = <<>>)
AllMessagesProduced == <>(produced = 5)
ChannelEventuallyClosed == <>(closed = TRUE)
AllMessagesConsumed == <>(consumed = 5)

這里定義了四個活性屬性，用于在TLC Model check時驗證最終狀態(tài)使用，其中：ChannelEventuallyEmpty表示最終消息隊列 ch 一定會為空；AllMessagesProduced表示最終一定會生產(chǎn)5條消息；ChannelEventuallyClosed表示最終消息隊列一定會被關(guān)閉；AllMessagesConsumed表示最終一定會消費(fèi)5條消息。

接下來，我們可以使用前面提到的TLA+ Toolbox來check該spec，下面是model的設(shè)置和model check的結(jié)果：

model設(shè)置

check結(jié)果

注：在VSCode中使用TLA+插件的Checker對上述tla進(jìn)行check，會出現(xiàn)不滿足活性屬性的error結(jié)果。

6. 小結(jié)

在這篇文章中，我們從Lamport提供的C語言代碼示例出發(fā)，一步步介紹了如何將其轉(zhuǎn)換為TLA+ spec，并使用TLA+ Toolkit進(jìn)行驗證。然后我們又以一個Go語言的生產(chǎn)者-消費(fèi)者并發(fā)程序為例，展示了如何使用TLA+對其進(jìn)行建模和驗證。

不過我必須承認(rèn)，TLA+這種形式化驗證語言是極小眾的。對大多數(shù)程序員來說，可能沒什么實際幫助。即便是在大廠，真正使用TLA+對分布式系統(tǒng)進(jìn)行形式化驗證的案例也很少。

但是，我認(rèn)為TLA+仍然有其獨(dú)特的價值：

• 它迫使我們用更抽象和精確的方式思考系統(tǒng)設(shè)計，有助于發(fā)現(xiàn)潛在的問題。
• 對于一些關(guān)鍵的分布式系統(tǒng)組件，使用TLA+進(jìn)行驗證可以極大地提高可靠性。
• 學(xué)習(xí)TLA+的過程本身就是一次提升系統(tǒng)設(shè)計能力的過程。

當(dāng)然，形式化方法并非萬能。比如它無法解決性能退化等問題，也不能驗證代碼是否正確實現(xiàn)了設(shè)計。我們應(yīng)該將其視為系統(tǒng)設(shè)計和驗證的補(bǔ)充工具，而不是替代品。

總之，雖然TLA+可能不適合所有人，但對于那些構(gòu)建復(fù)雜分布式系統(tǒng)的工程師來說，它仍然是一個值得學(xué)習(xí)和使用的強(qiáng)大工具。我希望這篇文章能為大家了解和入門TLA+提供一些幫助。

本文涉及的源碼可以在這里[19]下載 - https://github.com/bigwhite/experiments/blob/master/go-and-tla-plus

本文部分源代碼由claude 3.5 sonnet生成。

7. 參考資料

• The TLA+ Home Page[20] - https://lamport.azurewebsites.net/tla/tla.html
• 《Practical TLA+：Planning Driven Development[21]》- https://book.douban.com/subject/30348788/
• Learn TLA+[22] - https://www.learntla.com/
• 《[A Science of Concurrent Programs]》(https://lamport.azurewebsites.net/tla/science.pdf) - https://lamport.azurewebsites.net/tla/science.pdf
• 《Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers[23]》- https://book.douban.com/subject/3752446/
• Linux Foundation Announces Launch of TLA+ Foundation[24] - https://www.linuxfoundation.org/press/linux-foundation-launches-tlafoundation
• TLA+ Foundation[25] - https://foundation.tlapl.us/
• TLA+ in TiDB[26] - https://github.com/pingcap/tla-plus
• TLA+ Web Explorer[27] - https://will62794.github.io/tla-web
• TLA+ language support for Visual Studio Code[28] - https://github.com/tlaplus/vscode-tlaplus
• Use of Formal Methods at Amazon Web Services[29] - https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf
• Leslie Lamport's The TLA+ Video Course[30] - https://www.youtube.com/playlist?list=PLWAv2Etpa7AOAwkreYImYt0gIpOdWQevD
• Leslie Lamport's The TLA+ Video Course homepage[31] - https://lamport.azurewebsites.net/video/videos.html
• Introduction to TLA+[32] - https://lamport.azurewebsites.net/video/video1-script.pdf
• TLA+ Google Group[33] - https://groups.google.com/g/tlaplus
• HILLEL WAYNE Blog[34] - https://www.hillelwayne.com/
• Leslie Lamport: Thinking Above the Code[35] - https://www.youtube.com/watch?v=-4Yp3j_jk8Q