跳到主要内容

Impossibility of Distributed Consensus with One Faulty Process (FLP Theorem)

TL;DR

  1. 沒有任何一個fully asynchronous & fault tolerance protocol可以保證形成共識。
  2. 在保證execution 的時候沒有process died & 在執行初始階段majority的processes都alive的情況下,有partially correct consensus protocol存在。

Term Definition

ConfigurationConfiguration: ConfigurationConfiguration CC代表所有processprocess的internal state 加上 message buffer。

StepStep: processprocess pp 經過 event ee == (p,m)(p, m),把CC帶到下一個state,這稱為一個stepstep

ScheduleSchedule: 從CC開始,經過finite or infinite的events,把CC帶到下一個configruation CC'

Lemmas

Lemma 1

兩個 schedule σ1\sigma_1σ2\sigma_2,如果兩個 schedule disjoint,則順序不影響最終的結果 (σ1σ2\sigma_1\sigma_2 -> C3 C_3, also σ2σ1\sigma_2\sigma_1 -> C3C_3)。

proof

兩者不interaction,所以根據系統定義,執行順序不影響結果。

Lemma 2

PP會有一個bivalent initial configuration。(bivalentbivalent: 最終結果的candidate有兩個)

proof

假設不存在bivalent initial configuration,所有的initial configuration執行完deciding schedule以後,應該都是univalent

我們先把initial configuration先照process排序,在照value排序,則會有一個 C0C_0pp的value 為0,而相鄰的C1C_1pp的value為1,其餘proccess的value都相同。

我們現在執行一個deciding schedule,在這個deciding schedule中,pp並沒有任何動作,因為是deciding schedule,根據假設所有的initial configuration執行完應該都要是univalent,因此either是0-valent或是1-valent

但是讓C0C_0C1C_1執行結果以後,result configurations卻有0-valent1-valent(因為pp並沒有動作,所以value不會改變),與假設矛盾,故可知假設錯誤,因此有一組bivalent initial configuration

Lemma 3

假設CC是一組bivalent configurationee == (p,m) (p, m)為一個可以跑在CC的event,YY是所有 CC 不跑ee可以reachable的 configuration set,而DD == e(Y)e(Y),則DD包含一組bivalent configuration

proof

假設DD不包含bivalent configuration,定義C0C_0C1C_1neighbor,如果e(C0)e(C_0)經過一個step可以到C1C_1

YY中必存在一組C0 C_0, C1C_1使得 DiD_i == e(C0)e(C_0)(i = 0, 1),為了不搞混我們稱此event為ee'ee' == (p,m)(p', m')

Case 1 pp' !=!= pp 如果pp' !=!= pp,則根據 lemma 1D0D_0 應該等於 D1D_1,所以此狀況不可能。

Case 2 pp' == pp

image info 如圖,定義一個deciding schedule使得CC轉移到AA,在由AA各自轉移到E0E_0E1E_1。根據lemma 1,執行的順序不影響結果,而σ\sigmadeciding schedule,所以AA不會是導致變成bivalent的點,代表D0D_0D1D_1導致了E0E_0E1E_1,而DD包含D0D_0D1D_1,所以DDbivalent,得證。

Theorems

Theorem 1

沒有任何一個fully asynchronous & fault tolerance protocol可以保證形成共識。

proof

假設PPfully asynchronous & fault tolerancetotal 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 configruationbivalent(沒有consensus),所以證明protocol無法保證consensus,故不是total correct,得證。

Theorem 2

在保證execution 的時候沒有process died & 在執行初始階段majority的processes都alive的情況下,有partially correct consensus protocol存在。

proof

作者提出一個作法證明可以partially correct,故不用證明。

References