FLP Impossibility證明過程

Consensus共識的定義:

termination終止性: 所有進(jìn)程最終會在有限步數(shù)中結(jié)束并選取一個值, 算法不會無盡執(zhí)行下去.

agreement一致性: 所有進(jìn)程必須同意同一個值.

validity有效性/合法性: 最終達(dá)成一致的值必須是V1到Vn其中一個, 如果所有初始值都是vx, 那么最終結(jié)果也必須是vx.

排除拜占庭問題躬它,只考慮異步通信下的宕機(jī)-恢復(fù)故障模型:消息系統(tǒng)是異步的, 但是任何消息都會被接收一次且僅一次, 并且無法偽造或者丟失。這是比一般的異步網(wǎng)絡(luò)更加可靠的一個網(wǎng)絡(luò)模型. 這樣收窄的一個模型如果在只有一個faulty進(jìn)程的情況下都不能有一個完全正確的共識協(xié)議, 那么在更一般的異步網(wǎng)絡(luò)或者包含Byzantine故障的模型里,更不可能在有一個faulty進(jìn)程的情況下有完全正確的protocol. 這里完全正確(totally correct)是指同時滿足safety和liveness. 在實(shí)際應(yīng)用中, Paxos, Raft, PBFT都是保證safety但是不保證liveness的, 所以他們都不是完全正確的算法, 理論上存在進(jìn)入無限循環(huán)的可能性(實(shí)際上概率非常低, 在工程中完全可以使用). 在當(dāng)時可以說這是一個非常令人震驚的結(jié)論了, 給我們?nèi)粘9こ讨泻芏鄦栴}判了死刑,比如分布式系統(tǒng)的緩存一致性和可用性麻顶,比如分布式事務(wù)的一致性和可用性等等.

一個Sample:假設(shè)有A纹安、B、C锐锣、D技即、E五個進(jìn)程就是否提交事務(wù)為例著洼,每個進(jìn)程都有一個隨機(jī)的初始值提交(0)或回滾(1)來向其他進(jìn)程發(fā)送請求,進(jìn)程自己必須接收到其他進(jìn)程的請求后才能根據(jù)請求內(nèi)容作出本地是提交還是回滾的決定而叼,不能僅根據(jù)自己的初始值做出決定身笤。如果所有的進(jìn)程都做出相同的決定,則認(rèn)為一致性達(dá)成(Validity屬性)葵陵;根據(jù)前面的系統(tǒng)模型液荸,允許最多一個進(jìn)程失敗,因此一致性要求要放松到允許非失敗進(jìn)程達(dá)成一致脱篙。當(dāng)然娇钱,若有兩個不同的值被不同的進(jìn)程選擇,則認(rèn)為無法達(dá)成一致绊困。

現(xiàn)在目標(biāo)是要設(shè)計這樣一個算法文搂,保證符合上述三個屬性,并允許最多一個進(jìn)程失敗秤朗。

假如我們設(shè)計一個算法P煤蹭,每個節(jié)點(diǎn)根據(jù)多數(shù)派表決的方式判斷本地是提交還是回滾:

假如C收到了A、B的提交申請取视,收到了D的回滾申請硝皂,而C本身也傾向于回滾,此時贫途,提交吧彪、回滾各有兩票,E的投票決定著C的最終決議丢早。而此時,E失敗了,或者E發(fā)送給C的消息被無限延遲(無法探測失斣乖汀)傀缩,此時C選擇一直等待,或者按照某種既定的規(guī)則選擇提交或失敗农猬,后續(xù)可能E正常而C失敗赡艰,總之,導(dǎo)致C沒有做出最終決策斤葱,或者C做了最終決策失敗后無人可知慷垮。稱所有進(jìn)程組成的狀態(tài)為Configuration,如果一系列操作之后揍堕,沒有進(jìn)程做出決策稱為“不確定的”Configuration料身;不確定Configuration的意思是,后續(xù)可能做出提交衩茸,也可能做出回滾的決議芹血。

相反,如果某個Configuration能準(zhǔn)確地說會做出提交/回滾的決議楞慈,則稱為“確定性”的Configuration(不確定/確定對應(yīng)于原論文中的bivalent/univalent)幔烛。如果某個Configuration是確定的,則認(rèn)為一致性是可以達(dá)成囊蓝。

