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+ といった命題記述言語に熱心なのか何となく気持ちはわかるような気にはなりました。