Facebook 公佈了 Libra 白皮書和相關技術文檔之後,鏈聞發現了 Libra 區塊鏈將使用基於拜占庭容錯共識的「LibraBFT」共識算法,而 LibraBFT 算法則是「HotStuff」的一個變種。之後,鏈聞又順藤摸瓜,找到了「HotStuff」論文的第一作者、美國康奈爾大學(Cornell)大學在讀博士生尹茂帆(Ted Yin),請他講述了 HotStuff 的奧妙

Ted Yin 今年 25 歲,目前導師是著名計算機科學家 Emin Gün Sirer 教授和 Robbert van Renesse 教授。他同時也是市場頗爲矚目的區塊鏈新項目 Ava Labs 的聯合創始人和首席系統架構師。2018 年暑期期間,他在 VMware Research 實習時提出了「HotStuff」協議中核心算法,並完成了相關論文。

我們邀請 Ted Yin 撰文分享了他提出 「HotStuff」核心算法前前後後的經歷。我們希望通過這篇文章,記錄下一個創新性算法被年輕華人研究者提出的背景,一個有可能推動區塊鏈技術發展的基礎性研究工作完成的來龍去脈。我們希望以此幫助讀者更好了理解「HotStuff」,更可以激勵區塊鏈行業的研究者和開發者更好地建設。

撰文:Ted Yin,康奈爾大學博士生,Ava Labs 的聯合創始人兼首席系統架構師

Libra 採用的 HotStuff 算法作者親述:「尤物」誕生記Ted Yin,HotStuff 論文第一作者, Ava Labs 的聯合創始人和首席系統架構師。

一入系統深似海

沒想到,HotStuff ,這個被我中文起名爲「尤物」協議的科研成果,或多或少竟源自於我第一個「失敗」的研究。請容我細細說來。2016 年,博士之旅伊始,我的導師 Emin Gün Sirer 教授便拿出幾份論文讓我細細研讀。其中有:

  • Paxos Made Moderately Complex;
  • Byzantine Quorum Systems;
  • Implementing Fault-Tolerant Services Using the State Machine Approach。

這些都是共識協議研究經典中的經典。更沒想到的是,有一天,我竟有幸與 Byzantine Quorum Systems 的兩位作者合作完成了後來的尤物協議。

相較於人工智能(AI)的論文,計算機系統相關的研究論文篇幅都較長,一般有十來頁。而共識協議算法的論文每一頁的難度又令人望而卻步。在理解了共識問題的基礎以及經典算法以後,一次開會中,Gün 教授開始考我了。本來胸有成竹的我,被他連珠炮一般的問題問得說不出話來。

「看來你需要回去重新讀一遍啦,Ted!」,他淡然一笑,「不必擔心,本來這世界上沒多少人懂 Paxos。」(鏈聞注:「Paxos」指 Paxos 算法,Paxos 算法是萊斯利·蘭伯特(Leslie Lamport)在 1990 年提出的一種基於消息傳遞且具有高度容錯特性的一致性算法,很多大型分佈式系統都採用 Paxos 算法來解決分佈式一致性問題,Paxos 算法被普遍認爲難以理解,難以實現。)

我愧色滿面,倉皇逃出了辦公室。於是下決心要把其中邏輯理清,以至無懈可擊。

「異步」難題

共識協議,或者推廣至各種分佈式系統的協議,是一類基於時態邏輯的算法描述,其難點在於「異步」(asynchrony)。

所謂異步,就是若干個相對獨立邏輯可以同時執行,並且它們之間能夠依據算法發生交互。這裏的「異步」與異步協議中異步所指不同,更接近於併發(concurrency)的概念。

其實在日常生活中,我們也無時無刻不進行這種「異步」的操作:我們不會幹等一天別人的消息,也不會在整個項目所有的事情做完後才睡覺休息。我們往往是會「同時」處理若干個不同的事務,儘量不會因爲一件事沒有做完而被卡住不做後續的所有事情。

這種等待着一件事情完成再處理另一件事情的過程,就可以被稱爲「同步」;而把事情做一部分丟給別人,接着馬上進行其他操作的過程中,則產生了「異步」。

