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

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

本セッションでは、AWS Lambda の Durable Functionsを題材に、ワークフローを中断・再開可能にする仕組みと、その正しさを支える「決定性」について、数学の言葉を用いて解説します。

Durable Functions では、「途中で人間の承認を待つ」「失敗した処理を再試行する」「複数の処理を並列に実行する」といった複雑なワークフローを、通常のプログラムに近い形で記述できます。しかし、ドキュメントを読み進めると、ワークフローのコードには「決定性」が要求されていることに気づきます。現在時刻の取得、乱数、UUID の生成、外部 APIの呼び出しなどは決定性を破壊する要因であり、これらは実装者が注意して一つのステップの中に閉じ込める必要があります。通常のプログラムのように書けるという割には、ずいぶん神経質ですね。

では、この「神経質な実行基盤」によって、我々は何を得ているのでしょうか？

Durable Executionでは、中断時のメモリやコールスタックをそのまま保存する代わりに、完了した処理の履歴を保存します。再開時には関数を先頭から実行し直し、完了済みの処理について保存された結果を返すことで、過去の実行をリプレイします。このとき、最初の実行とリプレイされた実行が異なる分岐へ進んでしまえば、履歴から元の状態を復元できません。決定性は単なる SDK 上の制約ではなく、限られた履歴から中断前の実行状態を一意に復元するための条件なのです。

この仕組みに理論的な説明を与えるのが、Burckhardt らによる 2021 年の論文 “Durable Functions: Semantics for Stateful Serverless” です。論文では、決定的なワークフローについて、実行状態そのものを保存する方式と、履歴を保存して再生する方式とが、外部から観測できる範囲で同じように振る舞うことを数学的に証明しています。

本セッションでは、現在時刻や外部 API に依存するコードがリプレイ時にどのように破綻するかを、短いコード例と実行履歴を使って追跡します。また、「リプレイ時に同じ実行パスを通る」という決定性と、「処理が再試行されても結果が壊れない」という冪等性の違いも整理し、実務的なサーバレスの実装知識と論文の内容を接続・再構成して解説します。

受講にあたって必要なものは、サーバーレスを一度でも書いたことがある程度の知識と、ほんの少しの知的好奇心だけです。形式的意味論の前提知識は要求しません。便利な SDK の但し書きの背後には、障害に満ちたサーバーレス環境と通常のプログラムの世界を接続する、きちんとした数学があります。そしてそれは、普段コードを書いている他ならぬあなた自身とも、決して無関係の世界ではないことを知っていただけると幸いです。

イベント情報：https://tokyo.serverlessdays.io

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