paxos

分散システム（分散データベースなど）を勉強しているとどこかでコンセンサスの話が出てきます。そこで paxos と言うアルゴリズム(もしくはプロトコル)がデファウクトスタンダードで、使われているんだが、なんだか難しいことで有名といった記事にぶち当たることがよくあります。ここでは、なんで難しいと言われるか、また理解するにはどうしたらいいかについて個人的な意見を述べます。

コンセンサスアルゴリズムとは
複数のサーバーが、次に何を行うかについて意見を一致させたいといったことは普遍的に起きます。ネットワーク上に分散された複数のサーバー環境では同一の行動をちゃんと取れるか？といったことがでは問題となります。（簡単なケースではネットワークの通信が途切れたりする場合）

paxos の登場
歴史的には上記の問題に対して「2フェイズコミット」と呼ばれる手法があるけれど、それだと、ある種の障害においてはコンセンサスに失敗するということがわかります。(つまりあっちのサーバーとこっちのサーバーで違う意見を採用するといったこと。)
そこで Leslie Lamport は paxos という通信プロトコルを論文「The Part-Time Parliament」 により発表しました。この Lamport という方は分散システム分野の大御所でして他にもビザンチン問題と呼ばれる問題について有名な論文を出しています.
この paxos がなぜ必要になるのかについては「Henry Robinsonによる優しいPaxosの解説」が詳しいのでそちらに譲ります。

paxos は難しい
上記のサイトなども含めて paxos については色々な解説があります。しかし私がそもそもデータベーストランザクションなどに疎いという部分もあるためか、そもそも何がうまくいって何がうまくいっていないのか全くわからないという感覚がずっとありました。それは「Paxos Made Simple」という Lamport 自身により書かれた簡易版を読んでも残りました。また一般的にもやはり paxos は難しいといった認識はあるようです。

(「Paxos, Raftなど分散合意プロトコルを概観する(2) 」などにもそのようなことが書かれております。)

何が難しいのか

一つは原論文「The Part-Time Parliament」の体裁にあります。この論文の体裁なのですが、「古のpaxos 島での会議での合意についての古文書が見つかった、その方法について現代のデータベースシステムでも参考になる部分があるので紹介する」といった体になっています。これがどこまで本当なのかジョークなのかよくわからないといったところでなんだかよくわからないといった気持ちになります。

二つ目は paxos は色々なバリエーションがあり(Lamport 自身も「cheep paxos」「vertical paxos」といったバリエーションを発表している。)、また chubby, zookeeper で使用されている、いやいやあれらは paxos ではないといった議論が色々あり、「paxos とは。。」といった迷路に迷い込むことになります。

結局 paxos は何なの?
色々議論はありますが私としては原論文「The Part-Time Parliament」に Consistency の証明が載っている「Synod’s basic protocol」が paxos であるとして話を進めたいと思います。そうして見ますと上記の「何が難しいのか」について色々見えてくるものもあったという具合です。

改めて paxos について
まずこの「Synod’s basic protocol」ですが、これだけでは本当に一つのコンセンサス問題に対してだけコンセンサスの値を返すだけのものにしかなっていないのです。また複数のサーバーから一台のリーダーを選ぶ必要があるのですが、その選び方については言及はありません(古文書には書いてなかったなどと述べられていたりする。。)。本格的に分散システムを作ろうとすれば、順番にいくつもの動作に関してコンセンサスを取らなければならないし、レプリケーションによるサーバーの交代なども考慮しなければならないなど、このプロトコロルだけではそもそも分散システムを作るには全然足りないのです。そのためにレプリケーション、リーダー選出の部分、複数のコンセンサス問題に対する並列な取り扱いなど色々なバリエーションの paxos が生じることになったわけです。

原論文に戻る
上記のように色々なバリエーションと論文がある訳ですが私個人としては結局、原論文が一番納得できる内容だと思っています。というのも結局、各サーバーがどのデータを永続的に保持し、どのようなアクションを atomic に実行すれば、どのデータの Consistency が壊れないかを、一番明確に記載しているのは原論文だということにあります。原論文を読むという基本的なところからやり直す、遠回りなようだけれどそれが一番だということです。

原論文「The Part-Time Parliament」を読む際のポイント

1. まず paxos 島の議会(paxos 島は実際にありますがこの議会については架空らしいです。)についての話が長く、実際のシステムとどう関係してくるかが最後の方までよくわかりません。この点について私としては「2 The Single-Decree Synod」と「Appendix: Proof of Consistency of the Synodic Protocol 」の部分を読むことに集中するというのが良いのではないかと思います。
2. 次に ballot というものが何なのか微妙によくわからないところがあります。特に後から出てくる vote とどう違ってるのか証明の部分を読まないとよくわからないところがあります。実際は vote は署名、 ballot はそれぞれの署名を署名集、といった感じです。この ballot について数学的なものとして説明がなされるのですが実はこの ballotというデータは各サーバーは保持しないものなのです。
3. ではなぜそんな実際にはサーバーに用意されないデータの説明をしているかというとballot は実はプロトコルの形式証明を行うために必要な補助データとして用意されたものなのです。実際の動的な環境においては意味を持たないです。が、このような補助データを用いて、全てのサーバーを一度に見れる神の視点を用意することで、グローバルに分散システムの状態を記載することができるという点は、生のプログラムコード記述にはない有用な点ではないかと思います。Lamport はこういった証明をつけたかったがために話が複雑になってしまったという点は確かにあるのだと思います。

