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
,故不用證明。