FLP不可能原理(转)
1. FLP impossibility背景
FLP Impossibility(FLP不可能性)是分布式領域中一個非常著名的結果,該結果在專業領域被稱為“定理”,其地位之高可見一斑。該定理的論文是由Fischer, Lynch and Patterson三位作者于1985年發表,之后該論文毫無疑問得獲得了Dijkstra獎。
順便要提一句的是,Lynch是一位非常著名的分布式領域的女性科學家,研究遍布分布式的方方面面,對分布式領域有著極其卓越的貢獻,其著有<<Distributed Algorithms>>一書,書中有非常嚴謹而簡潔的邏輯討論了許許多多的分布式算法。
FLP給出了一個令人吃驚的結論:在異步通信場景,即使只有一個進程失敗,也沒有任何算法能保證非失敗進程達到一致性!
因為同步通信中的一致性被證明是可以達到的,因此在之前一直有人嘗試各種算法解決以異步環境的一致性問題,有個FLP的結果,這樣的嘗試終于有了答案。
FLP證明最難理解的是沒有一個直觀的sample,所有提到FLP的資料中也基本都回避了sample的要求。究其原因,sample難以設計,除非你先設計幾種一致性算法,并用FLP說明這些算法都是錯誤的。
2. 系統模型
任何分布式算法或定理,都尤其對系統場景的假設,這稱為系統模型。FLP基于下面幾點假設:
?
- 異步通信
與同步通信的最大區別是沒有時鐘、不能時間同步、不能使用超時、不能探測失敗、消息可任意延遲、消息可亂序 - 通信健壯
只要進程非失敗,消息雖會被無限延遲,但最終會被送達;并且消息僅會被送達一次(無重復) - fail-stop模型
進程失敗如同宕機,不再處理任何消息。相對Byzantine模型,不會產生錯誤消息 - 失敗進程數量
最多一個進程失敗
在現實中,我們都使用TCP協議(保證了消息健壯、不重復、不亂序),每個節點都有NTP時鐘同步(可以使用超時),純的異步場景相對比較少。但隨著只能終端的發展,每個手機會為省電而關機,也會因為不在服務區而離線,這樣的適用場景還是存在。
我們再衡量一個分布式算法是否正確時有三個標準:
- Termination(終止性)
非失敗進程最終可以做出選擇 - Agreement(一致性)
所有的進程必須做出相同的決議 - Validity(合法性)
進程的決議值,必須是其他進程提交的請求值
終止性,描述了算法必須在有限時間內結束,不能無限循環下去;一致性描述了我們期望的相同決議;合法性是為了排除進程初始值對自身的干擾。
3. 一個Sample
假設有A、B、C、D、E五個進程就是否提交事務為例,每個進程都有一個隨機的初始值提交(0)或回滾(1)來向其他進程發送請求,進程自己必須接收到其他進程的請求后才能根據請求內容作出本地是提交還是回滾的決定,不能僅根據自己的初始值做出決定。如果所有的進程都做出相同的決定,則認為一致性達成(Validity屬性);根據前面的系統模型,允許最多一個進程失敗,因此一致性要求要放松到允許非失敗進程達成一致。當然,若有兩個不同的值被不同的進程選擇,則認為無法達成一致。
現在目標是要設計這樣一個算法,保證符合上述三個屬性,并允許最多一個進程失敗。
假如我們設計一個算法P,每個節點根據多數派表決的方式判斷本地是提交還是回滾:
假如C收到了A、B的提交申請,收到了D的回滾申請,而C本身也傾向于回滾,此時,提交、回滾各有兩票,E的投票決定著C的最終決議。而此時,E失敗了,或者E發送給C的消息被無限延遲(無法探測失敗),此時C選擇一直等待,或者按照某種既定的規則選擇提交或失敗,后續可能E正常而C失敗,總之,導致C沒有做出最終決策,或者C做了最終決策失敗后無人可知。稱所有進程組成的狀態為Configuration,如果一系列操作之后,沒有進程做出決策稱為“不確定的”Configuration;不確定Configuration的意思是,后續可能做出提交,也可能做出回滾的決議。
相反,如果某個Configuration能準確地說會做出提交/回滾的決議,則稱為“確定性”的Configuration(不確定/確定對應于原論文中的bivalent/univalent)。如果某個Configuration是確定的,則認為一致性是可以達成。
對上述算法P,可能存在一種極端場景,每次都構造出一個“不確定”的Configuration,比如每次都是已經做出決議的C失敗,而之前失敗的E復活(在異步場景中,無法真正區分進程是失敗,還是消息延遲),也就是說,因為消息被延遲亂序,導致結果難以預料!
而FLP證明也是遵循這個思路,在任何算法之上,都能構造出這樣一些永遠都不確定的Configuration,也就沒有任何理論上的具體的算法,能避免這種最壞情況。
4. Paxos為什么可以?
此時我們會馬上想到,Paxos算法的場景比FLP的系統模型還要松散,除了異步通信,Paxos允許消息丟失(通信不健壯),但Paxos卻被認為是最牛的一致性算法,其作者Lamport也獲得2014年的圖靈獎,這又是為什么?
其實仔細回憶Paxos論文會發現,Paxos中存在活鎖,理論上的活鎖會導致Paxos算法無法滿足Termination屬性,也就不算一個正確的一致性算法。Lamport在自己的論文中也提到“FLP結果表明,不存在完全滿足一致性的異步算法...",因此他建議通過Leader來代替Paxos中的Proposer,而Leader則通過隨機或其他方式來選定(Paxos中假如隨機過程會極大降低FLP發生的概率)。也就是說Paxos算法其實也不算理論上完全正確的,只是在工程實現中避免了一些理論上存在的問題。但這絲毫不影響Paxos的偉大性!
5.定理證明
5.1 一些定義
原文雖然字數不多(只有6頁)但卻給出了大量的概念定義,我們盡量簡化為下面幾個:
- 消息隊列:
假定存在一個全局的消息隊列,進程可以發送消息,也可以在其上接收消息。
send/receive:send(p,m)是指給進程p發送消息m,只是放入隊列,稱”發送“,如果消息被p接收,成送達(delivery);receive(p):接收發送給p的消息,若沒有則返回空
消息隊列實際上是模擬了異步通信,即消息會被延遲、亂序 - Configuration:前面已經提到,所有進程的狀態集合,進程的狀態包括初始值、決議值、消息隊列的內容
初始Configuration:各個進程初始值是隨機的、消息隊列為空、決議為空的開始狀態 - 事件e=(p,m)
事件代表給某個進程發送消息,并且消息已經送達。正是因為執行了某個事件,導致Configuration變化為另一個Configuration - 事件序列run
一連串順序執行的事件序列稱為一個run - 可達Configuration
如果某個Configuration A執行了一個run得到另一個Configuration B,則稱B從A可達
接下來通過三個引理證明了最終的FLP結果。
5.2 ?引理1(連通性)
【把所有的進程P分成兩個不相交的集合P1,P2,有兩個run R1,R2,如果先給P1應用R1,再給P2應用R2與先給P2應用R2,再給P1應用R1,對P的Configuration C來說得到的結果是一致的(結果顯而易見,不再羅列證明)】
5.3 引理2(初始Configuration不確定性)
【對任何算法P都存在一個不確定性的初始Configuration(從該Configuration即可到達提交也可到達回滾,參考上面smaple)】
?
這個引理主要是為了說明,不是所有的決議結果都有初始值決定。如果所有進程的初始值都為“提交”,則決議值肯定為“提交”;相反若都為“回滾”則決議為“回滾”,但如果初始值隨機化后,因為消息的延遲,最終的決議值就可能是“提交”也可能是“失敗”(不確定性),這個引理也揭示了異步消息的本質特征。
反證法,假如所有的初始Configuration都是確定性的,即一些決議值必定為“提交”,而另一些一定是“回滾”。如果兩個Configuration只有一個進程的狀態有差別,則稱為相鄰,把所有Configuration按相鄰排成一個環,則必定存在一個Configuration C0和C1相鄰,并且C0是決議“提交”,C1決議“回滾”。
假如某一個Run R導致C1最終的決議值為“回滾”,根據系統模型,允許最多一個進程失敗,我們就假設C0和C1的連接進程P發生失敗。刨除P后,C0和C1的內部狀態應該完全一致,這樣Run R也可應用于C0,也會得到與C1同樣的決議結果:“回滾”。這與C0是“提交”的結果矛盾,因此,必定存在“不確定”的初始Configuration。
?
證明嚴密而巧妙,其中構建相鄰環和基于最多一個進程失敗的假設是關鍵。構建環的方法還會在后續證明中用到。
5.4 引理3(不可終止性)
【從一個“不確定”的Configuration執行一些步驟(delivery消息)后,仍可能得到一個“不確定”的Configuration】
這一點我們已經從前面的Sample看到了,下面是要證明對任何的分布式算法P都存在這樣的不可終止性。為了證明方便,再定義一些用到的符號:
5.4.1 ?證明的正規化
假設Configuration X是“不確定”的,e=(p,m)是可應用于X的事件,C從X可達且沒有應用e的Configuration集合;D=e(C)是對C應用事件e得到的Configuration集合。則D中一定包含一個“不確定”的Configuration。
非常不可思議,e已經應用到了C,雖然進程p已經接受了消息m,得到的Configuration還可能是不確定性的。如Sample所示,在異步環境中的確可以發生這樣的情況。
還是反證法,證明D中的Configuration都是“確定性”的。
5.4.2 證明D中既包含決議為”提交“的Configuration,也包含決議為”回滾“的Configuration。也即證明D中的Configuration不是單值決議。
設E0、E1分別是X中的0-valent(提交)和1-valent(回滾),因為X是”不確定“的,因此E0、E1必存在。假如E0屬于C,即沒有應用事件e,則令F0=e(E0),則F0屬于D;若E0已經應用了e,則在到達E0的過程中,存在D中的F0,E0從F0可達。畫一張圖說明以下:
因為D是”確定“的,E0是0-valent的,無論E0從F0可達,還是F0從E0可達,則F0必定是0-valent的。同樣對E1,也可到的一個1-valent的F1。這就證明了,D包含著0-valent和1-valent。
5.4.3 若D是”確定“的,則導出一個矛盾
如果一個Configuration采取了一個步驟(比如接收一個事件)而產生另一個Configuration,則稱二者為鄰居。根據相鄰環的構建方法,在C中存在C0、C1,二者是鄰居,并且C0是0-valent的,C1是1-valent的。
Di=e(Ci),i=0,1,是i-valent的。假設C1=e'(C0),e'=(p',m'):
(1)如果p≠p',則D1=e'(D0),根據連通性會導出一個矛盾(從D0會到D1,這顯然是不可能的):
(2)那必然是p=p',先看下圖:
我們考慮構造一個Run R,從C0開始,在其中進程p沒有采取任何動作(比如,根據假設,進程p失敗了),則到達Configuration A;
因為,R對進程p沒有任何作用,故R可應用于D0、D1,分別得到E0、E1(因為根據假設D是”確定“的,E0和E1也分別就是0-valent和1-valent)。根據連通性,如果對A連續應用e',e, 則會到達E1;如果對A應用e,則會到達E0。也就是說A是”不確定“的。這與C0是確定的Configuration矛盾,這導致最初的假設D是”確定的”錯誤,因此D是“不確定”的。
這個證明非常巧妙,其核心是根據連通性,構造了一個“不確定”的Configuration。
6. 總結
FLP的證明非常簡潔而嚴謹,這應該是Lynch一貫的作風。看到FLP想起數學上著名的1+1問題的一個例子,1+1這個著名的問題唄關注時,大多數中國人只有初等數學的水平,每天都有很多人給中科院數學研究所寫信,確信自己解決了這個看起來非常簡單的問題。信非常多,但多數證明是錯誤的,不看又怕漏掉一些正確的,工作人員非常辛苦。
后來,有人給出了一個證明,對1+1問題,不可能使用初等數學去解決,這樣那些成麻袋的信就無需再看了,當然那些人對1+1的熱情也隨之被澆滅。最殘忍的是自己認識到“就自己目前掌握的知識根本無法解決這個問題,不是是否努力的問題”。
FLP對此也有類似的影響,但FLP只是理論上存在不可終止性,實際場景中,連續發生不可終止的概率是很低的,可以說為0.至少,FLP證明了異步通信的最壞情況。
非常感謝Ken Birman教授,正是他不厭其煩的講解,才使我對此有較深入的了解。
總結
以上是生活随笔為你收集整理的FLP不可能原理(转)的全部內容,希望文章能夠幫你解決所遇到的問題。
- 上一篇: HPUX下虚拟技术IVM的使用整理
- 下一篇: 运行单机游戏时,缺少D3DCompile