原論文を読んだ後
Lamport がなぜ TLA+ といった命題記述言語に熱心なのか何となく気持ちはわかるような気にはなりました。

赤黒木

以下を参考にしたメモ
http://www.geocities.jp/m_hiroi/light/pyalgo16.html

赤黒木の定義
　赤黒木は次の条件を満たす「二分木」

1. 各ノードは赤または黒に区分される。
2. 赤ノードの子は必ず黒である。(黒ノードの子に制限はない。)
3. ルートからリーフまでの黒節の個数を「黒高さ」という。赤黒木はルートからリーフへのどの経路でも黒高さが同じであることを要求する。 ここで、子が一つのノードもリーフと取り扱い、上記の条件を満たすことを要求する。
4. ルートのノードは黒。

上記を満たすように挿入、削除を行うことでノードの個数に対して、高さを低く保つことになる。

挿入
まず二分木としてノードを挿入する。この時、挿入されたノードは赤として挿入する。
次に赤黒木の定義を満たすためにノードの色の更新を行う。
二分木の挿入は全てリーフとして挿入されるが、挿入したノードの親ノードが黒の場合は赤黒木の定義に違反することはない。挿入したノードの親ノードが赤の場合、修正操作が必要となる。

一般に二分木に対して次の回転と呼ばれる操作がある。

図1

図2

図3

回転の操作は二分木の条件を満たしつつ行われる操作であり、この操作を組み合わせることで赤黒木の条件を満たすように木を修正する。

挿入の場合分け

以下での説明のためのスライドにおいては挿入されたノードは「n」で表す。また通常挿入されるノードはリーフであるが、証明の都合により、挿入されたノードがリーフでない場合も含めて論証する。またその際、黒高さの条件は満たされており、挿入されたノード以下では赤ノードに関する条件は満たされているとする。
1. 挿入したノードの親が黒ノードの場合

赤黒木の条件を崩さないのでこのままで良い。(図4)

図4

2. 挿入したノードの親が赤ノードの場合

この時、親ノードの親ノードは黒であり、兄弟ノードの親ノードの兄弟ノードの色の場合によって、以下の 3 通りに場合分けされる。
2-1. 親の兄弟がいない場合

この場合、黒高さの条件より、親ノードも子ノードを持たず、自ノードも子ノードを持たない。また挿入したノードが内側にある場合と外側にある場合で、操作に差が出る。以下の 2 通りに場合分けする。
2-1-1.挿入したノードが外側にある場合(図5)

図5

親ノードの親ノードで回転し、親ノードの親ノードと親ノードの色を交換する。これで条件を回復する。

2-1-2. 挿入したノードが外側にある場合(図6)

図6

親ノードの親ノードを起点としてRLの二重回転を行うい、自ノードと親ノードの親ノードの色を変える。これで赤黒木の条件が回復する。

2-2. 親ノードの兄弟が赤ノードの場合(図7)

図7

親ノードの色を赤に、兄弟ノードの自ノードを黒にする。こうすることで、黒高さに対する条件を満たした状態になり、問題をよりルートに近い位置に赤ノードを挿入した場合に帰着できる。木の高さは有限なので、この操作は有限回である。しかし親ノードの親ノードに対する操作がルートまで到達した際には、ルートは黒にして操作が終了する。

2-3. 親ノードの兄弟が黒ノードの場合

挿入したノードが内側にある場合と外側にある場合で、操作に差が出る。以下の 2 通りに場合分けする。
2-3-1.挿入したノードが外側にある場合(図8)

図8

親ノードの親ノードに対して自ノードがいる側を上に持ち上げる回転を行い、親ノードとその親ノードの色を逆にする。これで赤黒木の条件が回復する。

2-3-2.挿入したノードが内側にある場合(図9)

図9

親ノードの親ノードを起点としてRLの二重回転を行う。自ノードと親ノードの親ノードの色を変える。これで赤黒木の条件が回復する。

以上。実は「2-1. 親ノードの兄弟ノードがない」場合と「2-3. 親ノードの兄弟が黒」の場合は同一の操作であることがわかる。また場合分けとして挿入するノードは親ノードの親ノードから見て、右側にある場合を示したが、左側にある場合は逆の回転操作になる。

削除の場合
以降では削除について述べる。削除の場合はさらに場合分けがあり、ある場合がある場合に帰着されるなど、場合の依存がわかりにくいことが赤黒木を複雑にしている要因と思われる。
方針としては挿入の時と同様にまず、2分木の削除を行い、その後、赤黒木の条件を満たすようにノードと色の操作を行う。

