作者：羅勝金
版權(quán)聲明：歡迎轉(zhuǎn)載鲜滩，請注明原作者

1. 前言

下文將總結(jié)我的TLA+技術(shù)學(xué)習(xí)心得黎侈，分為道（理論）闷游、法（方法）脐往、術(shù)（技術(shù)）业簿、器（工具）梅尤、用（案例）五個(gè)主要部分巷燥。

2. TLA+之“道”——時(shí)態(tài)邏輯

如何保證和證明軟件系統(tǒng)的正確性缰揪？

正確性，是系統(tǒng)最重要的特性抛姑。
CORRECTNESS driven Design定硝。
一般認(rèn)為喷斋，正確性是很難證明的星爪，尤其是并發(fā)系統(tǒng)的正確性粉私，因?yàn)槠湫袨樽兓目赡苄蕴嗯岛恕５墙焉保绻軌虬严到y(tǒng)的狀態(tài)/行為抽象為時(shí)態(tài)邏輯入客，再結(jié)合數(shù)學(xué)分析方法腿椎，就可以判斷系統(tǒng)是否正確。

TLA+與Debug的類比

Debug的原理是通過觀測軟件的屬性和狀態(tài)夭咬，判斷軟件執(zhí)行過程的正確性啃炸。
屬性和狀態(tài)隨時(shí)間的變化過程，就是TLA+中的“時(shí)態(tài)”卓舵。

通過分析系統(tǒng)的狀態(tài)序列變化南用，可以找到系統(tǒng)特性（規(guī)律）

1） 黑子白子問題的例子

壺中有黑子掏湾、白子各若干裹虫，每次取出2子。若2子同色融击，則放回1個(gè)黑子恒界；若2子不同色，則放回1個(gè)白子砚嘴。問最后壺中為黑子還是白子十酣？
舉例分析系統(tǒng)狀態(tài)序列變化。下圖中：B為黑子际长，W為白子耸采，S為狀態(tài)：

說明：公式(N - Wi) % 2 == 0，N工育、Wi分別為壺中白子最初虾宇、最后數(shù)量，公式說明壺中“白子奇偶性不變”如绸，這就是系統(tǒng)的特性（規(guī)律）嘱朽。

2）一個(gè)簡單的多進(jìn)程并發(fā)例子

Lamport論文中給出的多進(jìn)程并發(fā)簡單例子——
有N個(gè)并發(fā)的進(jìn)程，進(jìn)程號i為0～N-1怔接，
每個(gè)進(jìn)程的初始化搪泳，X[i]:=0，
每個(gè)進(jìn)程執(zhí)行后扼脐，

X[i]:=1
Y[i]:=X[(i-1) mod N]  // 當(dāng)i = 0岸军，((i-1) mod N) = N-1  

如何證明：這個(gè)系統(tǒng)滿足——當(dāng)所有進(jìn)程停止后，至少有一個(gè)進(jìn)程的Y[i]:=1瓦侮？

舉例分析如下——
假設(shè)系統(tǒng)中只有2個(gè)進(jìn)程艰赞，進(jìn)程號為0、1肚吏，每個(gè)進(jìn)程執(zhí)行A方妖、B兩步（說明：A——X[i]:=1，B——Y[i]:=X[(i-1) mod N]）罚攀，那么：
【進(jìn)程0執(zhí)行后】

P0A: X[0]:=1         
P0B: Y[0]=x[1] 

【進(jìn)程1執(zhí)行后】

P1A:X[1]:=1
P1B:Y[1]=X[0]

系統(tǒng)所有的可能執(zhí)行序列如下（6種）：

P0A P0B   P1A P1B  ——Y[1]=1
P0A P1A   P0B P1B  ——Y[0]=1 Y[1]=1
P0A P1A   P1B P0B  ——Y[0]=1 Y[1]=1
P1A P1B   P0A P0B  ——Y[0]=1
P1A P0A   P1B P0B  ——Y[0]=1 Y[1]=1
P1A P0A   P0B P1B  ——Y[0]=1 Y[1]=1

