Impossibility of Distributed Consensus with One Faulty Process (FLP Theorem)
TL;DR
- 沒有任何一個fully asynchronous & fault tolerance protocol可以保證形成共識。
- 在保證execution 的時候沒有process died & 在執行初始階段majority的processes都alive的情況下,有partially correct consensus protocol存在。
Term Definition
: 代表所有的internal state 加上 message buffer。
: 經過 event ,把帶到下一個state,這稱為一個。
: 從開始,經過finite or infinite的events,把帶到下一個configruation 。
Lemmas
Lemma 1
兩個 schedule 、,如果兩個 schedule disjoint,則順序不影響最終的結果 ( -> , also -> )。
proof
兩者不interaction,所以根據系統定 義,執行順序不影響結果。
Lemma 2
會有一個bivalent initial configuration。(: 最終結果的candidate有兩個)
proof
假設不存在bivalent initial configuration,所有的initial configuration執行完deciding schedule以後,應該都是univalent。
我們先把initial configuration先照process排序,在照value排序,則會有一個 是的value 為0,而相鄰的是的value為1,其餘proccess的value都相同。
我們現在執行一個deciding schedule,在這個deciding schedule中,並沒有任何動作,因為是deciding schedule,根據假設所有的initial configuration執行完應該都要是univalent,因此either是0-valent或是1-valent。
但是讓 和 執行結果以後,result configurations卻有0-valent和1-valent(因為並沒有動作,所以value不會改變),與假設矛盾,故可知假設錯誤,因此有一組bivalent initial configuration。
Lemma 3
假設是一組bivalent configuration, 為一個可以跑在的event,是所有 不跑可以reachable的 configuration set,而 ,則包含一組bivalent configuration。
proof
假設不包含bivalent configuration,定義與是neighbor,如果經過一個step可以到。
中必存在一組, 使得 (i = 0, 1),為了不搞混我們稱此event為, 。
Case 1
如果 ,則根據 lemma 1, 應該等於 ,所以此狀況不可能。
Case 2
如圖,定 義一個deciding schedule使得轉移到,在由各自轉移到、。根據lemma 1,執行的順序不影響結果,而是deciding schedule,所以不會是導致變成bivalent的點,代表、導致了、,而包含、,所以是 bivalent,得證。
Theorems
Theorem 1
沒有任何一個fully asynchronous & fault tolerance protocol可以保證形成共識。
proof
假設是fully asynchronous & fault tolerance且total correct,那必定存在一個deciding step使得最後達成consensus。
但根據lemma 2,一開始存在一組initial bivalent configuration,且根據lemma 1我們可以調換disjoint的event順序不影響結果,因此如果有fault發生我們可以先處理其他event並調換執行順序,因為fault會發生,而且process不知道其他process是掛了還是處理得很慢(因為asynchronous),所以總是可以把deciding run往後延,先處理其他event。
在根據lemma 3,總是可以找到一個event使得result configruation是bivalent(沒有consensus),所以證明protocol無法保證consensus,故不是total correct,得證。
Theorem 2
在保證execution 的時候沒有process died & 在執行初始階段majority的processes都alive的情況下,有partially correct consensus protocol存在。
proof
作者提出一個作法證明可以partially correct,故不用證明。