2分木の削除の場合、次の図のように二つの子ノードをもつノードを削除する場合にも
一つの子ノードもしくは一つも持たない場合に帰着される。(図10)

図10

よって削除されるノードは2分木の削除なので子ノードが一つか、リーフである場合になる。場合分けとしてまずは削除されるノードの色で場合分けする。
1. 削除ノードが赤の場合

黒高さ、赤ノードに対する条件を破ることはないので、良い。

2. 削除されたノードが黒の場合

かなり場合分けが複雑となる。以下の図11 にある記号を使って、親ノード、兄弟ノード、兄弟ノードの子ノードの色の組み合わせによって場合分けを行う。

図11

上記のように X のルートの部分に取り除いたノードがあったものとする。

2-1. 親ノードが黒の場合

2-1-1. 親ノードが黒、兄弟ノードが黒の場合

2-1-1-1. 親ノードが黒、兄弟ノードが黒、兄弟ノードの子ノードが両方とも黒の場合(図12)

図12

兄弟ノードを赤にすることで取り除いた黒ノードの個数と合わせて黒高さが一定になる。ただし q 以下の黒高さは全体に比べて一つ小さくなっている。なので q 以下の部分木から一つノードを取り除いたパターンとして、また再帰的に木に操作する必要がある。ただし、元々の X の部分から見れば一つ、ルートに近いところから削除されたと見なせるので、この操作は有限回で終わる。もしも q がルートならば操作は終了。全体の黒高さが -1 されたことになる。

2-1-1-2. 親ノードが黒、兄弟ノードが黒、兄弟ノードの子のノードで内側のノードが赤、外側が黒の場合(図13)

図13

兄弟ノードで回転させて、赤の子ノードを持ち上げる回転の操作を行う。そのあと持ち上げた赤ノードと元の兄弟ノードの色を交換する。すると部分木 A,B,C の黒高さはどれも等しいので、これは次の項目で説明する 「2-2-1-3. 親ノードが黒、兄弟ノードが黒、兄弟ノードの子ノードの内側のノードが黒、外側のノードが赤の場合に帰着する。

2-1-1-3. 親ノードが黒、兄弟ノードが黒、兄弟ノードの子のノードの内側のノードが黒、外側が赤の場合(図14)

図14

親ノードで回転させて部分木 X のリーフから全体の木のルートへの黒高さを一つ増やす。この時、部分木 Cの各リーフから全体の木のルートへの黒高さが一つ減るので黒高さを合わせるために C のルートノードを黒にする。

2-1-1-4. 親ノードが黒、兄弟ノードが黒、兄弟ノードの子ノードが二つとも赤の場合(図15)

図15

親ノードを回転させ、部分木 C のルートを黒にすることで黒高さが等しくなる。

2-1-2. 親ノードが黒で兄弟ノードが赤の場合

兄弟ノードの子ノードはないか、両方とも黒となる。(図16)

図16

この場合、親ノードを回転して、元々の親ノードと兄弟ノードの色を交換する。この時、Xにおけるパスではノードの黒高さは回復していない。しかし親ノードが赤であるとき場所のノードを削除した場合、すなわち後述する「2-2.親ノードが赤の場合」に帰着される。

2-2. 親ノードが赤の場合

赤黒木の条件より兄弟ノードは黒となる。よって、兄弟ノードの子ノードが何色かという場合分けをすれば良い。
2-2-1-1. 親ノードが赤、兄弟ノードが黒、兄弟ノードの子ノードが二つとも黒の場合(図17)

図17

親ノードと兄弟ノードの色を交換すれば黒高さの条件が回復する。

2-2-1-2. 親ノードが赤、兄弟ノードが黒、兄弟ノードの子ノードの内側のノードが赤、外側が黒の場合(図18)

図18

兄弟ノードで回転させ、兄弟ノードと、その子ノードの赤い方のノードと色を交換する。すると、部分木 A,B,C の黒高さはどれも等しいので、これは次の項目で説明する 「2-2-1-3. 親ノードが赤、兄弟ノードが黒、兄弟ノードの子ノードの内側のノードが黒、外側のノードが赤の場合に帰着する。

2-2-1-3. 親ノードが赤、兄弟ノードが黒、兄弟ノードの子ノードの内側のノードが黒、外側が赤の場合(図19)

図19

親ノードで回転をし、親ノードと兄弟ノードの色を交換し、部分木C のルートを黒にする。これで黒高さの条件が回復する。

2-2-1-4.親ノードが赤、兄弟ノードが黒、兄弟ノードの子ノードが両方とも赤の場合(図20)

図20

親ノードで回転をし、親ノードと子ノード色を交換し、部分木 C のルートを黒にする。 これで黒高さの条件が回復する。

以上で全ての場合分けをとらえた。図は削除されるノードが左の場合となっているが、右ノードになっている場合は左右が逆の回転となることに注意せよ。また親ノードが赤の場合と黒の場合でほとんど同じ操作となる場合があるが、場合分けの網羅性を明示するためにあえて、そのまま載せることにした。