正如生活中的多任務同時處理一樣,帶有異步 / 併發性質的算法設計充滿了挑戰。以Paxos算法爲例,它是一種 對宕機有一定容忍度的冗餘算法(Crash Fault Tolerance,下稱 CFT)。用通俗的話講,也就是我們希望有若干個機器去備份同一個系統狀態。這個狀態可以是用戶的信息、銀行的交易,或者平臺上程序的執行序列。這種「備份」(replication) ,使得整個系統有一定的抗故障能力 —— 一臺帶狀態副本的機器崩潰之後,我們仍然有別的機器可以使用。

Paxos 作爲這類協議的代表已經在業界獲得了廣泛的使用,比如 Google 的Spanner 系統。毫不客氣地說,雲服務和大規模數據中心的崛起,重要原因之一就要歸功於此。美國計算機科學家萊斯利·蘭波特(Leslie Lamport)提出了 Paxos 算法,這成爲讓他在 2013 年獲得圖靈獎的重要原因之一 —— 當然,蘭波特有太多的貢獻了,包括後文會提到的拜占庭容錯算法(BFT),這裏就不一一展開了。

不過,像 Paxos 這類算法因爲需要保證系統各個機器同時處於一致的狀態,以便對外表現爲一個不間斷的服務,因而十分難以設計和理解。

當然,我的那個故事的結局是:重新來過,認真鑽研,自信滿滿地再次接受也解答了 Gün 教授提出的若干個刁鑽的問題,最終通過了他的考驗。

「那麼接下來我希望你思考一下能不能基於區塊鏈的結構設計一個 CFT 算法,打敗 Paxos。」Gün 教授說。

「好的。」我回答到。

雖萬難吾往矣

就這麼簡單的一句話,花去了我整整第一年一個學期的時間。

現在回想,這個過程短暫又漫長,時而枯燥無味,但時而又充滿驚奇。我曾經構想出了一些看似正確的算法,但僅僅過了一天,隨即便發現無法證明,或者算法本身存在錯誤。直到在第一個暑假來臨前,我向導師提交了一份關於這方面研究的報告。

在報告中我分析了嘗試用鏈式結構打敗 Paxos 的各種大方向。其中主要分爲兩種:

  • 一種路線是採取類似原中本聰共識中的概率模型,然後通過隨機的等待時間來建立起一個可以收斂的共識鏈;
  • 另一種截然不同的思路則是像 Paxos 那樣,使用子集(Quorum)交來把 Paxos「編碼」在鏈上。

在報告中,我給出了基於 Python 快速構建的 Raft (一種類似 Paxos 的協議)和第一種路線的性能對比,得出了不成功的結論。而 Gün 教授對另一個路線並不持樂觀態度 —— 因爲 Paxos/Raft 現在已經被優化得很快了,在這種只有宕機的容錯場景(即 Crash Fault__Tolerance,CFT)下是不具備優勢的。

我們決定放棄這個 CFT 相關的研究,我也轉而有了一個新項目,也就是後來的Avalanche 協議。它是一種概率安全的拜占庭容錯協議,這裏暫不展開。

有趣的是,報告提到的兩條路線中,第一個正好和早期的 DPoS 思路如初一轍。DPoS 是一個備受爭議的協議,它在早期並不是拜占庭容錯的,而且協議本身沒有嚴格的證明或者性能的測試,主要使用它的 EOS 虛擬貨幣,也淪爲了一個高度中心化的系統。而第二個路線,如果將問題的領域由宕機容錯(CFT)變爲拜占庭容錯(BFT),Paxos 改換成 DLS/PBFT,則像極了後來的尤物協議(即 HotStuff) 。

一拍即合

17 年秋季學期即逝,我向 VMware Research 的首席研究員Dahlia Malkhi表達了實習的意向。

Libra 採用的 HotStuff 算法作者親述:「尤物」誕生記Dahlia 畢業於希伯來大學,曾在 AT &T; 研究室工作多年,後自 1999 年到 2007 年在希伯來大學計算機系執教,之後又曾擔任微軟研究院在硅谷 (MSR Silicon Valley) 的首席研究員,並在 2014 年 MSR 硅谷被微軟解散後參與創立了雲基礎架構和移動商務解決方案廠商威睿 (VMware) 的研究機構 VMware Research,擔任首席研究員。她在分佈式系統穩定性和安全性領域研究頗深