對上述算法P饿悬,可能存在一種極端場景,每次都構(gòu)造出一個“不確定”的Configuration聚霜,比如每次都是已經(jīng)做出決議的C失敗狡恬,而之前失敗的E復(fù)活(在異步場景中,無法真正區(qū)分進(jìn)程是失敗俯萎,還是消息延遲)傲宜,也就是說,因?yàn)橄⒈谎舆t亂序夫啊,導(dǎo)致結(jié)果難以預(yù)料函卒!

而FLP證明也是遵循這個思路,在任何算法之上撇眯,都能構(gòu)造出這樣一些永遠(yuǎn)都不確定的Configuration报嵌,也就沒有任何理論上的具體的算法,能避免這種最壞情況熊榛。

定義:

message buffer:系統(tǒng)共用的消息隊列锚国。支持兩個操作 ①send(p,m):把一個消息(p,m)放入message buffer。②receive(p): p從message buffer刪除并取得消息值m, 或者返回null. 前者表示消息被接收到, 如果message buffer為空后者表示沒有p的消息, 如果message buffer不為空表示p的消息傳輸被延遲. 注意, p的消息被延遲的次數(shù)有上限, 任何消息最終都會被收到.

configuration:整個系統(tǒng)的狀態(tài):決議玄坦,所有進(jìn)程的內(nèi)部狀態(tài)血筑,message buffer狀態(tài)

faulty進(jìn)程:可能在一系列操作后绘沉,最終停止的進(jìn)程

決議:進(jìn)程接收到其他進(jìn)程的請求后才能做出決議,不能僅靠自身的初始值豺总。決議Yp有三種可能 0 车伞,1 ,b(不確定)喻喳。只要有一個non-faulty進(jìn)程做出決議Y0或Y1另玖,認(rèn)為整個configuration做出決議(因?yàn)橐笏惴ūWC不能出現(xiàn)兩個不同的決議值)。一個configuration若無論后面發(fā)生什么事件表伦,都會選擇0谦去,則叫0-valent(等價于一個進(jìn)程做出決議Y0)。若都會選擇1蹦哼,則叫1-valent鳄哭。若必須依賴后續(xù)事件才能確定,則叫bi-valent翔怎。

Lemma1連通性:

這條引理表示如果一個C里有兩組事件, 每個事件(p, m)分別是在兩組沒有交互的進(jìn)程上, 那么先使用任何一組事件再使用另外一組事件在C上, 結(jié)果都一樣. 下圖描述了這樣的情況.

Lemma1

這個引理太容易理解了, 就不做證明了. 不過我們可以舉個例子來描述一下: 比如Paxos的兩階段算法中, 假設(shè)有A, B, C, D窃诉,E五個節(jié)點(diǎn), ??1是B收到了A的第一階段消息, ??2是D/E收到了C的第一階段消息(假設(shè)網(wǎng)絡(luò)有延遲,D/E還沒收到A的第一階段消息赤套,B還沒收到C的第一階段消息). 因?yàn)锳/B是一組進(jìn)程, C/D/E是一組進(jìn)程, ??1和??2分別作用于這兩組不相交的進(jìn)程上.那么無論是先??1, ??2的順序被送達(dá)還是按照??2, ??1的順序, 最終結(jié)果都是C3飘痛。前面模型中提到的message buffer可能返回空就很好的模擬了這種消息延遲或者短暫的發(fā)生網(wǎng)絡(luò)分區(qū)的情況.

Lemma2初始configuration不確定性:【對任何算法P都存在一個不確定性的初始Configuration(從該Configuration即可到達(dá)提交也可到達(dá)回滾,參考上面smaple)】

這個引理主要是為了說明容握,不是所有的決議結(jié)果都由初始值決定宣脉。如果所有進(jìn)程的初始值都為“提交”,則決議值肯定為“提交”剔氏;相反若都為“回滾”則決議為“回滾”塑猖,但如果初始值隨機(jī)化后,因?yàn)橄⒌难舆t谈跛,最終的決議值就可能是“提交”也可能是“失敗”(不確定性)羊苟,這個引理也揭示了異步消息的本質(zhì)特征。

