Upgrade to Pro — share decks privately, control downloads, hide ads and more …

CockroachDB から覗く形式手法の世界 #CNDT2020 / CloudNative...

y_taka_23
September 09, 2020

CockroachDB から覗く形式手法の世界 #CNDT2020 / CloudNative Days Tokyo 2020

CloudNative Days Tokyo 2020 で使用したスライドです。

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

イベント概要:https://event.cloudnativedays.jp/cndt2020
ブログ記事:https://ccvanishing.hateblo.jp/entry/2020/09/10/044848

y_taka_23

September 09, 2020
Tweet

More Decks by y_taka_23

Other Decks in Technology

Transcript

  1. 本日お話しすること • CockroachDB の概要 ◦ スケーラビリティを実現するアーキテクチャ ◦ 生じた課題と Parallel Commit

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

    ◦ 旧来の RDB と異なりスケールアウト可能 • データは Node 間で冗長化される ◦ 一定規模以下の Node 障害時でもデータを守れる
  3. SQL Transaction Distribution Replication Storage SQL を Key-Value 命令に変換 トランザクション管理(本日メイン)

    適切な Node に命令をルーティング Node 間でデータを冗長化 データをディスクに永続化(省略)
  4. id (PK) author like 1 alice 4 2 alice 8

    3 bob 5 table: posts /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
  5. Node 2 Distribution Layer Node 3 Node 1 Range 1

    Range 2 Range 3 PUT k1 = v1 (k1 ∈ Range 1)
  6. Raft • 合意 (Consensus) プロトコル ◦ 一度、合意が得られればその値は覆らない • Leader Election

    ◦ 見本となる Node (Leader, LeaseHolder) を選択 • Log Replication ◦ 操作列について合意し leaseholder の状態を複製
  7. Node 2 Distribution Layer Node 3 Node 1 Range 1

    Range 2 Range 3 Range 1 Range 2 Range 3 Range 1 Range 2 Range 3
  8. Raft Consensus Groups 1, 2, 3 Range 1 (LH) Range

    2 Range 3 Range 1 Range 2 (LH) Range 3 Range 1 Range 2 Range 3 (LH) (LH = LeaseHolder)
  9. Node 2 Distribution Layer Node 3 Node 1 k1 =

    v1 PUT k1 = v1 (k1 ∈ Range 1)
  10. Node 2 Distribution Layer Node 3 Node 1 k1 =

    v1 k1 = v1 k1 = v1 Ack Success
  11. Range 2 Distribution Layer Range 3 Range 1 k1 =

    v1 PUT k1 = v1 (k1 ∈ Range 1)
  12. Range 2 Distribution Layer Range 3 Range 1 k1 =

    v1 PUT k1 = v1 (k1 ∈ Range 1)
  13. Distribution Layer Range 1 k1 = v1 PUT k1 =

    v1 (k1 ∈ Range 1) • 各 Range は Raft で可用性と一貫性が 保たれた一塊の DB とみなせる • Range 間にはコミュニケーションの 仕組みがない
  14. Range 2 Range 3 Range 1 k1 = v1’ k2

    = v2’ (合意待ち) Client 1 Client 2 k2 = v2
  15. Range 2 Range 3 Range 1 k1 = v1’ k2

    = v2 Client 1 Client 2 v1’ + v2 (?)
  16. Transaction Record 1. トランザクション開始時、Key-Value データと同様に Pending 状態の Transaction Record を書き込む

    2. データを書き込む際は上書きする代わりに、 Intent と呼ばれるマーカをつけ、Record を参照 3. 全てのデータ書き込みが成功したら Record の状態を Committed に変更することでコミット
  17. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2
  18. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ : t1 k2 = v2’ : t1 t1 = pending Round-1 Consensus
  19. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ : t1 k2 = v2’ : t1 t1 = pending Round-1 Consensus
  20. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ : t1 k2 = v2’ : t1 t1 = committed Round-2 Consensus
  21. Range 2 Range 3 Range 1 k1 = v1 k2

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

    Record が Pending 状態であれば元の値を採用 3. Record が Committed 状態であれば Intent として 保持されている値を採用
  23. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ (t1) k2 = v2’ (t1) t1 = pending
  24. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ (t1) k2 = v2’ (t1) t1 = pending
  25. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ (t1) k2 = v2’ (t1) t1 = pending
  26. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ (t1) k2 = v2’ (t1) t1 = pending v1 + v2
  27. 第 1 章のまとめ • CockroachDB のアーキテクチャ ◦ Range ごとに Raft

    Group を構成し合意 • 分散トランザクションの必要性 ◦ SQL に伴う Raft Group をまたいだ操作 • Transaction Record による実装 ◦ データ + Transaction Record で 2 回の合意
  28. 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 https://github.com/cockroachdb/cockroach/blob/master/docs/RFCS/20180324_parallel_commit.md
  29. 分散システムのテスト困難性 • マルチプロセスの問題 ◦ 動作する順番の全組み合わせを考える必要がある • 故障の問題 ◦ 個々の Node

    の動作にもランダム性がある • ネットワークの問題 ◦ 通信は遅延・消失し、順番も保存されない
  30. TLA+ の特徴 • モデル検査ツールとして使われることが多い ◦ IDE (TLA Toolbox) とセットで配布 ◦

    Lamport (Paxos の人) が中心となって開発 ◦ Temporal Logic of Actions と呼ばれる論理が基盤 • システムを状態遷移系として表現 ◦ 擬似プログラミング言語 PlusCal から生成可能
  31. CloudNative 界隈の TLA+ 人気 • AWS DynamoDB / S3 •

    Elasticsearch • Cosmos DB • TiDB • FINAL FANTASY XV POCKET EDITION ◦ DynamoDB の結果整合性が問題にならないか検証
  32. process user \in { "alice", "bob" } variables x =

    0; begin Get: x := like; Incr: x := x + 1; Put: like := x; Ack: acked_users := acked_users + 1 end process; CountOK == acked_users = 2 => like = 2
  33. process user \in { "alice", "bob" } variables x =

    0; begin Get: x := like; Incr: x := x + 1; Put: like := x; Ack: acked_users := acked_users + 1 end process; CountOK == acked_users = 2 => like = 2 プロセス alice と bob が並行に動く
  34. process user \in { "alice", "bob" } variables x =

    0; begin Get: x := like; Incr: x := x + 1; Put: like := x; Ack: acked_users := acked_users + 1 end process; CountOK == acked_users = 2 => like = 2 ラベルが一つの実行ステップを表し その間では他プロセスの割り込みが入る
  35. process user \in { "alice", "bob" } variables x =

    0; begin Get: x := like; Incr: x := x + 1; Put: like := x; Ack: acked_users := acked_users + 1 end process; CountOK == acked_users = 2 => like = 2 検査したい条件
  36. 第 2 章のまとめ • 分散システムをテストするのは難しい ◦ タイミングに依存したバグの再現性 • TLA+ による問題の発見

    ◦ 状態遷移系を網羅的に探索して条件を確認 • TLA+ が使用された事例 ◦ CockroachDB、Cosmos DB、TiDB など
  37. Parallel Commit 1. データと Transaction Record を並列で書き込み 2. ただしこの時点での Record

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

    = v2 Client 1 Client 2
  39. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ (t1) k2 = v2’ (t1) t1 = staging : k1, k2 Round-1 Consensus
  40. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ (t1) k2 = v2’ (t1) t1 = staging : k1, k2 Round-1 Consensus
  41. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ (t1) k2 = v2’ (t1) t1 = committed : k1, k2 Round-2 Consensus
  42. Range 2 Range 3 Range 1 k1 = v1 k2

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

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

    = v2 Client 1 Client 2 k1 = v1’ (t1) k2 = v2’ (t1) t1 = staging : k1, k2
  45. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ (t1) k2 = v2’ (t1) t1 = staging : k1, k2
  46. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ (t1) k2 = v2’ (t1) t1 = staging : k1, k2
  47. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ (t1) k2 = v2’ (t1) t1 = staging : k1, k2 v1’ + v2’
  48. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ (t1) k2 = v2’ (t1) t1 = committed : k1, k2
  49. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ (t1) t1 = staging : k1, k2
  50. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ (t1) t1 = staging : k1, k2
  51. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ (t1) t1 = staging : k1, k2
  52. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ (t1) t1 = staging : k1, k2 (No k2 intent)
  53. Range 2 Range 3 Range 1 k1 = v1 k2

    = v2 Client 1 Client 2 k1 = v1’ (t1) t1 = aborted : k1, k2 v1 + v2
  54. コミット状態の再定式化 • 暗黙的コミット済み状態(読み取り可能状態) ◦ Transaction Record が Staging 状態 ◦

    かつ全てのキーについて Intent が書き込み成功 • 明示的コミット済み状態 ◦ Transaction Record が Committed 状態 ◦ Parallel Commit 導入前と同じ、安全側の条件
  55. ImplicitlyCommitted == /\ record.status = "staging" /\ \A k \in

    KEYS: /\ intent_writes[k].epoch = record.epoch /\ intent_writes[k].ts <= record.ts ExplicitlyCommitted == Record.status = "committed"
  56. ImplicitlyCommitted == /\ record.status = "staging" /\ \A k \in

    KEYS: /\ intent_writes[k].epoch = record.epoch /\ intent_writes[k].ts <= record.ts ExplicitlyCommitted == Record.status = "committed" 任意の key ∈ KEYS に対し
  57. 安全性と活性 • 安全性 (Safety) ◦ 何か悪いことが「起こらない」ことを要求 ◦ 実行中、常に有効なアサーションのようなもの • 活性

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

    ◇A:現在の状態から A が真になるルートが存在 • 状態の「列」に対して真偽が決まる ◦ 一連の実行の様子に対して条件を定義できる ◦ 真偽の与え方は CTL、LTL などいくつか存在
  59. AckImpliesCommit == commit_ack => ImplicitlyCommitted \/ ExplicitlyCommitted ImplicitCommitLeadsToExplicitCommit == ImplicitlyCommitted

    ~> ExplicitlyCommitted AckLeadsToExplicitCommit == commit_ack ~> ExplicitlyCommitted 安全性
  60. AckImpliesCommit == commit_ack => ImplicitlyCommitted \/ ExplicitlyCommitted ImplicitCommitLeadsToExplicitCommit == ImplicitlyCommitted

    ~> ExplicitlyCommitted AckLeadsToExplicitCommit == commit_ack ~> ExplicitlyCommitted 活性
  61. AckImpliesCommit == commit_ack => ImplicitlyCommitted \/ ExplicitlyCommitted ImplicitCommitLeadsToExplicitCommit == ImplicitlyCommitted

    ~> ExplicitlyCommitted AckLeadsToExplicitCommit == commit_ack ~> ExplicitlyCommitted A ~> B (lead to) 一度 A が成立すると その後いつか B も成立
  62. AckImpliesCommit == commit_ack => ImplicitlyCommitted \/ ExplicitlyCommitted ImplicitCommitLeadsToExplicitCommit == ImplicitlyCommitted

    ~> ExplicitlyCommitted AckLeadsToExplicitCommit == commit_ack ~> ExplicitlyCommitted A ~> B == A => <>B
  63. プロセスの公平性 • 公平性なし(TLA+ のデフォルト) ◦ まったく動かない可能性がある • 弱い公平性の仮定(fair をつけた場合) ◦

    常に動ける状態ならいつか必ず動く • 強い公平性の仮定 ◦ 動ける瞬間が無限回来るならいつか必ず動く
  64. process committer = "committer" begin ... end process; fair process

    preventer \in PREVENTER begin ... end process;
  65. process committer = "committer" begin ... end process; fair process

    preventer \in PREVENTER begin ... end process; トランザクションの持ち主のプロセスが 任意のタイミングで Stall する分岐を生成
  66. process committer = "committer" begin ... end process; fair process

    preventer \in PREVENTER begin ... end process; それ以外のプロセスは、動ける状況が続けば 必ずどこかのタイミングでは動く
  67. PipelineWrites: while to_write /= {} do with key \in to_write

    do to_write := to_write \ {key}; ... end with; end while;
  68. PipelineWrites: while to_write /= {} do with key \in to_write

    do to_write := to_write \ {key}; ... end with; end while; Key を一つ取り出す際、 すべての「取り出し方」を 網羅して分岐を生成
  69. ... either Intent_writes[k] := [ epoch |-> txn_epoch, ts |->

    txn_ts, resolved |-> FALSE ]; or skip; end either; ...
  70. ... either Intent_writes[k] := [ epoch |-> txn_epoch, ts |->

    txn_ts, resolved |-> FALSE ]; or skip; end either; ... 二つのパターンのうち どちらが選ばれるかを両方考えて 分岐を生成
  71. ... either Intent_writes[k] := [ epoch |-> txn_epoch, ts |->

    txn_ts, resolved |-> FALSE ]; or skip; end either; ... 書き込みが成功したパターン
  72. ... either Intent_writes[k] := [ epoch |-> txn_epoch, ts |->

    txn_ts, resolved |-> FALSE ]; or skip; end either; ... 書き込みが失敗したパターン
  73. 第 3 章のまとめ • Parallel Commits のプロトコル ◦ Staging 状態の導入と

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

    ◦ 動作順・故障・通信のランダムネス • 形式手法を利用したシステムの記述や検証 ◦ より厳密な仕様の理解と膨大なパターン網羅
  75. 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 https://www.cockroachlabs.com/blog/parallel-commits/