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

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

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

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