要約

  • Fischer、Lynch、Paterson は、完全非同期モデルで一つの停止故障を許すと、部分的に正しいどの決定的合意プロトコルにも、永遠に決定しない正当な実行が存在すると証明した。
  • 二価構成では 0 と 1 の両方が将来の決定として残る。独立した事象の順序を交換できるため、重要な事象を遅らせながら、公平な実行と最終的なメッセージ配送を両立できる。
  • 部分同期、故障検出器、乱択は前提を変える。タイムアウトは制御には使えるが、遠隔プロセスの故障を証明する観測ではない。

リーダーから返答が来ないとき、運用画面はしばしば「異常」と表示する。しかし上限のない通信遅延を許す世界では、見えている事実は返答がまだ来ていないことだけだ。プロセスは停止したのかもしれず、単に遅いのかもしれない。この二つを区別できないことが FLP の入口になる。

1985 年の論文 Impossibility of Distributed Consensus with One Faulty Process は、Michael J. Fischer、Nancy A. Lynch、Michael S. Paterson の共同成果である。結論は「合意は不可能」という一般論ではない。指定されたモデルでは、安全な決定的プロトコルが、すべての正当な実行で決定に到達するとは保証できない、という限定された主張だ。

信頼できても、時刻は約束されない

各プロセスは決定的に動き、メッセージで通信する。処理速度にも配送時間にも上限はなく、同期時計もない。メッセージは任意に遅れ、順序も入れ替わり得る。ただし、好きに消えてよいわけではない。非故障プロセスが受信を続けるなら、宛てられたメッセージは最終的に正しく一度だけ届く。

正当な実行で故障できるプロセスは高々一つであり、非故障プロセスは無限回ステップを実行する。この条件は重要だ。証明は、重要な一通を永久に捨てることで停止を作るのではない。プロセスにも待機中のメッセージにも順番を回しながら、決定だけを将来へ送り続けられる。

しかも否定される終了条件は弱い。すべての正当な実行で、少なくとも一つのプロセスがいつか決定すればよい。それさえ保証できないなら、全員の決定を求める強い条件も保証できない。

二価性は状態ではなく可能な未来を表す

構成とは、全プロセスの内部状態と配送待ちメッセージの集合である。どの決定経路も 0 へ向かうなら 0 価、1 だけなら 1 価、両方の結果がまだ到達可能なら二価である。

まず、二価な初期構成が存在しなければならない。すべての初期構成が一価だと仮定し、入力を一プロセスずつ変えると、決定値の異なる隣接構成が現れる。その差を持つプロセスが何もせず停止すれば、残りはどちらの構成か識別できないのに、異なる値を決めるよう求められてしまう。

次に、特定のメッセージ受信のような適用可能な事象を見る。その事象をいったん遅らせ、後で実行すると必ず一価になると仮定すれば、どこかに決定を固定する臨界境界があるはずだ。ところが異なるプロセスの独立なステップは可換である。A の後に B を実行しても、B の後に A を実行しても同じ構成に着く。この可換な四角形は、同じ構成に矛盾する価を与えてしまう。

したがって選んだ事象を有限時間後に実行し、それでも二価性を保つ経路が常にある。対象を公平に巡回すれば、すべてが動き、メッセージも届くのに、決定しない無限実行が得られる。

「存在する」は「いつも起きる」ではない

悪い実行が一つ存在することと、すべての実行が失敗することは違う。現実のシステムは、実際のネットワークが最悪の順序を取らない、あるいは FLP にない追加仮定を設けることで頻繁に決定する。失われるのは無条件の保証であり、実用性ではない。

選挙の停止を見ただけで「FLP が起きた」とも言えない。パケット損失、過負荷、メンバー変更の欠陥、相関故障、実装バグは別の説明である。FLP を使うなら、どのモデルが当てはまり、安全性がどの行動を禁じ、遅延と故障の識別不能性がどのように進行を止めたかを示す必要がある。

前提を追加する三つの方向

Dwork、Lynch、Stockmeyer の部分同期では、存在する時間上限が未知である場合、または既知の上限が未知の安定化時刻以後に成立する場合を扱う。強い条件が成立する期間に進行できる。

Chandra と Toueg の故障検出器は、完全性と正確性という性質を持つ情報源を追加する。沈黙から故障を論理的に導くのではない。Ben-Or などの乱択合意は決定性そのものを外し、確率的な終了を目指す。

どれも FLP の反例ではない。進行の代価として、何を新たに仮定したかを明示する設計である。

Lynch の仕事を共同成果として読む

Lynch の回想によれば、1982 年に Fischer と Lynch が問題に取り組み始め、後に Paterson が加わって最終的な証明へ至った。三人の著者名を保つことは、歴史的な礼儀だけでなく、証拠の精度でもある。

運用への教訓は、耐える故障、時計の性質、故障検出器の保証、安全性を可用性より優先する条件、活性を期待できる環境を公開することだ。FLP は合意を禁じない。保証が依存する世界を隠すことを禁じる。

情報源