なぜ「決定性」が 決定的に重要なのか？ Durable Execution 基盤の数理的理解 #serverlessjp / ServerlessDays Tokyo 2026

Serverless Days Tokyo 2026 で使用したスライドです。

Transcript

1. #serverlessjp チェシャ猫 (@y_taka_23) ServerlessDays Tokyo 2026 (19th Sep. 2026) なぜ「決定性」が 決定的に重要なのか？ Durable Execution 基盤の数理的理解
2. 本日のアジェンダ • お話しする内容 ◦ AWS Lambda Durable Functions の仕組みと性質 ◦ Durable Execution に対する 3 つのモデル ◦ 理論面から見た「決定性」の重要性 • 持ち帰ってほしい視点 ◦ 「どう使うべきか」を「なぜ正しいのか」から理解
3. 例：決済処理 • 注文情報を DynamoDB に保持している • 外部の決済 API を叩く ◦ ただし決済が失敗することがある ◦ その場合は 1, 3, 7, 14 日後にリトライ • 決済できたら領収書を送信 ◦ 宛先はメールと SMS の 2 箇所
4. Durable Functions • AWS Lambda の新しいプログラミングモデル ◦ 2025 年 12 月に GA、東京リージョンもサポート • ワークフローをプログラミング言語で記述 ◦ リトライ・待機・分岐などをロジックと結合可能 ◦ 最大 1 年待機が可能で、待機中は課金も中断 • 本イベント Day2 にワークショップあり
5. 自動リトライの単位を step で囲む ループや条件分岐 長時間の待機 並行処理の Fan-Out
6. wait 中は実際には 関数が起動していない （註：便宜上、1 日を 1 秒に短縮）
7. もし実行中にクラッシュしたら？
8. 決済 API ログ：リトライによる二重課金
9. 決済 API ログ：冪等性キーが異なり二重課金
10. リプレイと決定性 • エラーや wait で中断された場合 ◦ 中断された場所ではなく全体を最初からリプレイ ◦ すでに完了した step は結果を保存して再利用 • リプレイは決定的でなくてはならない ◦ 入力・保存値が同じなら同じフローの再現が必要 ◦ UUID や現在時刻など、非決定的な値は step に包む
11. 1 回目 2 回目 key = A key = B ✖ 再度 UUID を 振ってしまう
12. 1 回目 2 回目 key = A key = B ✖ 再度 UUID を 振ってしまう
13. 単に「step の中に入れる」だけだと うまくいかない場合もある
14. 1 回目 2 回目 key = A step が完了すれば 値が記憶される ✖
15. 決済 API ログ：正しい冪等実行
16. なぜ「決定性」が必要なのか？ 決定性によって何が保証されているのか？
17. Durable Functions: Semantics for Stateful Serverless S. Burckhardt, C. Gillum, et al. (OOPSLA 2021) https://doi.org/10.1145/3485510
18. Durable Serverless の厄介さ • 開発者にとって考えるべきことが実は多い ◦ 課題 1：プログラムの実行状態の引き継ぎ ◦ 課題 2：永続層への安全な読み書きの制御 ◦ 課題 3：同一処理の重複・並行起動 ◦ 課題 4：ビジネスロジックの並行実行と同期 • 論文では課題 1 + 課題 3 をターゲットとしている
19. 三つの実行モデル • 高レベルモデル ◦ エラー中断や二重起動がない、理想化されたモデル • Compute-Storage モデル（略記 C-S） ◦ 揮発性の計算ノード + 永続ストレージのモデル • Replay-Based モデル（略記 R-B） ◦ 引数・戻り値の履歴のみを永続化するモデル
20. 各モデル間の関係 定理（Burckhardt, et al., 2021, Theorem 5.3） 高レベルモデルと C-S モデルを比較すると、 C-S モデルの方が実現可能な挙動のパターンが狭い 定理（Burckhardt, et al., 2021, Theorem 6.4） C-S モデルと R-B モデルでは実現可能な挙動が等しい
21. つまり、Replay-Based モデルは 高レベルモデルの挙動を逸脱せず安全
22. システムの挙動とは何か？
23. インタプリタの意味論 • インタプリタの実行は状態遷移系とみなせる ◦ 状態：その時点の残りコード + 変数の値 ◦ 遷移：ステップ実行 • 遷移は書き換え規則として定義される ◦ 状態を式の形で表現する ◦ 現在の状態が規則にマッチしたら式を書き換える
24. インタプリタの実行
25. インタプリタの遷移規則（一部）
26. では挙動の逸脱とは何か？
27. 模倣と双模倣 • 二つの状態遷移系の挙動の「選択肢の幅」を比較 • 状態遷移系 S1 が S2 を模倣するとは： ◦ S1 の状態と S2 の状態になんらかの対応が付く ◦ S2 がどう遷移しても、S1 がそれに追従できる • 観測できない遷移を無視する場合、弱模倣と呼ぶ • 逆向きも模倣になっている場合、双模倣と呼ぶ
28. 高レベルモデルの意味論 • エラーや二重実行のない、理想化された「仕様」 • 状態 ◦ 場に存在する Durable Function と step のリスト ◦ それぞれの処理位置（インタプリタの場合と同じ） • 遷移規則 ◦ Durable Function や step の起動・完了・ステップ実行
29. 高レベルモデルの遷移規則（一部）
30. Compute-Storage モデルの意味論 • 揮発性の計算と、永続ストレージを分けたモデル • 状態 ◦ メッセージキューと実行状態を保存できる KVS • 遷移規則 ◦ 計算のステップ実行 ◦ ストレージへの Compare-And-Swap 的なコミット
31. 高レベルモデルと C-S モデルの関係 定理（Burckhardt, et al., 2021, Theorem 5.3） ストレージへのコミットのような内部遷移を隠蔽することで 高レベルモデルは Compute-Storage モデルを弱模倣する • つまり C-S モデルは高レベルモデルの挙動を逸脱しない • 高レベルモデルが「挙動の見本」として機能している
32. しかし「普通のプログラム言語」では 実行状態の取得や保存は基本、無理
33. Replay-Based モデルの意味論 • 実行状態の代わりに、入出力の履歴を保存するモデル • 状態 ◦ メッセージキューと in / out の列を保存できる KVS • 遷移規則 ◦ ステップ実行を行いつつ、in / out を履歴として記録 ◦ 履歴を消費してリプレイし、実行状態を復元する
34. C-S モデルと R-B モデルの関係 定理（Burckhardt, et al., 2021, Theorem 6.4） 履歴とそれをリプレイした結果の実行状態を対応させると Replay-Based モデルと Compute-Storage モデルとは 双模倣の関係にある • つまり R-B モデルは C-S モデルをお互いを真似できる • 状態遷移系として観測可能な挙動が区別できない
35. 決定性はどこで効くのか？
36. リプレイの決定性 補題（Burckhardt, et al., 2021, Lemma 6.5） 履歴がリプレイ可能であれば、その結果は一意的に定まる • R-B モデルを C-S モデルと結びつける上で最重要 • 逆に言えば、R-B モデルの定式化が「問題ない」ことは この性質が成り立っている範囲でしか主張できない
37. 例：UUID の非決定性 • step の外での UUID 生成 ◦ UUID が履歴として記録されない ◦ リプレイで復元した実行状態が同じにならない • 定理 6.4 の証明で使う補題 6.5 が満たされない ◦ R-B モデルが高レベルモデルの挙動に収まることが 必ずしも保証できなくなる
38. 本日のまとめ • AWS Lambda Durable Functions ◦ プログラムとして状態機械が記述できる ◦ 決定性を壊さないようにするのは実装者の責任 • Durable Functions の意味論と証明 ◦ 実行の進行を「状態」と「遷移規則」として定式化 ◦ 決定性の下で、リプレイは理想的な仕様を逸脱しない
39. The Worker Is Dead. Long Live the Workflow! Presented By チェシャ猫 (@y_taka_23)