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并發程序的設計正確性。

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

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

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

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

1. 為什么需要TLA+

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

為什么要編寫目標系統的spec呢？

綜合來自Lamport的相關資料，大致可以梳理出以下兩點：

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

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

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

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

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

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

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

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

2. Lamport對TLA+的定義

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

• Digital System

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

• High Level

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

去除細節進行簡化的過程就是抽象（Abstraction），它是工程領域最重要的環節。抽象可以讓我們理解復雜的系統，如果不了解系統，我們就無法對系統進行正確的建模并實現它。

而使用TLA+編寫系統spec其實就是一個學習對系統進行抽象的過程，學會抽象思考，可以幫助工程師提高設計能力。

• Modeling

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

此圖由claude sonnet 3.5根據我的prompt生成

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

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

圖片

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

在TLA+中，有兩類屬性是我們特別需要關注的，一類是安全屬性（Safety Properties），一類則是活性屬性（Liveness Properties）。前者確保“壞事永遠不會發生”，比如使用不變量在并發系統中確保兩個進程不會同時進入臨界區；后者則是確保“好事最終會發生”，在分布式系統中的最終一致性（eventual consistency）是一個活性屬性，它保證系統最終會達到一致的狀態。TLA+允許我們精確地指定這些屬性，然后使用TLC模型檢查器來驗證系統是否滿足這些屬性。這種方法特別適合于復雜的并發和分布式系統，因為它能夠發現在傳統測試中難以發現的微妙錯誤。

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

接下來，我們就來看看TLA+究竟如何編寫。不過直接介紹TLA+語法比較抽象和枯燥，在我讀過的TLA+語法資料中，Lamport在The TLA+ Video Course[16]第二講中將一個C示例程序一步一步像數學推導一樣轉換為TLA+語法的講解對我幫助非常大，我覺得有必要將這個示例放到這篇文章中。

3. 從C代碼到TLA+：轉換步驟詳解

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

3.1 初始C程序分析

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

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

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

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

3.2 狀態機描述

該程序可以劃分為三個狀態：

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

下面用自然語言描述一下上述狀態的轉換關系：

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

接下來，我們就來將上述對于狀態轉換的描述變換一下，盡量用數學來表示。

3.3 轉換為數學表示

這里的轉換分為幾步，我們逐一來看。

• 換掉"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"，結果如下：

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

替換的結果如下：

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換為數學符號∈

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+語法轉換

• 將集合表示換為正式的數學符號

{0, 1, ..., 1000}并非數學表示集合的方式，替換后，結果如下：

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+的集合表示語法。

• 轉換為單一公式(formula)

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

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

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

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

• 改造else公式

問題來了! 當存在某個狀態，使得整個公式等于最后一個else公式的值時，我們發現這個值為"no next values"，而前面的then、else if then公式的值都為布爾值TRUE或FALSE。這里最后的ELSE公式，它的值應該為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+的關鍵字為大寫且TLA+源碼為ASCII碼

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

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)

好了，現在我們再把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"

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

3.6 完整的TLA+ spec

從數學層面，上面C代碼將被拆分為兩個公式，一個是初始狀態公式，一個是下個狀態的公式：

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

但對于一個完整的TLA+ spec來說，還需要額外補充些內容：

---- 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名相同，這樣上面代碼對應的tla文件應為SimpleProgram.tla。

EXTENDS會導入TLA+內置的標準module，這里的Integers就提供了基礎的算術運算符，比如+和..。

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

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

"===="用于標識一個module的Body內容的結束。

對于上面簡單的C程序，這樣的spec是可以的。但在實際使用中，spec中的Next一般會很長，一個好的實踐是對其進行拆分。比如這里我們就將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：

圖片

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

圖片

我們看到model check一共檢查了2003個不同的狀態。

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

5. 使用TLA+驗證Go并發程序

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

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

// 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初學者都可以很容易讀懂上面的程序邏輯：Producer生產0到4四個數，每生成一個就通過unbuffered channel發出，consumer從channel接收數字并消費。Producer生產完畢后，關閉channel。Consumer消費完所有數字后，退出，程序終止。

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

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

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

VARIABLES 
    ch,           \* 通道內容
    produced,     \* 已生產的消息數
    consumed,     \* 已消費的消息數
    closed        \* 通道是否關閉

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不算長，但也不短，你可能看不大懂，沒關系，接下來我們就來說說從main.go到ProducerConsumer.tla的建模過程，并重點解釋一下上述TLA+代碼中的重要語法。

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

接下來，我們就要定義action，即導致狀態變化的step，包括Produce、Consume和Close。

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

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

---- MODULE ProducerConsumer ----

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

EXTENDS Integers, Sequences

這行會導入整數和序列模塊，以使用相關運算符。

VARIABLES 
    ch,           \* 通道內容
    produced,     \* 已生產的消息數
    consumed,     \* 已消費的消息數
    closed        \* 通道是否關閉

這里使用VARIBALES關鍵字定義了四個狀態變量，整個TLA+程序的函數邏輯就圍繞這四個變量進行，TLC Model check也是基于這些狀態變量對TLA+ module進行驗證。

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

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

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

這是初始狀態的公式，對應了四個變量的初始值。

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

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

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

這里定義了關閉操作的公式，這里的ch = <<>>子公式的目的是等消費完之后再關閉channel，當然這里與Go的機制略有差異。

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

這里定義了消費操作的公式，只有channel不為空，才進行消費。

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

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

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

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

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

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

THEOREM Spec => []TypeOK

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

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

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

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

model設置

check結果

注：在VSCode中使用TLA+插件的Checker對上述tla進行check，會出現不滿足活性屬性的error結果。

6. 小結

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

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

但是，我認為TLA+仍然有其獨特的價值：

• 它迫使我們用更抽象和精確的方式思考系統設計，有助于發現潛在的問題。
• 對于一些關鍵的分布式系統組件，使用TLA+進行驗證可以極大地提高可靠性。
• 學習TLA+的過程本身就是一次提升系統設計能力的過程。

當然，形式化方法并非萬能。比如它無法解決性能退化等問題，也不能驗證代碼是否正確實現了設計。我們應該將其視為系統設計和驗證的補充工具，而不是替代品。

總之，雖然TLA+可能不適合所有人，但對于那些構建復雜分布式系統的工程師來說，它仍然是一個值得學習和使用的強大工具。我希望這篇文章能為大家了解和入門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