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

サーバーレスアーキテクチャの数理的理解と分析 #devsumi / Developers Su...

サーバーレスアーキテクチャの数理的理解と分析 #devsumi / Developers Summit 2023 Summer

Developers Summit 2023 Summer で使用したスライドです。

サーバーレスアーキテクチャは強力ですが、同時に冪等性やトランザクションなど特有の考慮事項が必要であり、高い設計力が求められます。ところで、安全なプログラムを書く上で、静的型付き言語は広く利用されていますね。型はいわば実行前に間違いを検出できる仕組みであり、その背後には「プログラムの正しさ」を厳密な数式で記述し分析する理論が存在します。では、同様に「サーバーレスの正しさ」も厳密な数式で記述することは可能でしょうか?本講演ではAWS Lambdaを用いた設計を例として取り上げながら解説します。

イベント概要:https://event.shoeisha.jp/devsumi/20230727/session/4486/
ブログ記事:https://ccvanishing.hateblo.jp/entry/2023/07/27/195634

y_taka_23

July 27, 2023
Tweet

More Decks by y_taka_23

Other Decks in Technology

Transcript

  1. 今日お話しすること・しないこと • 明日からの仕事で役に立ったりはしません ◦ How-To の紹介でも設計フレームワークでもない ◦ 理論的な計算機科学の入門的内容が中心 • とはいえ

    Developer にとって無駄ではない(はず) ◦ 普段見るサーバーレス with ガチ理論の面白さ ◦ 聞いた後「参考文献読んでみるか」となると嬉しい
  2. 例:認証用のサーバーレス関数 function auth(req, res) { let (user, pass) = req.body;

    if (db.get(user) == pass) { res.write(true); } else { res.write(false); } }
  3. 例:ローカルキャッシュの導入 var cache = new Map(); function auth(req, res) {

    let (user, pass) = req.body; if (cache.contains(user, pass)) { res.write(true); } else if (db.get(user) == pass) { cache.insert(user, pass); res.write(true); } else { res.write(false); } }
  4. AWS Lambda のベストプラクティス • Take advantage of execution environment reuse

    ◦ SDK や DB コネクションはハンドラ外で初期化 ◦ /tmp ディレクトリにキャッシュを保存 ◦ ただしセキュリティ情報は保存しないように注意 • White idempotent code ◦ 重複したイベントでも同じように処理されるように https://docs.aws.amazon.com/lambda/latest/dg/best-practices.html
  5. サーバーレスの解析困難性 • 直感的には安全そうだが、どう確認するか ◦ 複数の関数が同時に実行されたら? ◦ Warm Start でインスタンスが再利用されたら? ◦

    At-Least-Once により複数回実行されたら? • 低レベルな「プラットフォームの都合」が露出 ◦ 言語の外の話なので Linter 等では役に立たない
  6. if 0 + 1 < 2 then 3 + (4

    + 5) else 6 + 7 = ?
  7. if 0 + 1 < 2 then 3 + (4

    + 5) else 6 + 7 = ?
  8. 言語の「意味」を定義する方法 • 実装による定義(かつての Ruby=MRI など) ◦ 参照実装を提供:正しさとはその実装との一致 • 自然言語による定義(C++、Java、ECMAScript など)

    ◦ 仕様書を提供:曖昧性や矛盾の発見は人間の観察力 • 形式的意味論による定義(Scheme、Standard ML など) ◦ 数学的ルールを提供:アルゴリズム的な検証が可能
  9. トイ言語の意味論(3/3) • "if e1 then e2 else e3" の形の式は、 e1

    の評価値に応じて e2 か e3 の評価値に評価される
  10. Big-step と Small-step • ここまでで見た規則は Big-step 意味論と呼ばれる ◦ すべての部分式を同時に値まで評価 •

    Big-step はサーバーレスと相性が悪い ◦ 複数の関数が並列で進行する途中経過こそが重要 ◦ イベントドリブンであり「値まで評価」はナンセンス • もう一つの Small-step 意味論で考える
  11. Small-step 意味論(3/3) • "if e1 then e2 else e3" の形の式は条件部分を先に簡約

    • 条件が true / false まで簡約されて初めて選択を行う
  12. 言語は構文のみに非ず • 構文が同じでも意味論が違えば別の言語 ◦ 例:遅延評価 vs 正格評価 • 意味論が妥当であることの保証も言語設計の一部 ◦

    計算結果が簡約順に依存したり途中で詰まったり ◦ 先程の Big / Small-step が等しいことも実は非自明 ◦ 理論付けた保証のために厳密な意味論が必要
  13. 形式的意味論の三分類 • 操作的意味論(Operational Semantics) ◦ 構文に対する書き換え規則により実行方法を定義 • 表示的意味論(Denotational Semantics) ◦

    意味論がより単純な対象への変換方法を定義 • 公理的意味論(Axiomatic Semantics) ◦ パーツごとの事前・事後条件と組み立て規則を定義
  14. 第 1 章のまとめ • 操作的意味論による言語の「意味」の定義 ◦ 構文と、その構文に対する変換規則を定める ◦ 言語の性質に対して厳密な議論が可能に •

    他の方式として、表示的意味論や公理的意味論がある ◦ 操作的意味論は実行(インタプリタ)に対応 ◦ 表示的意味論は翻訳・変換(コンパイル)に対応
  15. サーバーレスの意味論(3/6) • リクエスト R に対して Warm Start が発生 • idle

    だった既存の関数インスタンス F が busy に • リクエスト R はやはり関数起動後も残る(二重起動)
  16. サーバーレスの意味論(4/6) • 関数インスタンス F のプログラム f の実行が σ から σ’

    へ 1 ステップ進む • まだ return しておらず、式全体としては何も増えない
  17. サーバーレスの意味論(5/6) • 関数インスタンス F が return する • リクエスト R

    は消えてレスポンス S が出現 • 関数インスタンス F は busy から idle になり残る(再利用)
  18. 第 2 章のまとめ • サーバーレスプラットフォームの「構文」 ◦ 場に存在する関数インスタンスやリクエスト • サーバーレスプラットフォームの「意味論」 ◦

    関数インスタンスが 1 ステップずつ進む並行性 ◦ リトライによる At-least-once 実行 ◦ Warm Start による関数インスタンスの再利用
  19. ◯の遷移 a → b に対し □が遷移 a → b で

    追従(模倣)できない 動作パターンが存在 a b c a b c a 「同じ」とは言えない
  20. 関数インスタンスの内部状態 • 内部状態をどう扱うか? ◦ キャッシュを持つ関数は内部に状態が残る ◦ Warm Start 時に「完全に同じ状態」にはならない ◦

    外部から観測不能な差なら許容したい • 状態間に Safety Relation と呼ぶ「許容差」を定義 ◦ 処理中に許容差から逸脱しないことを保証したい
  21. Safety Relation(1/3) • 関数インスタンスの状態 σ の上に定義された同値関係 ≒ は 以下の条件を満たすとき Safety

    Relation であるという • リクエスト受信前に ≒ が成立すれば、受信後にも成立
  22. 単純化した構文との対応(概要) • 単純化側のレスポンスは元の側のリクエストに起因 • 関数インスタンスの状態は Safety Relation を除き対応 • この対応関係を

    A ≈ C で表す ◦ A は単純化された構文の式、C は元の構文の式 ◦ 論文だとちゃんと構成が書いてあるが今回は割愛 ◦ ≈ が Safety Relation を用いて定義される点が重要
  23. 単純化の正当性(Theorem 4.3) • 単純化側 A と元の側 C は、関係 ≈ を介し弱双模倣同値

    • 要するに、もし Safety Relation が存在するならば 関係 ≈ が定義でき、両者は外から見て区別できない
  24. 例:ローカルキャッシュの導入(再掲) var cache = new Map(); function auth(req, res) {

    let (user, pass) = req.body; if (cache.contains(user, pass)) { res.write(true); } else if (db.get(user) == pass) { cache.insert(user, pass); res.write(true); } else { res.write(false); } }
  25. 例:キャッシュ実装の理論的正当性 • 考慮したい状態:変数の値 + キャッシュ + DB 上の値 • キャッシュの差を無視した同一視は

    Safety Relation の 条件を満たす ◦ 数式で書くと「DB が変更されない」条件が現れる • 従ってこの実装は単純化された意味論で考えても OK で サーバーレス特有の事情の影響は受けない
  26. 第 3 章のまとめ • サーバーレスの意味論の単純化 ◦ 一旦サーバーレス特有の挙動を無視して単純化 ◦ 実行は一度に一つの関数のみ、Warm Start

    も無し • 元の意味論との対応関係 ◦ Safety Relation により特有の挙動による差を吸収 ◦ 元の意味論との間に弱双模倣の関係が成立する
  27. あなたが次に読む本(3/3) • アンダースタンディング・コンピュテーション ◦ Tom Stuart 著・笹田耕一 監訳・笹井崇司 訳 ◦

    オライリージャパン(2014) • Ruby で実装しながら計算機科学を学ぶ ◦ 手を動かして勘をつかむスタンス ◦ Chomsky 階層や停止性問題なども登場