July Tech Festa 2021 winter で CockroachDB と TLA+ について話してきました
こんにちは、チェシャ猫です。
インフラ技術のカンファレンス July Tech Festa 2021 winter で、形式手法ツール TLA+ が CockroachDB の設計に使用された事例について発表してきました。公募 CFP 枠です。
今回の登壇は、昨年の CloudNative Days Tokyo 2020 と同じ題材を扱っています。ただ、前回より持ち時間が長くなった分、前回のスライドで説明不足だった部分を拡充してあります。特に、CockroachDB 以外の TLA+ 採用事例や、分散システムにおける Chaos Engineering の位置付けについて解説を追加しました。
なお、前回の登壇報告は以下の記事をご参照ください。
当日出た質問
実時間を含む性質
今回の時相論理では「いつか成り立つ」という性質を記述していたが、時間制限をつけて「n 分以内に成り立つ」いう記述は可能ですか？
いいえ、TLA+ では「何らかの条件 B が成り立つより前に A が成り立つ」という記述はできますが、「n 分以内」のような実際の時間に言及するような記述はサポートしていません。
ただ TLA+ 以外だとこのような性質を記述・検査できるツールも存在します。実時間モデル検査と呼ばれる分野で、有名なツールとしては商用製品ですが UPPAAL が挙げられます。スライド中で「ベースとする数学的対象によってツールの性質が変わる」という話を出しましたが、UPPAAL は時間オートマトン (Timed Automata) をベースにしています。
事例の詳細
その他の TLA+ 採用事例についてもう少し具体的に知りたいです
スライド中に挙げた事例については、以下のリンクが参考になると思います。
AWS DynamoDB
Azure Cosmos DB
TiDB / TiKV
Elasticsearch
学習リソース
形式手法の勉強をしようとすると情報が少なくて困るのですが、TLA+ を勉強する際に良い資料はありますか？
本家である Lamport が自身の Web ページ上にチュートリアルを公開しています。ご本人による動画による解説付きです。やや題材が硬派というか地味な感じですが、TLA+ の機能は最もしっかり解説されているように思います。
また、とりあえず動かしてみて雰囲気を掴みたいということであれば、以下のチュートリアルサイトも小綺麗で良い感じです。このサイトの作者 Hillel Wayne はCockroach Lab 社で TLA+ のセミナーを開催したとのことで、まさに今回の CockroachDB の事例のきっかけを作った人物です。
まとめ
以上、簡単ではありますが、July Tech Festa 2021 winter での登壇と、当日出た質問についてまとめました。
なお、今回の講演で解説した内容は、説明を簡略化するために実際の仕組みを省略している部分がいくつか存在します。もしオリジナル版に興味がある方は、GitHub で公開されている TLA+ 仕様記述を読み解いてみるのも面白いでしょう。
ところで、講演中に OSS の事例として挙げた TiDB と Elasticsearch は、「TLA+ だけでなく他の手法と組み合わせて検証を行なっている」という点でも興味深いプロジェクトです。TiDB が Chaos Mesh を開発していることはスライドに述べた通り、また Elasticsearch は Isablle というまた毛色の違う形式手法ツールを併用しています。
今回 CockroachDB を扱ったので、他のプロジェクトについてもいつかメインで取り上げたいと思っていますが、それはまた別の話。