當年 12 月,在清華—康奈爾區塊鏈研討會期間,Dahlia 和 VMware Research 的高級研究員 Ittai Abraham 飛到深圳,短暫參會並作了學術報告。報告內容是關於 BFT 協議在區塊鏈時代下的新研究課題。期間,他們宣佈發現了 2007 年獲得 SOSP 最佳論文的 Zyzzyva BFT 系統存在的正確性問題,藉此說明 BFT 協議過於複雜和難以理解,以致在業界無數專家審稿的 10 年以後,仍然可能會發現算法層面的正確性 bug。

我們在她宣講的當天吃了早飯,席間她簡短地用了 30 分鐘問了一些關於我目前科研的問題作爲面試。

Dahlia 在業界以一針見血和才思敏捷著稱,在挺過了她的一些關於 Avalanche 協議的一些尖銳問題後,她表達出了對我一開始那個「夭折」 CFT 項目的濃厚興趣。在次年的遠程交流中,她提到了一個在構想的 BFT 算法有些類似於我的項目,並且詢問我當初放棄的原因。之後我們一拍即合,去 VMware Research 實習的事情也就這麼定了下來。

太平洋的風

實習就這麼開始了。從東岸的紐約飛到了西岸的加州。美好的灣區,全新的暑假。烈日下,太平洋的風時而撥弄着我手中的紙頁,我則低頭繼續思考着「誰是壞人,誰是好人,誰又背叛了誰」的問題 —— 拜占庭容錯。

Libra 採用的 HotStuff 算法作者親述:「尤物」誕生記

Dahlia 告訴我說,一般世界各地的博士生來這裏實習的頭一週都不需要做什麼,而是應該去嘗試摸清自己的能力,以及尋找感興趣的項目。彼時,她提到希望我能看一下他們於三月份撰寫的文稿。

Libra 採用的 HotStuff 算法作者親述:「尤物」誕生記

我喜憂參半。「喜」是因爲有明確的文稿可以閱讀,「憂」則是這個預印稿是不是意味着算法已經設計完畢,而我能做的事所剩無幾?

實際上,在「掙扎」着閱讀了一週以後,我發現初稿中描述的算法很是模糊,正確性的證明也是一筆帶過,其中兩個核心引理都是一句話。於是,在商議後,我們做了一個後來覺得極爲明智,但對我來說也十分挑戰的決定:我不去看那篇預印稿,而是從一張白紙開始,憑着自己受到的啓發,結合已有的積累,用我的符號系統來重新描述算法,並且嘗試給出嚴格的證明。

整個過程大概又花費了將近一週,最後我將重寫的幾頁稿子交給了 Dahlia。令我欣喜的是,得到的反饋非常鼓舞人心。Dahlia 說我自己重頭設計的算法在本質上和她當初的構想大體相似。

但是不久她就發現了一個很不一樣的地方:我的協議裏面需要的假設比原本的預印稿的要更少。

我的解釋是,原稿裏面維護的變量和隱含條件過多,而且有的好像也不是必要。我相信「簡單即是優美」的原則,於是去掉了一些覺得冗餘的不變量。

瞬間,Dahlia 變得嚴肅認真了起來,直截了當地說,「不,這個簡化會直接破壞協議的正確性」。

好在我已早有準備,向她解釋了這個「重要」條件其實是不必要的。但是她依然堅持。

討論變得逐漸激烈,於是我壯了膽,帶着十足底氣的口吻「挑戰」道:「If so, could you please show me a counterexample? (如果真是這樣,你能給我構造一個反例嗎?)」她立即開始在眼前的白板上寫寫畫畫,我全神貫注,準備迎接對我思維以及口語表達的挑戰。

在她數次嘗試失敗之後,我再次耐心地解釋了一遍無需那個條件的原因。我說,聽上去確實挺反直覺的,我一開始也覺得困惑,但是後來發現證明正確性並不需要它。最後,她將馬克筆緩緩放下,笑着長出了一口氣說,「目前我想不到反對的理由。Ted,你贏了。哈哈。」

