用 TLA+ 幫你驗證系統規格設計

前言

在年初我分享過團隊在嘗試的 self-improvement 計畫，過了半年，還是持續運作中，而且也不斷有收穫，在最近一次的分享會上，後端團隊的同事提到了在設計系統上遇到的一個問題，他們想知道有沒有辦法能驗證自己設計的系統規格沒有邏輯上的錯誤；當下我最直覺的想法是：應該只能把程式照著規格寫出來後，用大量的測試去驗證吧？這也是為什麼越有經驗的人，設計出來的系統通常比較穩定，因為能想到比較多的可能性與細節。

然而事實證明我還是太菜了。

同事介紹了 TLA+ 這個 formal specification language，透過它就能讓你在撰寫實際程式碼前，先行一步針對你的規格設計從高於程式碼的抽象層進行驗證。

這對我來說有點顛覆想像，因此今天就跟大家一起來認識一下 TLA+！

（話先說在前頭，這篇會是一個淺白的介紹文，不會涉及到太多程式語法與細節，主要目的在分享這個工具給大家認識。）

TLA+ 的作者

介紹 TLA+ 前，必須先認識其作者 - Leslie Lamport，他除了創作出 TLA+ 語言外，也是發明麵包演算法與 LaTeX 的人（讀過資工研究所的人對這兩個應該都不陌生吧！），此外更在 2013 年拿到 Turing Award，是個不僅僅在理論上有所突破，在實務上也貢獻良多的大神。

現年已八十歲的他，除了出書以外，在幾年前更錄製了免費的線上課程來教導大家如何使用 TLA+，在 Youtube 與他自己的網站上都找得到。今天這篇文章也是我看了其中兩部影片後總結的一些筆記，從影片與文章中，可以看出他特有的幽默感，很有趣 😂，像是突然扮個小丑：

TLA+ 介紹

TLA+ 是一門針對 digital system 進行 high-level modeling 的語言，擁有檢查模型的工具、IDE；digital system 包含演算法、程式碼、電腦系統；high-level 指的是在設計階段，在實際程式之上，是針對系統規格的驗證與說明。

使用 TLA+ 是指撰寫一個 TLA+ spec，並用 TLA+ Model Checker 來執行驗證，先給大家看長相，最後會有完整的範例：

雖說是一個語言，但是 TLA+ 並不能產生可實際運行的程式碼。TLA+ 主要讓你能針對系統中 critical 的部分更好得進行建模，將非重要部份與實作細節抽離，在並行運算（concurrent）與分散式系統（distributed system）中尤其有用，能幫助你從設計上抓出透過測試難以發現的錯誤與 bug。

對許多工程師來說，可能直覺會認為這東西效益不大，平常寫程式說不定連測試都沒時間寫，額外寫 TLA+ spec 去單純驗證系統設計，真的值得嗎？

這是合理的質疑，但這個方法也是經過許多人實際應用後背書的，許多人學習並使用後，都認為 TLA+ 提供他們一個新的思考方式，即便在實戰上並沒有真的使用到 TLA+，也讓他們成為了更好的工程師。

我想背後的原因是，透過 TLA+ 你可以學習如何更好的將系統抽象化，而抽象化思考對於寫程式與設計系統來說，是非常重要的一個能力。

使用 TLA+ 最著名的例子是 Aamazon Web Services，他們用 TLA+ 設計與驗證了十幾套系統，並寫了一篇論文 - How Amazon Web Services Uses Formal Methods 分享他們如何利用 TLA+ 來對系統進行設計驗證。在每一個採用 TLA+ 的系統上，都有顯著的效果，而且不論老鳥新手，都能在幾週內上手 TLA+，是很值得投資的技術。

TLA+ spec 核心

一個 TLA+ 主要包含三個要素：Abstraction、State machine 與 Mathematic。

Abstraction

如同前面所說，抽象化思考對於寫程式與設計系統來說，是非常重要的一個能力，而學習 TLA+ 最困難的地方就在於學習如何對系統進行抽象化思考。

透過抽象化思考系統，能讓你不被實作細節干擾，專注在優化整體架構，可以改善的程式碼速度與大小都不是實作上程式碼優化能匹配的。Leslie Lamport 的課程中以運行在 Rosetta spacecraft) 的程式為例，透過 TLA+ 的幫助，他們減少了 10倍的程式碼。

對於 TLA+ 來說，系統的執行可以抽象化成一個離散步驟序列（A sequence of discrete steps）。

舉例來說，一個時鐘（系統）的運行，是透過一連串（sequence）的時分針移動（discrete steps）而完成的。

這樣的抽象化可以套用在各種系統上，甚至是並行運算的程式，也能用模擬的方式來表達出 A sequence of discrete steps。

State Machine

一個系統的運作可以用很多種不同方式來描述，程式語言本身就是一個描述方式，但說到底，不管是哪種方式都可以抽象成 State Machine。

上面說到的 A sequence of discrete steps，就是透過每一個 step 來改變系統的 state（狀態），進而完成一系列的系統動作。

一個 State Machine 可以簡化成兩個主要元素：Init 與 Next，分別代表初始狀態，以及可能的下一個狀態。

Math

而這些 State（狀態）的變化與交互，TLA+ 都能夠將其再近一步抽象簡化為數學表達式來呈現，透過數學表示式，能夠更精準且簡潔的表達這些抽象邏輯。

Example

說了這麼多，相信還是在霧裏看花看不清楚，來個最簡單的例子解釋 TLA+ 到底能做些什麼事情吧。