由分析結(jié)果看出党觅，每種可能序列雌澄，都至少有一個(gè)進(jìn)程的Y[i]:=1。
當(dāng)然仔役，這是用小樣本例子分析的結(jié)果。如果要證明正確性是己，則需要把問題抽象為時(shí)態(tài)邏輯又兵，用數(shù)學(xué)分析證明。

3）電影《Die Hard》問題

一個(gè)3加侖桶卒废，一個(gè)5加侖桶沛厨，倒騰出4加侖水：
｛3加侖桶水量，5加侖桶水量｝變化序列——

{0,0} {3,0} {0,3} {3,3} {1,5} {1,0} {0,1} {3,1} {0,4}

這個(gè)問題的時(shí)態(tài)邏輯摔认，又應(yīng)該如何描述逆皮，讓數(shù)學(xué)自動(dòng)推理得到結(jié)果呢？

無疑参袱，對很多問題進(jìn)行分析电谣，最終我們會(huì)發(fā)現(xiàn)，問題核心在于其時(shí)態(tài)邏輯抹蚀。
那么剿牺，如何讓計(jì)算機(jī)高效地幫助我們把問題的時(shí)態(tài)邏輯分析清楚，證明系統(tǒng)的正確性环壤，給出軟件設(shè)計(jì)人員想要的結(jié)果呢晒来？

微軟研究院首席研究員、2013年圖靈獎(jiǎng)獲得者郑现，Leslie Lamport大神歷時(shí)數(shù)十年湃崩，研究出了一種方法（數(shù)理邏輯分析）和一套實(shí)用的工具集（TLA+/TLC）。

3. TLA+之“法”——數(shù)理邏輯

要清晰的思考接箫，深入的思考

清晰攒读、深入的思考，是個(gè)人進(jìn)步的來源辛友。
清晰的思考整陌，使得TLA+成為一個(gè)不容易過時(shí)的技術(shù)（Leslie Lamport）。
數(shù)學(xué)瞎领，是幫助我們清晰泌辫、深入思考的一個(gè)工具、一種語言九默。
軟件設(shè)計(jì)及其語言的復(fù)雜性震放，會(huì)干擾我們對業(yè)務(wù)問題本身的思考。

用數(shù)理邏輯表達(dá)時(shí)態(tài)公式（1）

說明：
上圖中的符號驼修，大多數(shù)來自數(shù)學(xué)中集合論和邏輯論的基礎(chǔ)部分殿遂。
其中诈铛，相對不易理解的是“X=>Y”，意思是X“蘊(yùn)含”（imply）Y墨礁，意味著如果X為TRUE則Y一定為TRUE幢竹，X為FALSE則Y可能為FALSE也可能為TRUE，即X是一個(gè)比Y更強(qiáng)的條件恩静。那么焕毫，[X]（滿足X的集合元素）是[Y]（滿足Y的集合元素）的子集。
舉例說明驶乾，X為n>5邑飒，Y為n>1，n為整數(shù)级乐，那么顯然X是比Y更強(qiáng)的條件,滿足n>5的集合[X]是滿足n>1的集合[Y]的子集疙咸。

用數(shù)理邏輯表達(dá)時(shí)態(tài)公式（2）

說明：個(gè)人理解，上圖中风科，“方塊”符號表示Always（總是）撒轮，和“任給”符號都是強(qiáng)條件≡裟拢“菱形”符號表示“Eventually”（最終腔召，總會(huì)），和“存在”符號都是弱條件扮惦。

用數(shù)理邏輯表達(dá)時(shí)態(tài)公式（3）

說明：上圖中的數(shù)理邏輯公式臀蛛，參考（1）和（2）不難理解。

用數(shù)理邏輯表達(dá)時(shí)態(tài)公式（4）

用數(shù)理邏輯表達(dá)時(shí)態(tài)公式（5）