證明不是一筆揮就的。我一開始自鳴得意的證明很快就被 Dahlia 發現了一個致命問題:有一個條件從來沒有用過。和之前我們所爭論的冗餘條件不同,我們都意識到這是一個極爲關鍵的條件,奈何找遍了整個證明都沒有!

這種感覺就像是修好一個機器後發現手頭多了一些零件,又或是做完手術發現金屬盤裏多出了一些器官一般。所幸的是,很快我們發現了其中一句話其實暗含了條件,但欣慰之餘又感嘆就算是專業人士,做這種 BFT 協議也是十分棘手。

隨後,我們計劃將舊稿替換成現在重寫的新稿。

高手過招

Dahlia 一直是我最敬重的學者之一,因爲她平易近人,跟年輕人打成一片,而在討論學術問題時又有着淵博的知識儲備和學者的嚴肅威嚴,討論細緻入微,不讓毫釐。

老實說,在討論中,大多數時候還是她取得了「勝利」。跟高手「過招」,我不得不歎服她思維的深度、廣度和速度。這也是跟她合作的樂趣:就像是一場賽車比賽,稍一不留神,她就在彎道直接超車,一騎絕塵了;或是在你飛速狂奔而不知其所往時將其橫刀攔下,使之冷靜下來解釋清楚。

不久,坐在旁桌的Mike Reiter也加入了我們的討論。我對計算機安全領域的大佬知之甚少,自然也是不知道這位 Mike 的來頭。只是當時覺得他特別友善,還經常來問我需不需要來看一眼我的稿子,或者討論一下算法問題。

Libra 採用的 HotStuff 算法作者親述:「尤物」誕生記Mike Reiter,現爲北卡羅來納大學教堂山分校計算機系教授

他也對 HotStuff 感興趣,於是我們便有了三人的開會小組。再後來我才意識到,原來最早讀的那篇於 1998 年發表的著名論文「拜占庭仲裁系統 Byzantine Quorum Systems」,正是 Dahlia 和Mike 在 AT&T; 實驗室工作時期所合著的成果。那時的我還在幼兒園留着口水,咬着手指。

Libra 採用的 HotStuff 算法作者親述:「尤物」誕生記1998 年發表在學術期刊「分佈式計算」上的論文「Byzantine quorum systems」

相比 Dahlia,Mike 更像是那種深藏不露的掃地僧。他時常會在你作報告加速時打斷,慢條斯理道:「恕我愚鈍,但是我不理解你剛剛說的東西,你能再解釋一遍嗎?」而我逐漸察覺到他懂的其實遠比看上去的多,總能在關鍵的地方提出非常好的問題。一旦他和 Dahlia 爭論起來,我幾乎無法插嘴,只好在一旁以崇敬的目光看着兩位「神仙大戰」。

猶物之生

Dahlia 提起了最初的論文稿其實投了 2018 年的 PODC 會議(分佈式系統理論頂會),結果被拒。原因有二:審稿人覺得這論文寫得太籠統,他們沒能理解算法的具體過程,以及證明過於簡陋;另一方面則是他們認爲實用拜占庭容錯算法(PBFT)的期刊版本已經在其中「暗示」了可能存在線性複雜度的換屆(view change),所以論文號稱的線性換屆並不是新東西。

Dahlia 對第一點心服口服 —— 這也是讓我不看原文重頭寫過的原因之一。但她對第二點不以爲然,因爲她去找來了那個期刊論文,所謂「暗示」並不可行。

就這一點,我們兩人在一次討論中對 PBFT 期刊版本的算法進行了剖析,最終得出了一個好消息和一個壞消息:好消息是 PBFT 的換屆做不到線性,也就是審稿人的說法有誤;但壞消息是,Dahlia 的舊稿裏面的算法並不符合標題所說的完全線性,而是有更深層次的微妙之處。

Libra 採用的 HotStuff 算法作者親述:「尤物」誕生記就在這次和 Dahlia 對 PBFT 期刊版本的討論中,我們得到了新的思路