反證法感憾,假如所有的初始Configuration都是確定性的蜡励,即一些決議值必定為“提交”,而另一些一定是“回滾”阻桅。如果兩個Configuration只有一個進(jìn)程的狀態(tài)有差別凉倚,則稱為相鄰,把所有Configuration按相鄰排成一個環(huán)嫂沉,則必定存在一個Configuration C0和C1相鄰稽寒,并且C0是決議“提交”,C1決議“回滾”趟章。

假如某一個Run R導(dǎo)致C1最終的決議值為“回滾”杏糙,根據(jù)系統(tǒng)模型慎王,允許最多一個進(jìn)程失敗,我們就假設(shè)C0和C1的連接進(jìn)程P發(fā)生失敗搔啊。刨除P后柬祠,C0和C1的內(nèi)部狀態(tài)應(yīng)該完全一致北戏,這樣Run R也可應(yīng)用于C0负芋,也會得到與C1同樣的決議結(jié)果:“回滾”。這與C0是“提交”的結(jié)果矛盾嗜愈,因此旧蛾,必定存在“不確定”的初始Configuration。


證明嚴(yán)密而巧妙蠕嫁,其中構(gòu)建相鄰環(huán)和基于最多一個進(jìn)程失敗的假設(shè)是關(guān)鍵锨天。構(gòu)建環(huán)的方法還會在后續(xù)證明中用到。

lemma3不可終止性(不確定傳播性):【從一個“不確定”的Configuration執(zhí)行一些步驟后剃毒,仍可能得到一個“不確定”的Configuration】

e=(p病袄,m)代表p收到m消息,e=(p赘阀,null)代表p沒收到消息

所有進(jìn)程比如p必須要根據(jù)e的結(jié)果才會發(fā)生變化(e=(p,m)或e=(p,null))益缠,發(fā)出新的e或者得出決議。

所有的共識算法無非如此:①進(jìn)程發(fā)出msg向其他進(jìn)程通信 (發(fā)出許多e) ②根據(jù)e的結(jié)果處理的邏輯(接收到某些msg基公,就能做出決議幅慌,或者無法決議等待或再發(fā)出msg通信)

Lemma3意思是:任何算法在得到一個不確定的Configuration后(為什么不確定?因?yàn)榭ㄔ谀硞€閾值轰豆,有個一msg因?yàn)檠舆t或者宕機(jī)沒接到)胰伍,無論怎么玩(各種操作去處理),當(dāng)卡在那個閾值的msg到達(dá)后酸休,仍可能得到一個不確定的Configuration骂租。

因?yàn)楫惒江h(huán)境中無法確定是延遲還是宕機(jī)導(dǎo)致e不到達(dá),所以e總可能后續(xù)到達(dá)斑司,只要證明在某個時刻e到達(dá)能導(dǎo)致 bivalent configuration這個小圈渗饮,上面說的【從一個“不確定”的Configuration執(zhí)行一些步驟后,仍可能得到一個“不確定”的Configuration】大圈也就證明了

再說明一下:就是任何算法P總有可能從bivalent configuration一通操作后又變成 bivalent configuration陡厘,就有可能一直無法得到共識抽米。

先說明一下證明的方向

Cb(bivalent configuration 因?yàn)閑=(p,m)每到達(dá)所致),接下來算法會一系列的操作來試圖變?yōu)?/1-valent(讓某一個進(jìn)程做出決議即可)糙置,假設(shè)算法設(shè)定進(jìn)程p做出決議需要n步(n次get e的結(jié)果)云茸,e=(p,m)可能在任意一步后到達(dá) ,所有e到達(dá)后的D configuration 只要有一個bivalent configuration 谤饭,就又回到了Cb标捺,循環(huán)起來懊纳,總有可能無法得出決議。

用反證法亡容,證明 所有D組成的集合 ‘D中全是0-valent或1-valent 為假命題即可嗤疯。

證明:(反證所設(shè)前提 ‘D中全是0-valent或1-valent )

證明分3步,第一步先證明所有通過e可能得到的D 的集合‘D中一定有0-valent與1valent兩種闺兢。

把還沒收到e=(p,m)時茂缚,C可達(dá)的configuration 集合叫ε[configuration]。

