CloudNative Days Tokyo 2020 で CockroachDB と TLA+ について話してきました - チェシャ猫の消滅定理

こんにちは、チェシャ猫です。先日行われた CloudNative Days Tokyo 2020 で、形式手法ツール TLA+ が CockroachDB の設計に使用された事例について発表してきました。公募 CFP 枠です。 講演概要 CockroachDB は、Google Spanner の系譜に連なるいわゆる NewSQL データベースの一種です。 強い一貫性や ACID トランザクションといった従来の関係データベースが持つ「良い特徴」を残したまま、従来の関係データベースが苦手としていた水平スケーリングにも優れるのが特徴です。CockroachDB 自身は「地理分散 (geo-distributed) データベース」を標榜しています。 このような CockroachDB の特徴は、内部のデータ保持の方法に由来します。データは内部的には Key-Value レコードの形を取っていて、

[igrep]

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