實際上,爲了保證響應度(responsiveness, 即在正常運行中不需要讓每個共識等待最大的網絡延遲,從而淪爲「同步協議」),不得不變成平方複雜度;或者爲了線性複雜度而放棄響應度。無論何種取捨,皆使我們的貢獻度大幅縮水 —— 這朵烏雲不幸地於週五飄在了頭頂,在這淪爲「incremental work」的陰霾下我們若有所思地開始了週末。

柳暗花明

山重水複後,我席間提到的一個思路給了 Dahlia 新的啓發。於是,在那個週日的下午,當我還在家慵懶地用筆記本看新聞時,突然收到了一封她上千字的郵件。

果然,在我們的 HotStuff 體系中,儘管最初的算法跟 Tendermint 本質相仿(拋開我們更簡潔優美不談),但還有別的變種可以打破這種壁壘:在保證與 PBFT 類似響應度的同時,達到線性的消息複雜度下界,即理論最優。值得一提的是,前面提到的 Paxos (非拜占庭容錯)同樣也是線性複雜度。

主要思路就是那天討論中我突發奇想提到的:「如果我們增加一個階段呢?兩個階段的協議變三個階段,但是好像我們可以用中間階段維護的不變量(Invariant)來避免 Liveness 的問題,從而完全保證響應度。」

於是,便有了第三版的「尤物」,也是 Facebook 的LibraBFT所基於的那個。

儘管在最終發表的論文中,我被列爲第一作者,但是這個算法的提出,與 Dahlia 和 Mike 等經驗豐富學者的緊密協作及相互間激發出的靈感密切相關。我也很開心,能夠在 VMware Research 短暫的暑假實習期間完成「尤物」的主體部分算法。

在實習結束之後的半年間,我們堅持不懈地完善理論和代碼,並且也嘗試向業界推廣該成果。我們都對創造可以用於實際系統的協議充滿熱情,也都對理論和系統實踐有着一定經驗。Dahlia 顯然比我擁有更多的經驗和更深刻的認識,我從她身上學到了很多。令人感動的是,她對我的思考和每一個建議都認真加以考慮,並且也充分信任我的一些觀點——這使得我憑藉自己對系統和這個行業的理解能有所施展。

例如 Facebook 的 Libra 技術文檔中反覆提到的「起搏器」(Pacemaker),就是由我提出並取的名字。當時我看到 HotStuff 框架提供了一次從算法層面對共識安全(safety)和性能(Liveness) 進行解耦合(decouple)的機會,然後在第一次描述算法時就將保證系統安全的部分抽離出來,然後將與具體應用相關的 heuristics 部分分離成爲一個「起搏器」,來拯救 Liveness。

這一點,毫無疑問,是談論 HotStuff 無法避開的有趣話題。

我真心期待這個「尤物」,能夠讓無論是國外還是國內的巨頭,抑或是創業公司,能夠真正構建實際的拜占庭容錯系統。毫無疑問,Facebook 首先嚐了鮮。

我們在 2018 年向他們推薦了「尤物」,而後如技術文檔中所說,在考慮了市面上諸多其他算法後,他們作出了決定。

與此同時,我也向一些國內的創業公司宣傳了算法。遺憾的是我跟國內大公司並沒有機會接觸,只聽說他們在共識上栽了不少跟頭。

諷刺的是,如今的市場上,極大一部分區塊鏈公司並沒有實現所謂的區塊鏈,遑論拜占庭容錯。殘酷的現實就是,就算從 Google、Facebook 或是阿里、騰訊等公司抓出最優秀的程序員,其中能夠熟練掌握 Paxos (CFT 容錯非 BFT 容錯) 、且知曉如何從頭構建這樣高效系統的人屈指可數。

但是我們不要感到灰心喪氣,因爲這反而是對國內產業的一個前所未有的,趕超世界最領先水平的機遇。除比特幣和以太坊之外,一個合格的、成熟的新 BFT 容錯系統尚未誕生,誰將摘取這個王冠 —— 更確切的是,哪些公司將彎道超車,這尚未可知。

我希望「尤物」能夠拋磚引玉,爲此鋪平道路。

來源鏈接:mp.weixin.qq.com