對于開發(fā)過分布式系統(tǒng)的朋友們，相信大家都遇到過這種場景：系統(tǒng)開發(fā)完成后，通過了所有的測試用例，于是我們信心滿滿地將系統(tǒng)上線。可是線上系統(tǒng)跑著跑著，不知哪一天突然莫名其妙地出現(xiàn)了一些 bug。當我們打開日志，打開 gdb，準備追蹤定位這些問題時，它們又無法復現(xiàn)了?？扇绻湃尾还埽恢裁磿r候，它們又會詭異的冒出來了。這種 bug 非常棘手，甚至讓開發(fā)者很崩潰。這個問題本質(zhì)上是因為分布式系統(tǒng)過于復雜，測試 case 很難覆蓋所有可能的運行場景所導致的。無論再怎么細心，某些 corner case 總是存在的。當系統(tǒng)運行到這些 corner case 場景時，bug 就出現(xiàn)了。怎么系統(tǒng)地解決這種問題呢？答案就是本次直播分享的主角—-TLA+。

TLA+ 是 Paxos 算法發(fā)明者 Lamport 的大作。它是一套數(shù)學建模工具箱，用于給分布式系統(tǒng)建模。主要包括形式化建模語言 TLA+ 和形式化驗證工具 TLC model checker。

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

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