Lock in $30 Savings on PRO—Offer Ends Soon! ⏳

CockroachDB から覗く形式手法の世界 #JTF2021w / July Tech F...

y_taka_23
January 24, 2021

CockroachDB から覗く形式手法の世界 #JTF2021w / July Tech Festa 2021 winter

July Tech Festa 2021 winter で使用したスライドです。

バグのない分散システムの設計は果たして可能でしょうか? この問いに対する一つの答えとして、CockroachDB では形式手法ツール TLA+ を用いて分散トランザクションの正しさを担保しています。 形式手法はシステムの挙動を数学的に解析する技法で、「ノードが特定のタイミングで故障した場合にのみ発生するバグ」といった再現困難な問題を確実に検出することができます。 本講演では、CockroachDB の事例を通して、形式手法が実世界で活用されている様子をお伝えします。

イベント概要:https://techfesta.connpass.com/event/193966/
ブログ記事:https://ccvanishing.hateblo.jp/entry/2021/01/24/185819
録画:https://www.youtube.com/watch?v=T26-viZnrE0

y_taka_23

January 24, 2021
Tweet

More Decks by y_taka_23

Other Decks in Technology

Transcript

  1. • CockroachDB の概要 ◦ スケーラビリティを実現するアーキテクチャ ◦ 生じた課題と Parallel Commit による解決

    • 形式手法ツール TLA+ の概要 ◦ 理論はともかく、ツールとしての雰囲気 ◦ CockroachDB の挙動をどう表現・検証するか
  2. • Spanner 系の分散データベース ◦ インタフェースとして SQL をサポート ◦ 強い一貫性を持ったトランザクションをサポート ◦

    旧来の RDB と異なりスケールアウト可能 • データは Node 間で冗長化される ◦ 一定規模以下の Node 障害時でもデータを守れる
  3. id (PK) author like 1 alice 4 2 alice 8

    3 bob 5 /posts/2/author /posts/2/like /posts/3/id /posts/3/author /posts/3/like /posts/1/id /posts/1/author /posts/1/like /posts/2/id key alice 8 _ bob 5 _ alice 4 _ value
  4. • 合意 (Consensus) プロトコル ◦ 一度、合意が得られればその値は覆らない • Leader Election ◦

    見本となる Node (Leader, LeaseHolder) を選択 • Log Replication ◦ 操作列について合意し LeaseHolder の状態を複製
  5. k1 = v1 PUT k1 = v1 (k1 ∈ Range

    1) • 各 Range は Raft で可用性と一貫性が 保たれた一塊の DB とみなせる • Range 間にはコミュニケーションの 仕組みがない
  6. 1. トランザクション開始時、Key-Value データと同様に Pending 状態の Transaction Record を書き込む 2. データを書き込む際は上書きする代わりに、

    Intent と呼ばれるマーカをつけ、Record を参照 3. 全てのデータ書き込みが成功したら Record の状態を Committed に変更することでコミット
  7. k1 = v1 k2 = v2 k1 = v1’ (t1)

    k2 = v2’ (t1) t1 = pending Round-1 Consensus
  8. k1 = v1 k2 = v2 k1 = v1’ (t1)

    k2 = v2’ (t1) t1 = pending Round-1 Consensus
  9. k1 = v1 k2 = v2 k1 = v1’ (t1)

    k2 = v2’ (t1) t1 = committed Round-2 Consensus
  10. k1 = v1 k2 = v2 k1 = v1’ (t1)

    k2 = v2’ (t1) t1 = committed Round-2 Consensus
  11. 1. データを読み込もうとした際、Intent を見つけたら まず対応する Transaction Record の状態を確認 2. Record が

    Pending 状態であれば元の値を採用 3. Record が Committed 状態であれば Intent として 保持されている値を採用
  12. k1 = v1 k2 = v2 k1 = v1’ (t1)

    k2 = v2’ (t1) t1 = pending
  13. k1 = v1 k2 = v2 k1 = v1’ (t1)

    k2 = v2’ (t1) t1 = pending
  14. k1 = v1 k2 = v2 k1 = v1’ (t1)

    k2 = v2’ (t1) t1 = pending
  15. k1 = v1 k2 = v2 k1 = v1’ (t1)

    k2 = v2’ (t1) t1 = pending v1 + v2
  16. • CockroachDB のアーキテクチャ ◦ Range ごとに Raft Group を構成し合意 •

    分散トランザクションの必要性 ◦ SQL に伴う Raft Group をまたいだ操作 • Transaction Record による実装 ◦ データ + Transaction Record で 2 回の合意
  17. As a database that prides itself on geo-distributed use cases,

    we must strive to reduce the latency incurred by common OLTP transactions to near the theoretical minimum: the sum of all read latencies plus one consensus latency. CockroachDB RFC: Parallel Commits
  18. 0

  19. • AWS DynamoDB ◦ AWS での最初の採用、後に S3 などにも横展開 ◦ 「ゼロから

    2-3 週間で習得可能」 ◦ 「設計をデバッグする」と表現し浸透を図る • Azure Cosmos DB ◦ 5 つの整合性レベルの仕様を厳密に記述
  20. • TiDB / TiKV ◦ Percolator、Multi-Raft Merge、TiCDC など ◦ Chaos

    Mesh との両面から分散システムを検証 • Elasticsearch ◦ レプリケーション、クラスタのメタデータ管理 ◦ 「3 日間のモデリングでバグを発見できた」
  21. • Temporal Logic of Actions と呼ばれる論理が基盤 ◦ IDE (TLA Toolbox)

    とセットで配布 ◦ Lamport (Paxos の人) が中心となって開発 • システムを状態遷移系として表現 ◦ 擬似プログラミング言語 PlusCal から生成可能 ◦ AWS の事例では PlusCal の有効性を強調
  22. 1. データと Transaction Record を並列で書き込み 2. ただしこの時点での Record の状態は Staging

    とし、 トランザクションに属するキーのリストも付ける 3. データと Record が合意して戻ってきたら クライアントにトランザクション完了通知を出す 4. 最後に Record の状態を Committed に変更
  23. k1 = v1 k2 = v2 k1 = v1’ (t1)

    k2 = v2’ (t1) t1 = staging : k1, k2 Round-1 Consensus
  24. k1 = v1 k2 = v2 k1 = v1’ (t1)

    k2 = v2’ (t1) t1 = staging : k1, k2 Round-1 Consensus
  25. k1 = v1 k2 = v2 k1 = v1’ (t1)

    k2 = v2’ (t1) t1 = committed : k1, k2 Round-2 Consensus
  26. k1 = v1 k2 = v2 k1 = v1’ (t1)

    k2 = v2’ (t1) t1 = committed : k1, k2 Round-2 Consensus
  27. 1. Intent を発見したら Transaction Record を確認 2. その Record が

    Staging だった場合、リストされている キーについて Intent が書き込み成功かどうか確認 3. 全キーが OK なら Record を Committed に変更 4. まだ書き込まれていないキーを見つけた場合は Conflict と判断して Record を Aborted に変更
  28. k1 = v1 k2 = v2 k1 = v1’ (t1)

    k2 = v2’ (t1) t1 = staging : k1, k2
  29. k1 = v1 k2 = v2 k1 = v1’ (t1)

    k2 = v2’ (t1) t1 = staging : k1, k2
  30. k1 = v1 k2 = v2 k1 = v1’ (t1)

    k2 = v2’ (t1) t1 = staging : k1, k2
  31. k1 = v1 k2 = v2 k1 = v1’ (t1)

    k2 = v2’ (t1) t1 = staging : k1, k2 v1’ + v2’
  32. k1 = v1 k2 = v2 k1 = v1’ (t1)

    k2 = v2’ (t1) t1 = committed : k1, k2
  33. k1 = v1 k2 = v2 k1 = v1’ (t1)

    t1 = staging : k1, k2
  34. k1 = v1 k2 = v2 k1 = v1’ (t1)

    t1 = staging : k1, k2
  35. k1 = v1 k2 = v2 k1 = v1’ (t1)

    t1 = staging : k1, k2
  36. k1 = v1 k2 = v2 k1 = v1’ (t1)

    t1 = staging : k1, k2 (No k2 intent)
  37. k1 = v1 k2 = v2 k1 = v1’ (t1)

    t1 = aborted : k1, k2 v1 + v2
  38. • 暗黙的コミット済み状態(読み取り可能状態) ◦ Transaction Record が Staging 状態 ◦ かつ全てのキーについて

    Intent が書き込み成功 • 明示的コミット済み状態 ◦ Transaction Record が Committed 状態 ◦ Parallel Commit 導入前と同じ、安全側の条件
  39. • 安全性 (Safety) ◦ 何か悪いことが「起こらない」ことを要求 ◦ 実行中、常に有効なアサーションのようなもの • 活性 (Liveness)

    ◦ 何か良いことがいつかは「起こる」ことを要求 ◦ 何もしないシステムは無意味なので検証には必須
  40. • 通常の論理式に以下の記号を追加した体系 ◦ □A:現在の状態から先では常に A が真 ◦ ◇A:現在の状態から A が真になるルートが存在

    • 状態の「列」に対して真偽が決まる ◦ 一連の実行の様子に対して条件を定義できる ◦ 真偽の与え方は CTL、LTL などいくつか存在
  41. • Parallel Commits のプロトコル ◦ Staging 状態の導入と Transaction Recovery •

    時相論理式の導入 ◦ 時間的な幅を持った実行列に関する仕様を検証 • ランダム実行ではなく分岐の網羅 ◦ 障害の際にもプロトコルが正しく動くかを検証
  42. • CockroachDB と Parallel Commit ◦ 一貫性を保ったままパフォーマンスを改善したい • 分散システムのテスト困難性 ◦

    動作順・故障・通信のランダムネス • 形式手法を利用したシステムの記述や検証 ◦ より厳密な仕様の理解と膨大なパターン網羅
  43. We found that the process of writing this specification gave

    us more confidence in the Parallel Commit protocol itself and in its integration into CockroachDB. Parallel Commits: An Atomic Commit Protocol For Globally Distributed Transactions