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

形式手法による分散システムの検証 #builderscon / builderscon tok...

y_taka_23
August 31, 2019

形式手法による分散システムの検証 #builderscon / builderscon tokyo 2019

builderscon tokyo 2019 で使用したスライドです。

本セッションでは、形式手法 (formal methods) を用いた分散アルゴリズムの検証について解説しました。形式手法は、数学的な表現を用いて対象となるシステムを定式化することにより、システムの挙動の「正しさ」を厳密に保証するための方法論です。

なお解説として取り上げたのは、AWS による事例論文でも有名なモデル検査器 TLA+ です。講演前半で形式手法の一般論に触れたのち、後半では分散トランザクションを実現するための TCC (Try-Confirm/Cancel) Pattern のモデリングと検証を行いました。

講演概要:https://builderscon.io/tokyo/2019/session/fa356ee3-6be9-4850-ac9e-037bd34aabaa
録画:https://www.youtube.com/watch?v=NkQ60iVyavA

y_taka_23

August 31, 2019
Tweet

More Decks by y_taka_23

Other Decks in Technology

Transcript

  1. #builderscon #bc100a とある決済サービスの仕様 • 統合された決済基盤 ◦ 複数の EC サイトから利用される •

    複数の決済手段をサポート ◦ 銀行引き落とし / ポイント払い / ギフト券 ◦ 各々が別のマイクロサービスとして稼働 ◦ 複数の手段に按分して支払うことも可能
  2. #builderscon #bc100a TCC パターン • 全体を二つのフェイズに分ける • Try フェイズ ◦

    あらかじめ更新内容を仮登録させる • Confirm / Cancel フェイズ ◦ 全員から OK が帰って来たら改めて Confirm ◦ 一箇所でも失敗した場合は全員 Cancel させる
  3. #builderscon #bc100a 分散システムは罠だらけ • 各ノードが非同期に動く ◦ 考えるべきパターンが多すぎる • ノードやネットワークが信頼できない ◦

    独立にランダムなタイミングで故障が発生 • 仕様そのものが複雑になりがち ◦ 特定の瞬間ではなく一連の動作が問題になる
  4. #builderscon #bc100a Chaos Engineering • 運用環境であえて障害を発生させる ◦ サービス不能状態に陥らないか ◦ 障害状態から正しく復旧できるか

    • 隠れていた問題点が炙り出せる ◦ 安定状態を「正しい」として差分を解析 ◦ 意図して発生させることが難しいバグも見つかる
  5. #builderscon #bc100a 第 1 章のまとめ • ナイーブな分散システムは危険 ◦ 整合性を保つビルトイン機能に頼れない •

    分散システムは考えることが多すぎる ◦ 実際に動かさずにテストするのは非現実的 • 実際に動かしてテストする手も ◦ 故障を注入することで問題点を発見する
  6. #builderscon #bc100a 形式手法とは • システムを数学的対象により表現 ◦ その対象の性質に基づいて検証を行う ◦ 対象として何を選ぶかでツールの性質が決まる •

    通常のテストと比較すると ◦ テストケースの抜けや漏れが生じない ◦ 実装ではなく仕様・設計に対して検査できる
  7. #builderscon #bc100a 形式手法の分類 • モデル検査 ◦ システムが取りうる値を列挙して探索 ◦ 有限個のパターンに収まれば自動化できる •

    定理証明 ◦ いわゆる数学的な証明をプログラム的に表現 ◦ 真に無限個の入力を扱うことができる
  8. #builderscon #bc100a TLA+ の特徴 • モデル検査系のツール ◦ 多機能な IDE とセットになっている

    ◦ Lamport (Paxos の人) が中心となって開発 ◦ Temporal Logic of Actions と呼ばれる論理が基盤 • システムを状態遷移系として定式化 ◦ 起こりうる動作の前後で成り立つ関係を記述
  9. #builderscon #bc100a TLA+ の採用事例 • AWS DynamoDB、S3 ◦ https://dl.acm.org/citation.cfm?id=2699417 •

    CockroachDB の並列コミット ◦ https://github.com/cockroachdb/cockroach/tree/master/docs/tla-plus • FINAL FANTASY XV POCKET EDITION ◦ DynamoDB の結果整合性が許容できるかどうか検査 ◦ https://d1.awsstatic.com/events/jp/2018/summit/tokyo/customer/37.pdf
  10. #builderscon #bc100a サンプル:LampLighter • まず非常に単純なシステムを考える • フラグが一つだけ存在する ◦ 変数名は lamp

    とする • プロセスが一つだけ稼働している ◦ 断続的にフラグを反転させる ◦ 式で書けば lamp = ~ lamp
  11. #builderscon #bc100a VARIABLE lamp (* 初期状態 *) Init == lamp

    = TRUE (* 状態遷移時の関係 *) Next == lamp' = ~ lamp
  12. #builderscon #bc100a サンプル:TwinLighter • フラグが二つ存在する ◦ 変数名は lamp1 と lamp2

    とする • プロセスが二つ並行して稼働している ◦ それぞれ P1 と P2 とする ◦ P1 は lamp1 を、P2 は lamp2 を反転させる ◦ ただし同時には片方しか動かない
  13. #builderscon #bc100a lamp1: false lamp2: true lamp1: false lamp2: false

    lamp1: true lamp2: true lamp1: true lamp2: false
  14. #builderscon #bc100a VARIABLES lamp1, lamp2 (* 初期状態 *) Init ==

    lamp1 = TRUE /\ lamp2 = TRUE (* 状態遷移時の関係 *) Next == lamp1' = ~ lamp1 \/ lamp2' = ~ lamp2
  15. #builderscon #bc100a VARIABLES lamp1, lamp2 (* 初期状態 *) Init ==

    lamp1 = TRUE /\ lamp2 = TRUE (* 状態遷移時の関係 *) Next == lamp1' = ~ lamp1 \/ lamp2' = ~ lamp2 状態 : 各パーツの論理積
  16. #builderscon #bc100a VARIABLES lamp1, lamp2 (* 初期状態 *) Init ==

    lamp1 = TRUE /\ lamp2 = TRUE (* 状態遷移時の関係 *) Next == lamp1' = ~ lamp1 \/ lamp2' = ~ lamp2 遷移 : 各パーツの論理和
  17. #builderscon #bc100a PlusCal の使用 • 生の TLA+ を書くのは人間には辛い ◦ というか「分散システムの難しさ」そのもの

    • 付属の DSL “PlusCal” からコード生成 ◦ Pascal 風の記法と C 言語風の記法がある • AWS の事例では重要な役割を果たした ◦ 現場のプログラマへの心理的障壁を下げる
  18. #builderscon #bc100a --algorithm LampLighter process P \in { 1,2 }

    variable lamp = TRUE; begin while TRUE do lamp := ~lamp; end while; end process end algorithm
  19. #builderscon #bc100a --algorithm LampLighter process P \in { 1,2 }

    variable lamp = TRUE; begin while TRUE do lamp := ~lamp; end while; end process end algorithm 普通のループっぽい記法
  20. #builderscon #bc100a --algorithm LampLighter process P \in { 1,2 }

    variable lamp = TRUE; begin while TRUE do lamp := ~lamp; end while; end process end algorithm 複数プロセスの生成
  21. #builderscon #bc100a 第 2 章のまとめ • 形式手法 ◦ システムを数学的な対象にマッピング ◦

    大きく分けて定理証明とモデル検査がある • 今回は TLA+ をモデル検査器として使用 ◦ 国内含み、興味深い産業界の事例がある ◦ PlusCal により「数学」は気にならない
  22. #builderscon #bc100a #builderscon #bc100a 分散システムのモデリング Model Our System With TLA+

    3 参考文献:http://muratbuffalo.blogspot.com/2018/12/2-phase-commit-and-beyond.html
  23. #builderscon #bc100a fair algorithm TCC fair process Payment = 0

    begin (* 決済サービス側の挙動 *) end process fair process Method \in METHOD begin (* 各決済手段側の挙動 *) end process end algorithm
  24. #builderscon #bc100a fair algorithm TCC fair process Payment = 0

    begin (* 決済サービス側の挙動 *) end process fair process Method \in METHOD begin (* 各決済手段側の挙動 *) end process end algorithm それぞれをプロセスとして合成
  25. #builderscon #bc100a 決済サービスの仕様 • まず Try リクエストを出す ◦ モデリングは Try

    した状態でスタート • 確定なら Confirm を指示 ◦ 全員が準備 OK 状態になった場合 • 取り消すなら Cancel の指示 ◦ 一人でも準備 OK にならなかった場合
  26. #builderscon #bc100a variables paymentState = "try"; fair process Payment =

    0 begin either (* confirm リクエスト発行 *) await canConfirm; paymentState := "confirm"; or (* cancel リクエスト発行 *) await canCancel; paymentState := "cancel"; end either; end process
  27. #builderscon #bc100a variables paymentState = "try"; fair process Payment =

    0 begin either (* confirm リクエスト発行 *) await canConfirm; paymentState := "confirm"; or (* cancel リクエスト発行 *) await canCancel; paymentState := "cancel"; end either; end process either A or B or … で 状態遷移の分岐を作る
  28. #builderscon #bc100a variables paymentState = "try"; fair process Payment =

    0 begin either (* confirm リクエスト発行 *) await canConfirm; paymentState := "confirm"; or (* cancel リクエスト発行 *) await canCancel; paymentState := "cancel"; end either; end process await で遷移するための 条件をかける
  29. #builderscon #bc100a define (* 全員が準備 OK なら確定できる *) canConfirm ==

    \A m \in METHOD : methodState[m] \in {"reserved"} (* ひとりでもキャンセルされていればキャンセルできる *) canCancel == \E m \in METHOD : methodState[m] \in {"canceled"} end define
  30. #builderscon #bc100a define (* 全員が準備 OK なら確定できる *) canConfirm ==

    \A m \in METHOD : methodState[m] \in {"reserved"} (* ひとりでもキャンセルされていればキャンセルできる *) canCancel == \E m \in METHOD : methodState[m] \in {"canceled"} end define forall: 任意の... exists: 少なくとも一つの...
  31. #builderscon #bc100a 決済手段サービスの仕様 • Try に対して準備動作を行う ◦ 待機状態の時 Try を受信すると準備状態に

    • Confirm に対して確定動作を行う ◦ 自分が準備状態なら確定する動作が可能 • Cancel に対してキャンセル操作を行う ◦ さらに自分自身が失敗した場合もキャンセル
  32. #builderscon #bc100a variables mathodState = [ m \in METHOD |->

    "idling" ]; fair process Method \in METHOD begin while methodState[self] in {"idling", "reserved"} do either (* idling -> reserved : 次ページ*) or (* reserved -> confirm : 次ページ *) or (* x -> canceled : 次ページ *) end either; end while; end process
  33. #builderscon #bc100a variables mathodState = [ m \in METHOD |->

    "idling" ]; fair process Method \in METHOD begin while methodState[self] in {"idling", "reserved"} do either (* idling -> reserved : 次ページ*) or (* reserved -> confirm : 次ページ *) or (* x -> canceled : 次ページ *) end either; end while; end process confirmed か canceled に なったら停止
  34. #builderscon #bc100a either (* idling -> reserved *) await methodState[self]

    = "idling"; methodState[self] := "reserved"; or (* reserved -> confirmed *) await methodState[self] = "reserved" /\ paymentState = "confirm"; methodState[self] := "confirmed"; or (* x -> canceled : 次ページ *) end either;
  35. #builderscon #bc100a either (* idling -> reserved *) await methodState[self]

    = "idling"; methodState[self] := "reserved"; or (* reserved -> confirmed *) await methodState[self] = "reserved" /\ paymentState = "confirm"; methodState[self] := "confirmed"; or (* x -> canceled : 次ページ *) end either; Confirm 命令
  36. #builderscon #bc100a either (snip...) or (* x -> canceled *)

    await methodState[self] = "idling" \/ (methodState[self] = "reserved" /\ paymentState = "cancel"); methodState[self] := "canceled" end either;
  37. #builderscon #bc100a either (snip...) or (* x -> canceled *)

    await methodState[self] = "idling" \/ (methodState[self] = "reserved" /\ paymentState = "cancel"); methodState[self] := "canceled" end either; Cancel 命令
  38. #builderscon #bc100a either (snip...) or (* x -> canceled *)

    await methodState[self] = "idling" \/ (methodState[self] = "reserved" /\ paymentState = "cancel"); methodState[self] := "canceled" end either; 自分自身が失敗したパターン
  39. #builderscon #bc100a 検証したい TCC の性質 • トランザクションとしての一貫性 ◦ Confirmed と

    Canceled が混在しないか? ◦ 混在すると不整合が発生する • 一連の手続きが完了する保証 ◦ いつかは Confirmed もしくは Canceled になる? ◦ デッドロックや無限ループに陥りたくない
  40. #builderscon #bc100a 安全性と活性 • 安全性 (Safety) ◦ 何か悪い状況が「起こらない」ことを要求 ◦ 通常の言語のアサーションに近い

    • 活性 (Liveness) ◦ 何か期待することが「起こる」ことを要求 ◦ 何もしないシステムは無意味なので検証に必須
  41. #builderscon #bc100a 時相論理 (Temporal Logic) • 通常の論理式に記号を追加した体系 ◦ [] A

    : 現時点以降、常に A が成り立つ ◦ <> A : 現時点以降、いずれ A が成り立つ • 状態の「列」に対して真偽を判定 ◦ 時間的な幅がある実行パスの性質に言明できる ◦ 真偽の与え方は何種類か (CTL, LTL など) 存在
  42. #builderscon #bc100a <> A : 現時点以降、いずれは A が成り立つ A true

    false [] A : 現時点以降、常に A が成り立つ A A A A A false true
  43. #builderscon #bc100a (* 確定されたになった決済手段と *) (* キャンセルになった決済手段が混在しない *) Consistency ==

    \A m1, m2 \in METHOD : ~ (methodState[m1] = "confirmed" /\ methodState[m2] = "canceled") (* どの決済手段もいつかは確定もしくはキャンセルになる *) Completed == <>(\A m \in METHOD : methodState[m] \in {"confirmed", "canceled"})
  44. #builderscon #bc100a (* 確定されたになった決済手段と *) (* キャンセルになった決済手段が混在しない *) Consistency ==

    \A m1, m2 \in METHOD : ~ (methodState[m1] = "confirmed" /\ methodState[m2] = "canceled") (* どの決済手段もいつかは確定もしくはキャンセルになる *) Completed == <>(\A m \in METHOD : methodState[m] \in {"confirmed", "canceled"}) 時相演算子
  45. #builderscon #bc100a 検証したい TCC の性質(再掲) • トランザクションとしての一貫性 ◦ Confirmed と

    Canceled が混在しないか? ◦ 混在すると不整合が発生する • 一連の手続きが完了する保証 ◦ いつかは Confirmed もしくは Canceled になる? ◦ デッドロックや無限ループに陥りたくない
  46. #builderscon #bc100a 第 3 章のまとめ • TLA+ による TCC のモデリング

    ◦ 一つ一つのコンポーネントごとに記述 ◦ どんな条件のときどんな動きをし得るかを整理 • 時相論理による検証 ◦ Confirmed と Canceled の両方は生じない ◦ いつかは Confirmed / Canceled のいずれかになる
  47. #builderscon #bc100a 決済サービスの故障 • 先ほどのモデリングは故障しない仮定 ◦ 分散システムの難しさが十分見えない ◦ 分散システムは故障を考慮してこその華 •

    Confirm または Cancel 命令後に故障 ◦ 故障後はいかなる命令も出さなくなる ◦ 故障後はずっと故障していて、復旧はしない
  48. #builderscon #bc100a エラートレースの内容 1. Try 命令が出されている状態 2. 決済手段サーバ 1 ->

    2 -> 3 の順で Try が到達し、 3 台とも Reserved 状態に 3. 決済サーバが Confirm 命令を出す 4. 直後に決済サーバが故障して沈黙 5. Confirm 命令は決済手段サーバに到達せず 6. 決済手段サーバが Reserved のままデッドロックに
  49. #builderscon #bc100a 故障しない 性質の良いシステム Crash-Stop 故障 : 故障後、完全に沈黙 Crash-Recovery 故障

    : 故障後、復活の可能性 ビザンチン故障:サーバが嘘をつく可能性 性質の悪いシステム
  50. #builderscon #bc100a フェイルオーバによる冗長化 • 決済サービスの代替サーバを準備 ◦ 代替サーバは故障しないと仮定する • 代替サーバの仕様 ◦

    決済サービス本体が故障に陥っていないか監視 ◦ 本体が正常なら何もしない ◦ 故障した場合は代わりに Confirm / Cancel 命令
  51. #builderscon #bc100a エラートレースの内容 1. Try 命令が出されている状態 2. 決済手段サーバ 1 ->

    2 -> 3 の順で Try が到達し、3 台とも Reserved 状態に 3. 決済サーバが Confirm 命令を出す 4. 直後に決済サーバが故障して沈黙 5. Confirm 命令は決済手段サーバ 1 にのみ到達し、 決済手段サーバ 1 のみが Confirmed 状態に 6. 「全員が Reserved」ではないので代替サーバは動けず
  52. #builderscon #bc100a 第 4 章のまとめ • 分散システムは故障時の挙動が重要 ◦ 正常系よりもずっとパターンが豊富 ◦

    そもそもそれが分散アルゴリズムの存在意義 • TLA+ による検査 ◦ 全探索により、仕様に合わない検出 ◦ 人間がぱっと思いつかない条件の漏れを指摘
  53. #builderscon #bc100a 本日のまとめ • 分散システムの設計は難しい ◦ すべての場合を網羅して考慮するのが困難 • 形式手法を用いて検証が可能 ◦

    モデル検査によるシステム状態の探索 • 様々な実行パターンに関する検証 ◦ 長く複雑な実行パスであっても自動で検出できる