對于開(kai)(kai)發過分(fen)(fen)布式系(xi)(xi)統(tong)的(de)朋友們，相(xiang)信(xin)(xin)大家都遇到(dao)過這(zhe)種場(chang)景(jing)：系(xi)(xi)統(tong)開(kai)(kai)發完成后，通過了(le)所(suo)有的(de)測試用(yong)例，于是(shi)我們信(xin)(xin)心滿滿地將系(xi)(xi)統(tong)上(shang)線(xian)(xian)。可(ke)是(shi)線(xian)(xian)上(shang)系(xi)(xi)統(tong)跑(pao)著跑(pao)著，不知(zhi)哪一(yi)天突(tu)然莫名(ming)其妙地出現了(le)一(yi)些 bug。當我們打(da)開(kai)(kai)日志，打(da)開(kai)(kai) gdb，準備追蹤定位這(zhe)些問題(ti)時(shi)，它們又(you)無(wu)法(fa)復(fu)現了(le)。可(ke)如果放任不管，不知(zhi)什么(me)時(shi)候，它們又(you)會(hui)詭異(yi)的(de)冒出來了(le)。這(zhe)種 bug 非常棘(ji)手(shou)，甚至讓(rang)開(kai)(kai)發者很崩(beng)潰。這(zhe)個問題(ti)本(ben)質(zhi)上(shang)是(shi)因為分(fen)(fen)布式系(xi)(xi)統(tong)過于復(fu)雜，測試 case 很難覆蓋(gai)所(suo)有可(ke)能(neng)的(de)運行(xing)場(chang)景(jing)所(suo)導致的(de)。無(wu)論再怎(zen)么(me)細心，某些 corner case 總(zong)是(shi)存在的(de)。當系(xi)(xi)統(tong)運行(xing)到(dao)這(zhe)些 corner case 場(chang)景(jing)時(shi)，bug 就出現了(le)。怎(zen)么(me)系(xi)(xi)統(tong)地解決(jue)這(zhe)種問題(ti)呢(ni)？答案就是(shi)本(ben)次(ci)直(zhi)播(bo)分(fen)(fen)享的(de)主角—-TLA+。

TLA+ 是 Paxos 算(suan)法發明者 Lamport 的大作。它是一(yi)套數(shu)學建(jian)(jian)模工具箱，用于給分布式(shi)系統建(jian)(jian)模。主要包(bao)括形式(shi)化(hua)建(jian)(jian)模語言 TLA+ 和形式(shi)化(hua)驗(yan)證工具 TLC model checker。

TDengine 團隊(dui)對 TLA+ 做了一(yi)些探索(suo)，用 TLA+ 為 TDengine Database 的分布式算法（基于(yu)時序場景(jing)下(xia)改進的 Raft 算法）建(jian)模，以保證在時序數(shu)據(ju)場景(jing)下(xia)一(yi)致性和正確性，并兼顧(gu)讀(du)寫性能。也希望通過本次直播，分享下(xia)我(wo)們探索(suo)和實踐 TLA+ 的過程，供大家參考。

TDengine 研發工(gong)程師李(li)明昊結合 TLA+ 在(zai) TDengine Database 的探索，為大家分享如(ru)何用 TLA+ 思維為分布(bu)式算法建模。