> In this paper, we show the surprising result that no completely asynchronous consensus protocol can tolerate even a single unannounced process death. - [[Byzantine fault]]は考慮せずとも(もっとゆるく[[Crash fault]]しか仮定していない)、信頼性のある通信路があって、Exactly-onceのメッセージ配信が可能と仮定しても、ダメ！ - Nonterminationが起こりうる - [[Determinisitc Consensus]]を仮定している # 論文 - [ ] https://dl.acm.org/doi/10.1145/3149.214121 ([[JACM]]'85) ## 2. Consensus Protocols - Consensus Protocol $P$の定義: $N \geq 2$個のプロセスからなる[[Asynchronous System]] - 各プロセス$p$がもつinternal state: - 1bitの入力レジスタ$x_p$ - ${\{b, 0, 1\}}$の値を持つwrite-onceな出力レジスタ$y_p$ (初期値は$b$, $0$ or $1$が決定状態) - 無限の容量を持つinternal storage - program counter - 各プロセス$p$は状態遷移関数に従い決定論的に作用する - 他のプロセスとはメッセージングにより通信する（共有バッファがある） - バッファのinitial stateは空 - $\text{send}(p, m)$: メッセージバッファに$(p, m)$を置く - $\text{receive}(p)$: メッセージバッファから$(p, m)$を削除し、$m \in M \cup \{\phi\}$を返す。メッセージがなければ$\phi$を返す - メッセージは[[Eventual Delivery]]が保証されている - **event**: message mをpが受信したこと。e = (p, m) - Systemの**configuration**（構成、Global State） $C$: 各プロセスの内部状態・バッファの中身から構成される - **step**: configurationの遷移 - event $(p, m)$によって引き起こされる。pがmをreceiveして、mに応じて内部状態を決定論的に更新する。そして他のプロセスに有限個の新たなメッセージを送る。 - **schedule**: 有限・無限のイベントの列 - いくつかのプロセス$p$が$y_p = v$となる決定状態になるとき、$C$は決定値$v$を持つ - 故障モデル - プロセス$p$は、無限に多くのstepを持つ場合nonfaulty - それ以外はfaulty - [[Crash fault]]を想定しているということだろう - 最大で1つのプロセスのみ故障していて、それ以外のnonfaultyプロセスにはメッセージがeventuallyに届けられる - Consensus Protocolのcorrectness - **Partially correct** 1. No accessible configuration has more than one decision value - どのような遷移可能なConfigurationも、複数の決定値を持たない 2. Validity: For each $v \in {0, 1}$, some accessible configuration has decision value v - 0と1それぞれについて、その値を決定値とする遷移可能なConfigurationが存在する - **Totally correct** - 1つのfaulty processがいても、partially correct かつ いくつかのプロセスが決定状態にたどり着ければOK - schedule - accessible - Lemma 1 (scheduleの[commutativity](Commutative.md): あるconfiguration $C$から、schedules $\sigma_1, \sigma_2$がそれぞれconfigurations$C_1, C_2$を導くとする。$\sigma_1$と$\sigma_2$のstepを取るプロセスの集合がdisjointである場合、$C_1$に$\sigma_2$を適用し、また$C_2$に$\sigma_1$を適用することで同じconfiguration$C_3$を導くことができる - disjoint: 2つのscheduleの間で、stepを実行するプロセスの集合に共通部分がない。つまり、スケジュール$\sigma_1$とスケジュール$\sigma_2$が適用されるプロセスが全く別々なときのこと。 - **Admissible Run**: 最大1つのプロセスが故障していて、故障していないプロセスに送信されたすべてのメッセージが最終的に受信されるような実行 - **Deciding Run**: 実行中に何らかのプロセスが決定状態に到達する P is totally correct in spite of onefault if it is partially correct, and every admissible run is a deciding run. Our main theorem shows that every partially correct protocol for the consensus problem has some admissible run that is not a deciding run. - Partially correct: 以下の2つを満たす合意プロトコル 1. 到達可能な構成は、1つのdecision valueしかもたない 2. v = 0, 1それぞれについて、いくつかの構成がdecision value vをもつ - Totally correct: - Partially correct かつ 全てのadmissible runがdeciding runであること ## Main result - Theorem 1: No consensus protocol is totally correct in spite of one fault - 1つの故障にも関わらず、totally correctなconsensus protocolはない ([[Asynchronous System]]の場合は) ### 証明 - 背理法を用い、逆に$p$は1つのfaultがあってもtotally correctであると証明しようとしたときに矛盾が生じることでTheorem 1を証明する - 証明の流れ 1. まだ決定されていない初期構成がいくつか存在することを証明する 2. システムが特定の決定をするようなステップを回避するadmissible runを組み立てられることを示す とりあえず、Lemma 2で初期構成がbivalentであることを示し、Lemma 3でbivalentな構成からbivalentな構成にたどり着けることを示し、最終的にbivalentな構成からbivalentな構成に無限にグルグルしたらいつまでも値が決定されないので、terminationが保証されないということを言いたい #### まだ決定されていない初期構成がいくつか存在することを証明する - $V$: $C$から到達可能な構成の決定値集合 - Lemma 2: Total correctnessを満たすコンセンサスプロトコル$P$は、bivalent（2価）の初期構成（$|V| = 2$）を持つ - 背理法を使う - Pがunivalentの場合、Partially correctのvalidityより、決定値0をもつ構成と決定値1をもつconfigurationの両方が存在しなければならない #### Bivalentな構成からBivalentな構成にたどり着けることを示す - Lemma 3: $C$を$P$のbi-valent configurationとする。$e = (p, m)$を$C$に適用できる事象とする。$e$を適用せずに$C$から到達できる構成の集合を$\mathbf{C}$とし、$\mathbf{D} = e(\mathbf{C})$とする。このとき、$\mathbf{D}$はbi-valent configrationを含む - 証明 - ![[IMG_0005.jpeg]] - ![[IMG_0006.png]] #### Lemmaを用いたTheorem 1の証明 - deciding runはbivalentな初期configurationから開始し、univalentなconfigurationに到達する - つまり、bivalentからunivalentに到達するいくつかのsingle step（単一のイベントでの状態遷移）がないといけない（runの中にどこかにそういう瞬間があるはずだよね） - ここでは、常に、そのようなステップを回避するような、admissible nondeciding runがあることを示す - stage - プロセスキュー: 最初は適当な順番に並んでいる - プロセスキューの先頭プロセスがステップを実行 - プロセスのメッセージキューが空でなければ、最も古いメッセージを受信 - プロセスはプロセスキューの最後尾に移動 -