Brewer's Conjecture and the Feasibility of Consistent, Available, Partition-Tolerant Web(2002)

January 17, 2023

分散システムは一貫性、可用性、分断耐性を同時に満たすことができない。この予想は、2000年のPODCでBrewerが発表したCAP定理として知られている。しかし、Brewerの講演では厳密な定義や証明はない。そこで、それを補うために、ある2つの計算モデルでCAPが成立することを証明する。計算モデルは、asynchronous network modelとpartially synchhronous modelである。 asynchronouse network modelでは、モデルのノードは、クロックをもたず、受信したメッセージとノード内の計算のみで出力を決定する。 partially synchronous modelでは、各ノードは、一定間隔で単調増加するクロックをもち、処理をタイムアウトしたり、スケジューリングしたりできる。ただし、ノード間でクロックが同期されているとは限らない。

証明のために、はじめに、一貫性、可用性、分断耐性を定義する。一貫性を線形化可能性とみなす。線形化可能性の必要十分条件は、読み書きがアトミックであるかのように観測できる全順序の操作列が存在することである。可用性があれば、正常なノードにメッセージを送ると、かならず応答をえられる。ただし、応答の時間の長さに上限はない。分断耐性の分断は、ノードから別のノードへのメッセージが届かないことを意味する。

以上の定義でCAP定理が成立するとき、asynchronous network modelは、分断しうるネットワークにおいて、可用性と線形化可能性を満たすことはない。証明には背理法を使い、両性質を満たすアルゴリズム\(A\)を仮定する。ここに2つのノードの素集合\(G_1, G_2\)があり、異なる素集合のノード間の通信が分断されている。 \(A\)のプレフィックス\(\alpha_1\)を、\(G_1\)のノードが一貫性のあるオブジェクトの値を\(v_0\)とは別の値の書き込みで終わる操作系列とする。また、\(\alpha_2\)を、\(G_2\)のノードがオブジェクトの値の読み込みで終わる操作系列とする。また、\(\alpha_1, \alpha_2\)には、\(G_1, G_2\)間でのメッセージを送信はないとする。可用性があるので、\(\alpha_1\)の書き込みと\(\alpha_2\)の読み込みは完了する。 \(\alpha_1\)と\(\alpha_2\)を連結した実行系列を\(\alpha\)とおく。 \(G_2\)は、\(G_1\)とメッセージを交換できないため、\(\alpha\)と\(\alpha_2\)を区別できない。そのため、線形化可能性より\(\alpha_2\)の読み込みの結果は\(v_0\)でなければならない。ところが、\(\alpha\)において、\(\alpha_2\)の前には\(\alpha_1\)があり、オブジェクトの値が変更された後にしか読み込みはない。したがって矛盾である。

メッセージが消失しないネットワークであっても、可用性と一貫性を満たすことはない。 asynchronous network modelは、到達時間が無限に長いメッセージと消失したメッセージを区別できない。そのため、メッセージの消失しないネットワークで性質を同時に満たすアルゴリズムがあるならば、それは消失する環境でも2つの性質をみたすことになり、さきほどの証明に反する。一方、partially synchronous modelであれば、一貫性を犠牲にすれば可用性を実現できる。これは、ノードが別のノードに送信したメッセージの応答が一定時間経過しても返らない場合、フォールバックの値を出力すればよい。

論文のリンク

雑記

第二著者のNancy A. LinchはFLP不可能性を証明したことでも知られる。 FLP不可能性は、プロセスがクラッシュしうる場合には常に含意を保証できる非同期アルゴリズムは存在しないことをいう。

asynchronous network modelが線形化可能性をみたさないことを示すときに、線形化可能性のローカル性が使われている。各ノードが線形化可能かつそのとき限り、システム全体が線形化可能になる。そのために、\(G_2\)だけに着目した操作系列が線形化可能でないことから、システム全体が線形化可能でないといえる。

線形化可能性はかなり強い制約で、PostgreSQLをはじめとするRDMSでも、デフォルトのトランザクション分離レベルでサポートしていない。また、CAP定理の可用性は、1つのノードだけに着目した性質であって、ノードが故障したときにシステム全体が正常に機能するかを問うていない。 Nancy Linchの論文のなかで、後者について分析したものにConsensus in the Presence of Patial Synchronyがある。これは、partial synchronousとよばれる環境でシステムが正常に機能するために必要なプロセッサ数と障害を許容できるプロセッサ数の関係を示した。