チェシャ猫の消滅定理

数学にプログラミング、素敵なもの何もかも。

CloudNative Days Tokyo 2020 で CockroachDB と TLA+ について話してきました

こんにちは、チェシャ猫です。先日行われた CloudNative Days Tokyo 2020 で、形式手法ツール TLA+ が CockroachDB の設計に使用された事例について発表してきました。公募 CFP 枠です。

講演概要

CockroachDB は、Google Spanner の系譜に連なるいわゆる NewSQL データベースの一種です。

強い一貫性や ACID トランザクションといった従来の関係データベースが持つ「良い特徴」を残したまま、従来の関係データベースが苦手としていた水平スケーリングにも優れるのが特徴です。CockroachDB 自身は「地理分散 (geo-distributed) データベース」を標榜しています。

このような CockroachDB の特徴は、内部のデータ保持の方法に由来します。データは内部的には Key-Value レコードの形を取っていて、データ全体を一定のサイズで Range と呼ばれる単位に区切った上で、Range ごとに Raft 合意アルゴリズムを用いて Node 間複製を行います。

異なる Range 間では Raft による一貫性ははたらきません。したがって、複数の Key に対して同時に捜査する SQL をサポートするためには、分散トランザクションが必要になります。

当初の CockroachDB のトランザクションは、クライアントがトランザクションの完了通知を受け取るまでに Raft による合意のレイテンシが 2 往復分必要でした。新しく導入された Parallel Commit はこのレイテンシを減らし、1 往復で完了通知が出せるようにしたものです。

ところで、一般に分散アルゴリズムを正しく設計するのは難しい作業です。一般に複数のプロセスはそれぞれのタイミングで処理を進めており、実行順について正確に予測することができません。また、分散システムではプロセス間通信がネットワークを挟むため、パケットの遅延・入れ替わり・消失などについて全ての場合を考える必要があります。

結果として、非常に限られたパターンでしか発現しないバグが含まれていたとしても、それを通常のテストを通して発見するのは極めて困難です。

CockroachDB の Parallel Commit プロトコルも例外ではありません。そこで Cockroach Lab はこのプロトコルの正しさを検証するために形式手法 (formal methods)を利用しました。

形式手法は、対象となるシステムを数学的な定式化を用いて厳密に記述し、その性質を検査する方法群です。中でも今回利用されたツールは TLA+ と呼ばれるもので、CockroachDB 以外にも、Cosmos DB や TiDB など CloudNative として名前が挙がる OSS で使用されています。

Parallel Commit の具体的なプロトコル、および TLA+ による検査の内容について詳細はスライドを参照してください。

Parallel Commit に関する補足

講演中に解説した Parallel Commit の動作は簡略化されたものであり、説明のためにいくつかの要素が意図して省かれています。

Pipelining

今回の解説では、トランザクションに属するすべてのキーとトランザクションレコード自体を同時に書き込む形式になっていました。しかし実際には COMMIT コマンドが発行されるよりも前、すなわちトランザクションに含まれるキーが確定しないうちに Intent の書き込みリクエストが始まります。この最適化は Pipelining と呼ばれています。

この挙動は TLA+ の記述にも反映されており、キー確定前にリクエストを送信する pipelined_keys と、確定後にトランザクションと同時にリクエストを送信する parallel_keys が分けて扱われています。

Timestamp Cache と Epoch

今回の解説では、Transaction Recovery の途中でコンフリクトするインテントを発見し次第 Abort させる形式になっていました。このとき実際には、未達だった書き込みリクエストが Abort 後になって到着して書き込まれることがないよう、「Intent が存在しないことが観測された時刻」を Timestamp Cache として保持しておきます。また、書き込むとき Timesatmp Cache を悲観的にチェックした上で、衝突が発生した場合にはトランザクションの Epoch を増やして最初からやり直す処理が必要です。

この挙動も TLA+ の記述に反映されており、インテントを扱う際には tscache を確認する仕組みになっています。

参考資料

CockroachDB

TLA+

その他 TLA+ 事例

まとめ

今回の講演では、分散データベース CockroachDB のアーキテクチャを概説したのち、合意レイテンシを減らす最適化 Parallel Commit の必要性について述べました。また Parallel Commit の検証において、形式手法の一種 TLA+ が使われている様子について例を挙げて説明しました。

ところで、実は CockroachDB の TLA+ 仕様には正しくない部分があり、しかしそのミスは通常の検査では Transaction Recovery で覆い隠されてしまうため、非常に見つけにくい状態になっています。

github.com

チェシャ猫自身が今回の講演の準備中に気づいたので既に Issue として挙げておいたのですが、これをどうやって発見したのか、それはまた別の話。