說明：
上圖中崖蜜，[A]_e定義為浊仆，系統(tǒng)要么執(zhí)行A行為（通常A = Next，執(zhí)行下一步）豫领、要么保持目前狀態(tài)/屬性不變（e’ = e抡柿，e通常為系統(tǒng)中的所有變量）。
<A>_e定義為等恐，系統(tǒng)執(zhí)行A行為（通常A = Next）洲劣、并且狀態(tài)/屬性發(fā)生變化（e’ /= e）。stutter字面意思是“口吃”课蔬，表示重復(fù)囱稽、狀態(tài)不變。
[][Next]_v表示“系統(tǒng)總是執(zhí)行下一步或者保持狀態(tài)/屬性不變”二跋，這正是系統(tǒng)設(shè)計(jì)者期望的結(jié)果战惊，因此是safety（安全）的，意味著壞事不會(huì)發(fā)生扎即。
[]<><Next>_v表示“系統(tǒng)總是最終會(huì)執(zhí)行下一步并且改變狀態(tài)/屬性”吞获，這是系統(tǒng)保持liveness（活性）的表現(xiàn)况凉，意味著好事早晚總是會(huì)發(fā)生。
Safety和liveness是軟件系統(tǒng)正確性的兩個(gè)重要因素各拷，Lamport和別的計(jì)算機(jī)科學(xué)家在多篇論文中論述了Safety和liveness的含義和作用刁绒，包括：