因?yàn)镃 為bivalent configuration 屋谭,所以C可達(dá)E0(0-valent) 脚囊,也可達(dá)E1(1-valent)。先看E0桐磁,如果e在做出決議0-valent后到達(dá)悔耘,則D一定是0-valent的(因?yàn)橐呀?jīng)做出了決議,后續(xù)不管咋玩0-valent都不會變)我擂。如果e在做出決議0-valent前到達(dá)衬以,因?yàn)椤瓺中全是0-valent或1-valent,所以 D一定是0-valent(同樣也是因?yàn)橐呀?jīng)做出了決議,后續(xù)不會變化)? 校摩。E1同理看峻,既然C可達(dá)E0與E1,所以‘D中一定有0-valent與1valent兩種秧耗。

第二步备籽,從ε中找兩個configuration,C’與C''分井,使C‘通過一條消息e’= (p’, m’)得到C''(和lemma2一個道理车猬,不過lemma2是以一個進(jìn)程狀態(tài)為單位,這里用一個e做單位尺锚,總有相鄰的C’和C‘’差一個e‘珠闰,得到不同的決議)


D0(0-valent)通過e'變成了D1(1-valent),顯然不可能

情況2:e與e’作用于相同的進(jìn)程p瘫辩,假設(shè)p is faulty(p出了問題伏嗜,所有作用于p的e都不會改變系統(tǒng)的configuration),肯定有一系列事件??(不包含作用于p的事件)可以使C0變?yōu)锳(確定的configuration ,0 或者 1)伐厌。所以??與e作用的進(jìn)程不向交承绸,又可以用到Lemma1:A即可以變成E0,又可以變成E1.矛盾挣轨。(后面e军熏,e'發(fā)生時 p恢復(fù)了)

至此p=p’和p!=p’的兩種情況在我們的反證假設(shè)下都矛盾, 因此反證假設(shè)錯誤. Lemma 3 證明完成, 即: ? 一定包含bivalent configuration.

三個Lemma都證明結(jié)束后, 我們來推導(dǎo)最終FLP定理.

根據(jù)Lemma 2, P一定含有bivalent initial configuration, 那么任何從這個bivalent狀態(tài)進(jìn)入univalent的deciding run, 其中必然存在一個從bivalent到univalent的關(guān)鍵步驟, 這個步驟決定了最終結(jié)果. 我們接下來就是要證明系統(tǒng)中總是有可能會把這個步驟無限推遲下去.

我們設(shè)計一個隊列, 把所有進(jìn)程放到這個隊列中, 按照FIFO的順序每次一個進(jìn)程出來, 這個進(jìn)程從message buffer取出第一個此進(jìn)程的消息, 把計算后發(fā)給其他進(jìn)程的消息放回message buffer尾部, 然后進(jìn)程自己回到隊列尾部等待下一輪調(diào)度. 這個模型保證了每個進(jìn)程總是有機(jī)會獲得發(fā)送給他的消息. 根據(jù)Lemma 2我們知道一定會存在一個bivalent的configuration C0, 從C0開始執(zhí)行到某一個bivalent的C, 這時候message buffer中第一個C的消息是e. 再根據(jù)Lemma 3我們知道如果把e挪到message buffer后面延遲這個消息的送達(dá), 那么C一定會再產(chǎn)生一個bivalent configuration C’進(jìn)入?. 這意味著通過延遲e, 可以讓一個bivalent configuration再產(chǎn)生一個bivalent configuraiton, 因?yàn)榭赡軙肋h(yuǎn)無法達(dá)到一個univalent configuration, 也就永遠(yuǎn)無法產(chǎn)生結(jié)果.