這裡我舉一個我覺得最好懂的例子，叫做 Die Hard，沒錯，就是布魯斯威利主演的電影。在電影裡面，他需要用一個 3 加侖的瓶子與 5 加侖的瓶子裝出 4 加侖的水（這個題目似乎蠻常出現在一些腦經急轉彎的題目中，我甚至在某個面試中被問到過...）

那這個跟 TLA+ 有什麼關係呢？為什麼可以拿來當作範例？

首先，我們假設 用一個 3 加侖的瓶子與 5 加侖的瓶子裝出 4 加侖的水 就是我們系統的規格，那在我們真的實際去寫演算法找答案的之前，我們要怎麼知道這個規格是正確的，是真的有辦法用一個 3 加侖的瓶子與 5 加侖的瓶子裝出 4 加侖的水？

TLA+ 可以幫忙。

完整的 die hard TLA+ 程式碼可以從這裡觀看，我只簡單講解一下主要的邏輯，語法就不著墨了，畢竟我也沒有真的學會。

首先，我們先定義系統的 variables（變數），也就是一個大瓶子與一個小瓶子：

VARIABLES big,   \* The number of gallons of water in the 5 gallon jug.
          small  \* The number of gallons of water in the 3 gallon jug.

接著定義好一個 invariant，也就是一些限制；在這個規格中，我們的限制是大瓶子最多只能裝 5 加侖，而小瓶子最多只能裝 3 加侖：

TypeOK == /\ small \in 0..3 
          /\ big   \in 0..5

然後定義系統的 State machine，描述初始狀態與可能的 Next state：

Init == /\ big = 0 
        /\ small = 0

大小瓶子初始狀態都為空。

Next ==  \/ FillSmallJug 
         \/ FillBigJug    
         \/ EmptySmallJug 
         \/ EmptyBigJug    
         \/ SmallToBig    
         \/ BigToSmall

可能的下個狀態會是透過各種不同的 action(steps) 所產生的，這邊我們有 FillSmallJug（裝滿小瓶子）、SmallToBig（將小瓶子的水倒入大瓶子）、BigToSmall（將大瓶子的水倒入小瓶子）等等。

而實際的 action(steps) 也需要清楚定義其如何造成系統內的 variables（變數）的變化：

FillSmallJug  == /\ small' = 3 
                 /\ big' = big

填滿小瓶子的動作，會讓 small 變數更動為 3，而 big 變數保持不變。

SmallToBig == /\ big'   = Min(big + small, 5)
              /\ small' = small - (big' - big)

小瓶子倒入大瓶子，則要考慮大小瓶子內目前的水容量，已決定最終可以倒入的水量。

當我們描述完整個系統的狀態與狀態轉移動作後，可以訂一個 SPEC，來告訴 TLA+ 這個系統的運行規格是什麼，以這邊為例，我們要做的就是能在保持限制（small <=3, big <=5）的狀況下，能從 Init 狀態，不斷透過 Next 來轉移狀態：

Spec == Init /\ [][Next]_<<big, small>>

透過運行 TLA+ 的 model check，TLA+ 會將這個 spec 所能產生的各種分支狀況都跑過一遍，若運行過程都沒有出現 Error，也就是不管我們的狀態被多少次不同的 Next 改變，都不會違反我們的限制，那我們就能確保此規格是正確的。

疑？你說到目前為止我們還是沒有確保整個規格可以裝出 4 加侖的水呀？

很簡單，我們只要加入一個而外的限制（invariant）即可：

NotSolved == big # 4

這行代表 big 不會等於 4，所以若是出現 big 等於 4 的狀況，TLA+ 的 model checker 就會噴出 Error，並把他是怎麼從 Init 狀態透過哪些 steps 到達這個狀態列出來給你。

所以說，如果 TLA+ model checker 跑下去，都沒有噴出 Error，那就代表這規格有問題，我們不可能用 3 加侖的瓶子與 5 加侖的瓶子裝出 4 加侖的水，但若是有可能，就會在 big 為 4 時噴出 Error。

VSCode 跑 TLA+

最後用個簡單的小影片給大家看看實際運行 TLA+ 是什麼感覺，這邊我用的是 VSCode + TLA+ VSCode extension，對於熟悉 VSCode 的我來說，還是比官方的 TLA+ Tookbox 直覺一些。

若是懶得看影片，最後的結果截圖如下：

可以看他會列出所有造成該 Invariant 出現 error 的過程，也就能知道這個規格是正確的，我們的確能夠用一個 3 加侖的瓶子與 5 加侖的瓶子裝出 4 加侖的水。

最後的最後，還記得上面說過，TLA+ 會將其 Spec 抽象成數學表示式嗎？整個 diehard 的 TLA+ spec 可以透過 TLA+ 轉成如下的 pdf，用數學表示式呈現（不虧是 LaTeX 的作者）：

結論

今天的文章只是非常粗淺的介紹了 TLA+ 是什麼，以及它最簡單的範例，前面也有說到，它實際上是設計來針對並行運算與分散式系統的規格架構設計做驗證，這種系統的複雜程度可想而知，絕對不是一個 DieHard 範例就能呈現其強大之處，但是希望透過這篇文章，能夠帶給大家一些不同的刺激與想像；或許你跟我一樣，在此之前都不曾聽過 TLA+，也不曾想過可以針對規格去做驗證，那這篇文章應該對你還是有所幫助，若是你早已有所聞，甚至有在使用，也歡迎留言分享讓我跟其他人知道，一起教學相長！

資料來源

1. Lamport TLA+ Course
2. Learn TLA+
3. TLA+ offical website
4. 学习 TLA+ - 介绍
5. A gentle intro to TLA+