• Recognizing safety and liveness
• Preserving Liveness: Comments on `Safety and Liveness from a Methodological Point of View'
• Verifying Safety Properties With the TLA+ Proof System
• Proving the Correctness of Multiprocess Programs
• Mechanical Verification of Concurrent Systems with TLA
• Reduction in TLA
• Proving Possibility Properties

用數(shù)學(xué)（數(shù)理邏輯）描述一個(gè)系統(tǒng)（包括硬件和軟件系統(tǒng)，包括并發(fā)系統(tǒng)）的時(shí)態(tài)邏輯烤黍，進(jìn)而分析知市、論證這個(gè)系統(tǒng)的正確性，這是理論上可行的一種方法蚊荣。但是初狰，這種方法莫杈，如何工程化為一種“技術(shù)”呢互例？這就是Lamport發(fā)明的TLA+。

4. TLA+之“術(shù)”——TLA+語言

TLA+不是一種傳統(tǒng)意義上的編程語言筝闹，它的語法大部分來自于實(shí)際的數(shù)學(xué)（數(shù)理邏輯）媳叨，因此可以把TLA+視為一種程序員容易理解的數(shù)學(xué)語言。

TLA+編碼模板

----- MODULE M ----
EXTENDS M1, ..., Mn    \\* 引入其他模塊关顷，類似#include
CONSTANTS C1, ..., Cn   \\* 定義常量
VARUABLE x1, ..., xn    \\* 定義變量
ASSUME P1           \\* 假設(shè)糊秆、假定
\\* Definitions()  類似宏
OP(x1, ..., xn) == exp
\\* Functions 函數(shù)
f(x \in S) == exp

TLA+保留字

以下為TLA+語法的保留字，部分保留字的含義和其他編程語言類似议双。保留字的用法請參考：http://lamport.azurewebsites.net/tla/book.html痘番。

常用操作符

以下為TLA+的操作符，可以看出平痰，其中絕大部分來自數(shù)學(xué)領(lǐng)域汞舱，其含義也和數(shù)學(xué)公式中的對應(yīng)符號相同，只是為了方便編寫宗雇，可以采用ASCII碼來代表昂芜。保留字的用法請參考：http://lamport.azurewebsites.net/tla/book.html。

個(gè)別容易用錯(cuò)的TLA+語法說明

1）Records（記錄）類型用法

x == [a |-> 1, b |-> {2,3}]  \* “==”表示“定義為”
x.a = 1
x["b"]={2, 3}
DOMAIN x = {"a", "b"}
 
[a : {1}] = {[a |-> 1]}
[b : {{2,3}}] = {[b |-> {2, 3}]}

2） DOMAIN關(guān)鍵字的用法

DOMAIN(<<"a","b","c">>)=1..3
DOMAIN([a |-> 1, b |-> {2,3}])={"a","b"}
DOMAIN({"a","b","c"})  \\* failed. DOMAIN不能應(yīng)用于1個(gè)non-function(a set of the form {e1, ... ,eN})

用TLA+語法描述好系統(tǒng)的時(shí)態(tài)邏輯之后赔蒲，如何驗(yàn)證系統(tǒng)的正確性呢泌神？（實(shí)際上，TLA+還可以驗(yàn)證軟件系統(tǒng)的性能舞虱、時(shí)序等其他重要的特性）答案是使用TLA+提供的工具集TLAToolbox/TLC欢际，還可以使用TLA+的語法糖PlusCal。

5. TLA+之“器”——TLAToolbox/TLC矾兜、PlusCal

Toolbox/TLC

執(zhí)行TLA+語句幼苛，進(jìn)行TLC Model Check的工具。
下載地址：http://lamport.azurewebsites.net/tla/toolbox.html

PlusCal

TLA+的語法糖焕刮。有C和Pascal兩種風(fēng)格舶沿。
建議：先熟悉TLA+語法墙杯，具備用TLA+編寫時(shí)態(tài)邏輯的能力，再使用PlusCal括荡。PlusCal用“TLA+注釋”的方式編寫高镐，寫完后，按“Ctrl + t”·畸冲，Toolbox可自動(dòng)將PlusCal翻譯成TLA+語法嫉髓。出問題了，可以從翻譯生成的TLA+語句開始分析邑闲。

6. TLA+之“用”——驗(yàn)證并發(fā)系統(tǒng)的正確性

TLA+的設(shè)計(jì)算行，最初用于驗(yàn)證硬件系統(tǒng)設(shè)計(jì)的正確性，后來延伸到軟件系統(tǒng)苫耸。
目前州邢，TLA+最有價(jià)值的應(yīng)用之一，是驗(yàn)證并發(fā)系統(tǒng)的正確性褪子。

例子一：分析生產(chǎn)者-消費(fèi)者模型的并發(fā)死鎖問題

互聯(lián)網(wǎng)廣泛使用經(jīng)典的生產(chǎn)者（Producer）-消費(fèi)者（Consumer）模型的消息隊(duì)列（MQ）組件量淌，例如RabbitMQ、NSQ等嫌褪，在一些數(shù)據(jù)庫緩存模塊中也實(shí)現(xiàn)了類似的生產(chǎn)者-消費(fèi)者模型組件呀枢，例如Memcached、Redis等笼痛。
在這種模型下裙秋，當(dāng)多個(gè)Producer和Consumer進(jìn)程并發(fā)訪問消息隊(duì)列時(shí)，如果處理不當(dāng)缨伊，會(huì)產(chǎn)生死鎖問題摘刑。而且，并發(fā)引起的死鎖一旦發(fā)生倘核，很難分析出原因泣侮。

例如，我們不妨以Buffer替代消息隊(duì)列紧唱，來分析下面這段Java代碼的潛在錯(cuò)誤：

public class Buffer<E> {
    public final int capacity;
    private final E[] store;
    private int head, tail, size;
    
    @SuppressWarnings("unchecked")
    public Buffer (int capacity){
        this.capacity = capacity;
        this.store = (E[])new Object[capacity];
    }
    private int next (int x){
        return (x + 1) % store.length;
    }
    public synchronized void put(E e)throws InterruptedException {
        while(isFull())
            wait();
        notify();
        store[tail] = e;
        tail = next(tail);
        size++;
    }
    public synchronized E get() throws InterruptedException {
        while(isEmpty())
            wait();
        notify();
        E e = store[head];
        store[head] = null; // 由GC自動(dòng)回收
        head = next(head);
        size--;
        return e;
    }
    public synchronized boolean isFull(){
        return size == capacity;
    }
    public synchronized boolean isEmpty(){
        return size == 0;
    }
}

上面代碼中活尊，wait()和notify()是Object類提供的方法，wait()阻塞當(dāng)前線程漏益，notify()喚醒等待當(dāng)前對象的線程池中的任意一個(gè)蛹锰。
這段代碼存在著一個(gè)死鎖隱患。如果想通過Log來Debug出這個(gè)死鎖問題绰疤，代價(jià)巨大铜犬。有一篇英文文章介紹，國外某位程序員做了多種嘗試，最后在一臺8核高配機(jī)上癣猾，跑了18天敛劝、產(chǎn)生40億條消息后，復(fù)現(xiàn)了這個(gè)死鎖纷宇。

實(shí)際上夸盟，要找出這個(gè)代碼中的Bug，可以用TLA+來對系統(tǒng)建模像捶，分析其時(shí)態(tài)邏輯的變化過程上陕，找到死鎖原因，進(jìn)而解決它拓春。

TLA+對這個(gè)問題的建模：

EXTENDS Naturals, Sequences

CONSTANTS Producers, (* set of producers *)
          Consumers, (* set of consumers *)
          BufCapacity (* the max numer of messages in the bounded buffer *)
          
VARIABLES buffer, (* the buffer, as a sequence of objects *)
          waitSet (* the wait set, as a set of threads *)
          
Participants == Producers \union Consumers
RunningThreads == Participants \ waitSet

Notify == IF waitSet # {}
          THEN \E x \in waitSet : waitSet' = waitSet \ {x}
          ELSE UNCHANGED waitSet
          
NotifyAll == waitSet' = {}
Wait(t) == waitSet' = waitSet \union {t}

Init == buffer = <<>> /\ waitSet = {}

Put(t) == IF Len(buffer) < BufCapacity
            THEN /\ buffer' = Append(buffer, 1)
                 /\ Notify 
            ELSE /\ Wait(t)
                 /\ UNCHANGED buffer
                 
Get(t) == IF Len(buffer) > 0
            THEN /\ buffer' = Tail(buffer)
                 /\ Notify 
            ELSE /\ Wait(t)
                 /\ UNCHANGED buffer
                 
Next == \E t \in RunningThreads :
            IF t \in Producers THEN Put(t)
                               ELSE Get(t)
                               
Spec == Init /\ [][Next]_<<buffer, waitSet>>
NoDeadLock == [](RunningThreads # {})

在TLAToolbox中释簿，用TLC運(yùn)行、檢查以上模型硼莽，很快（24步庶溶，不到2分鐘）就復(fù)現(xiàn)了并發(fā)死鎖過程：

上圖中，p1沉删、p2渐尿、p3為3個(gè)生產(chǎn)者線程醉途，c1矾瑰、c2為2個(gè)消費(fèi)者線程，Buffer（倉庫）容量為2隘擎。
上圖中殴穴，死鎖發(fā)生的過程是這樣的：

• 某個(gè)時(shí)刻，所有“消費(fèi)者”（c1货葬、c2）和1個(gè)“生產(chǎn)者”（p3）站在等待隊(duì)伍（waitSet）中采幌，倉庫中有1個(gè)商品；
• 接下來震桶，正在工作的“生產(chǎn)者”（可能為p1或p2休傍，假設(shè)為p1）把倉庫塞滿（放入另1個(gè)商品），然后p1要notify()等待隊(duì)伍中的一個(gè)人蹲姐；
• 這時(shí)候磨取，悲劇發(fā)生了，p1它notify()的竟然是p3柴墩！p3離開等待隊(duì)伍后忙厌，留下所有“消費(fèi)者”（c1、c2）在隊(duì)伍中江咳，并且倉庫是滿的逢净；
• 這時(shí)候系統(tǒng)已經(jīng)回天乏力，因?yàn)檎_心工作的p1、p2爹土、p3都發(fā)現(xiàn)甥雕，倉庫已經(jīng)沒有地方讓它們放入商品，它們只好一一重新進(jìn)入等待隊(duì)伍胀茵。而可憐的“消費(fèi)者”們（c1犀农、c2），已經(jīng)沒有任何人有機(jī)會(huì)notify它們從倉庫取出商品（注意：只有完成1次Put或Get后宰掉，才有1次notify的機(jī)會(huì)）呵哨；
• 這樣，所有人都進(jìn)入等待隊(duì)伍轨奄，發(fā)生死鎖孟害。

如此清晰地復(fù)現(xiàn)死鎖過程后，解決起來也很簡單：把Notify()改為NotifyAll()挪拟，每完成1次Put()或Get()后挨务，都把所有線程趕出等待隊(duì)列，就不會(huì)發(fā)生這個(gè)死鎖玉组。

例子二：多線程通過緩存訪問數(shù)據(jù)庫的數(shù)據(jù)一致性問題

系統(tǒng)示意圖如下——
圖中谎柄，多個(gè)客戶線程通過cache操作數(shù)據(jù)庫，每次操作過程是“先讀取惯雳、再加1朝巫、后寫入”。

每個(gè)線程的執(zhí)行代碼如下——

cache = {}
def increment(id):
    x = cache.get(id, None)
    if x is None:
        x = DB_Read(id)
        cache[id] = x
        
    x = x + 1
    DB_Write(id, x)
    cache[id] = x

軟件設(shè)計(jì)者期望石景，假設(shè)數(shù)據(jù)庫中（key：id）的value初值為0劈猿，當(dāng)N個(gè)線程分別操作1次數(shù)據(jù)庫后，數(shù)據(jù)庫中（key：id）的value為N潮孽。這段代碼能實(shí)現(xiàn)嗎揪荣？

用TLA+的語法糖（PlusCal）建模如下：

EXTENDS Integers
CONSTANTS N, not_set
(********************************************************
--algorithm Cache{
    variables cache= not_set, database = 0;
    
    process(Thread \in 1..N)
        variable x;
    {    
t1:     if(cache /= not_set){
            x := cache;
        }else{
t2:         x := database;
            cache := x;
        };
        
t3:     x := x + 1;
t4:     database := x;
t5:     cache := x;    
    }
} ********************************************************)

樣本數(shù)據(jù)把N設(shè)為2（2個(gè)客戶線程），在TLC中運(yùn)行以上模型往史，分析結(jié)果如下：

上圖中仗颈，在第10步（num=10），當(dāng)線程0椎例、線程1都執(zhí)行結(jié)束（Done）后挨决，database為“1”，而不是軟件設(shè)計(jì)者期望的“2”粟矿。為什么呢凰棉？
分析可知，原因是在線程0更新cache值為1（t5）之前陌粹，線程1已經(jīng)取出cache中原來的0值撒犀，作為當(dāng)前操作對象，導(dǎo)致了最終的錯(cuò)誤。

分析發(fā)現(xiàn)或舞，這是數(shù)據(jù)庫訪問的一個(gè)常見問題：在數(shù)據(jù)庫數(shù)據(jù)（本例中為1）和Cache數(shù)據(jù)（本例中為0）不一致時(shí)寫入導(dǎo)致梁剔。解決方案诗芜，是業(yè)界成熟的CAS（Compare and Swap，“樂觀鎖”的一種實(shí)現(xiàn)方式）協(xié)議——
修改PlusCal建模的“寫數(shù)據(jù)庫”部分如下，用TLC分析驗(yàn)證正確：

t2:     y := x + 1;
t3:     if(database = x){   \* cas語義岭粤，目前比較流行的做法
            database := y;
        } else {
          goto t0;       \* retry  
        };    
t4:     cache := y;

使用TLA+把問題分析清楚后低零，“寫數(shù)據(jù)庫”部分的軟件代碼修改如下：

y = x + 1
    if DB_CASWrite(id, x, y):    # if db[id] == x  then db[id] = y
        cache[id] = y
    else:
        increment(id)     # retry

7. 后記

現(xiàn)場記錄的思維導(dǎo)圖

周六聚餐時(shí)鄧輝老師表達(dá)的一些觀點(diǎn)

• 這次是歷次軟件高級設(shè)計(jì)技術(shù)培訓(xùn)中最有價(jià)值的组题。
• 幾年之內(nèi)云矫，掌握TLA+，將成為高端軟件設(shè)計(jì)人才的一個(gè)核心競爭力矫渔。
• 以前一直認(rèn)為軟件設(shè)計(jì)是一門藝術(shù)/匠藝彤蔽，TLA+將把軟件設(shè)計(jì)變?yōu)橐婚T科學(xué)技術(shù)。很多行業(yè)在被科學(xué)攻克之前庙洼，都被認(rèn)為是藝術(shù)顿痪，例如圍棋。
• 準(zhǔn)備這次培訓(xùn)油够，鄧輝老師看了Lamport的180篇論文中的大部分蚁袭，3本專著，還有很多Lamport的技術(shù)視頻石咬。
• 國內(nèi)BAT今后可能會(huì)先引入TLA+來解決一些并發(fā)系統(tǒng)難題（這次培訓(xùn)有阿里人員過來參加）揩悄。國外亞馬遜應(yīng)用TLA+估計(jì)超過10年（羅勝金注：原文稱從2011年開始），2014年亞馬遜10個(gè)核心項(xiàng)目使用了TLA+碌补；目前谷歌虏束、微軟棉饶、甲骨文等公司都在應(yīng)用TLA+厦章。參考：

Since 2011, engineers at Amazon have been using TLA?+? to help solve difficult design problems in critical systems. This paper describes the reasons why we chose TLA?+? instead of other methods, and areas in which we would welcome further progress.
來源：https://link.springer.com/chapter/10.1007%2F978-3-662-43652-3_3

Since 2011, engineers at Amazon Web Services (AWS) have used formal specification and model checking to help solve difficult design problems in critical systems. Here, we describe our motivation and experience, what has worked well in our problem domain, and what has not.
來源：https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/abstract

• TLA+最有價(jià)值的地方，是它致力于解決工程實(shí)際問題照藻，而不是做理論研究袜啃。
• TLA+能夠改變軟件設(shè)計(jì)的思維，提高軟件設(shè)計(jì)人員的思考能力幸缕，清晰化思考群发，這是最有價(jià)值的。

我的個(gè)人感覺

這次培訓(xùn)學(xué)習(xí)確實(shí)很不一樣发乔，之前幾次主要講具體技術(shù)熟妓，例如高可用并發(fā)，機(jī)器學(xué)習(xí)等等栏尚。這次主要講一種思考問題起愈、解決問題的全新視覺——使用數(shù)理邏輯，分析系統(tǒng)的時(shí)態(tài)邏輯，從而驗(yàn)證系統(tǒng)（尤其是并發(fā)系統(tǒng)）的正確性抬虽。
當(dāng)然官觅，鄧輝老師對軟件開發(fā)的很多觀點(diǎn)是一以貫之的。例如阐污，以前在解釋“語義+計(jì)算”時(shí)講過休涤，DDD/DSL是用清晰明確的Spec描述系統(tǒng)行為（再通過解析器把Spec運(yùn)行起來，成為一個(gè)特定功能的機(jī)器）笛辟，Spec是可執(zhí)行功氨、“明顯無錯(cuò)誤”的；TLA+手幢，也是用可執(zhí)行疑故、“明顯無錯(cuò)誤”的Spec來描述系統(tǒng)行為。
所不同的是弯菊，DDD/DSL還是用編程語言來描述纵势，而TLA+可以等同于數(shù)學(xué)語言，更為精確管钳、直截了當(dāng)钦铁。
作為軟件設(shè)計(jì)人員，核心的能力是思考能力才漆，如果能把軟件需要解決的問題牛曹、系統(tǒng)的邏輯關(guān)系思考清楚了，問題就解決大半了醇滥。用何種編程語言和技巧把軟件寫出來黎比，并非核心能力。TLA+給我們提供了一個(gè)清晰化思考的工具鸳玩。

詩以記之

不辭炎暑金陵行阅虫，會(huì)友尋師意難平。
軟件匠工成往事不跟，編程科技蘊(yùn)光明颓帝。
數(shù)學(xué)設(shè)計(jì)同思考，技巧語言費(fèi)鉆營窝革。
江上流波長渺渺购城，不及傳道良師情。