最后編輯于
?著作權(quán)歸作者所有,轉(zhuǎn)載或內(nèi)容合作請聯(lián)系作者
  • 序言:七十年代末,一起剝皮案震驚了整個濱河市卷扮,隨后出現(xiàn)的幾起案子荡澎,更是在濱河造成了極大的恐慌均践,老刑警劉巖,帶你破解...
    沈念sama閱讀 219,589評論 6 508
  • 序言:濱河連續(xù)發(fā)生了三起死亡事件摩幔,死亡現(xiàn)場離奇詭異彤委,居然都是意外死亡,警方通過查閱死者的電腦和手機(jī)或衡,發(fā)現(xiàn)死者居然都...
    沈念sama閱讀 93,615評論 3 396
  • 文/潘曉璐 我一進(jìn)店門焦影,熙熙樓的掌柜王于貴愁眉苦臉地迎上來,“玉大人薇宠,你說我怎么就攤上這事偷办。” “怎么了澄港?”我有些...
    開封第一講書人閱讀 165,933評論 0 356
  • 文/不壞的土叔 我叫張陵,是天一觀的道長柄沮。 經(jīng)常有香客問我回梧,道長,這世上最難降的妖魔是什么祖搓? 我笑而不...
    開封第一講書人閱讀 58,976評論 1 295
  • 正文 為了忘掉前任狱意,我火速辦了婚禮,結(jié)果婚禮上拯欧,老公的妹妹穿的比我還像新娘详囤。我一直安慰自己,他們只是感情好镐作,可當(dāng)我...
    茶點(diǎn)故事閱讀 67,999評論 6 393
  • 文/花漫 我一把揭開白布藏姐。 她就那樣靜靜地躺著,像睡著了一般该贾。 火紅的嫁衣襯著肌膚如雪羔杨。 梳的紋絲不亂的頭發(fā)上,一...
    開封第一講書人閱讀 51,775評論 1 307
  • 那天杨蛋,我揣著相機(jī)與錄音兜材,去河邊找鬼。 笑死逞力,一個胖子當(dāng)著我的面吹牛曙寡,可吹牛的內(nèi)容都是我干的。 我是一名探鬼主播寇荧,決...
    沈念sama閱讀 40,474評論 3 420
  • 文/蒼蘭香墨 我猛地睜開眼举庶,長吁一口氣:“原來是場噩夢啊……” “哼!你這毒婦竟也來了砚亭?” 一聲冷哼從身側(cè)響起灯变,我...
    開封第一講書人閱讀 39,359評論 0 276
  • 序言:老撾萬榮一對情侶失蹤殴玛,失蹤者是張志新(化名)和其女友劉穎,沒想到半個月后添祸,有當(dāng)?shù)厝嗽跇淞掷锇l(fā)現(xiàn)了一具尸體滚粟,經(jīng)...
    沈念sama閱讀 45,854評論 1 317
  • 正文 獨(dú)居荒郊野嶺守林人離奇死亡,尸身上長有42處帶血的膿包…… 初始之章·張勛 以下內(nèi)容為張勛視角 年9月15日...
    茶點(diǎn)故事閱讀 38,007評論 3 338
  • 正文 我和宋清朗相戀三年刃泌,在試婚紗的時候發(fā)現(xiàn)自己被綠了凡壤。 大學(xué)時的朋友給我發(fā)了我未婚夫和他白月光在一起吃飯的照片。...
    茶點(diǎn)故事閱讀 40,146評論 1 351
  • 序言:一個原本活蹦亂跳的男人離奇死亡耙替,死狀恐怖亚侠,靈堂內(nèi)的尸體忽然破棺而出,到底是詐尸還是另有隱情俗扇,我是刑警寧澤硝烂,帶...
    沈念sama閱讀 35,826評論 5 346
  • 正文 年R本政府宣布,位于F島的核電站铜幽,受9級特大地震影響滞谢,放射性物質(zhì)發(fā)生泄漏。R本人自食惡果不足惜除抛,卻給世界環(huán)境...
    茶點(diǎn)故事閱讀 41,484評論 3 331
  • 文/蒙蒙 一狮杨、第九天 我趴在偏房一處隱蔽的房頂上張望。 院中可真熱鬧到忽,春花似錦橄教、人聲如沸。這莊子的主人今日做“春日...
    開封第一講書人閱讀 32,029評論 0 22
  • 文/蒼蘭香墨 我抬頭看了看天上的太陽。三九已至陷遮,卻和暖如春滓走,著一層夾襖步出監(jiān)牢的瞬間,已是汗流浹背帽馋。 一陣腳步聲響...
    開封第一講書人閱讀 33,153評論 1 272
  • 我被黑心中介騙來泰國打工搅方, 沒想到剛下飛機(jī)就差點(diǎn)兒被人妖公主榨干…… 1. 我叫王不留,地道東北人绽族。 一個月前我還...
    沈念sama閱讀 48,420評論 3 373
  • 正文 我出身青樓姨涡,卻偏偏與公主長得像,于是被迫代替她去往敵國和親吧慢。 傳聞我的和親對象是個殘疾皇子涛漂,可洞房花燭夜當(dāng)晚...
    茶點(diǎn)故事閱讀 45,107評論 2 356