こんにちは、チェシャ猫です。
先日開催された AWS Dev Day 2022 Japan で、サーバーレスコンピューティングの形式化について発表してきました。公募 CFP 枠です。
ちなみに会場は観葉植物が生い茂る Amazon 品川オフィスで、講演者向けには個室の楽屋が用意されており（滞在時間は講演直前の 15 分程度ですが）、全体的にとてもゴージャスな感じでした。配信設備も本格的でしたが、話す側としては照明が眩しくてやりづらかったです。
講演概要
AWS Lambda を初めとするサーバーレスコンピューティング基盤には、
- 複数の関数が同時に実行され共有リソースにアクセスしうる、本質的に並行システムである
- Warm Start により関数インスタンスが内部状態を残したまま再利用されうる
- 一つのリクエストに対して複数回の実行が行われうる、いわゆる At-Least-Once 特性
といった特性があり、通常のプログラムと比較して実行モデルが複雑かつアンコントローラブルな要素を多く含みます。関数を実装する側はこのような「プラットフォームの都合」を考慮して冪等性など細かい挙動に気を配りつつプログラムを書くことになり、これは一般にかなりの実装コストになります。また、アンコントローラブルな要素は、関数の実装から実際の挙動を静的に検査することを難しくしています。
このような問題に対して、Jangda らは 2019 年、サーバーレスコンピューティング自体に形式的な基礎付けを与えた論文 "Formal Foundations of Serverless Computing" を発表しました。今回の講演はこの論文、特に前半部分に焦点を当てたものです。上記の「プラットフォームの都合」を織り込んだサーバーレスの意味論、およびより直感的な挙動を表現した単純化された意味論の 2 種類を定義し、両者が弱双模倣の関係となる条件を記述するところまでを解説しました。
今回の講演の主眼は論文紹介ではありますが、あくまでも計算機科学に馴染みがない参加者に向けたものであり、「操作的意味論とは」といった入門者向けの内容も含め解説しています。参加者の次のステップにつなげてもらおうという意図から、最後には「次に読む本」としてプログラム意味論関係の参考書をいくつか挙げました。
スライド冒頭でも述べていますが、普段この分野に縁遠い方が、講演をきっかけに「ちょっと本でも読んでみるか」となればチェシャ猫の勝利です。以上、よろしく。
次に読むおすすめ書籍
Twitter の反応
「サーバーレスは操作的意味論の夢を見るか？」めちゃくちゃすげえこと言ってる。面白すぎる。アーカイブって出るのかな？#AWSDevDay
— なべ (@iho9z2qywfzt20w) 2022年11月10日
11月中読破目指す pic.twitter.com/sIqnh4iYxO
— なべ (@iho9z2qywfzt20w) 2022年11月15日
#AWSDevDay Eトラックやべー。
— mashiike (@mashiike) 2022年11月10日
この論文の解説が偉大すぎる
#AWSDevDay 意味論ほぼ初見だから頭爆発するかと思ったけどメチャクチャ面白いなコレ……。
— 吉村美代 (@myonyomu) 2022年11月10日
【E-2】サーバーレスは操作的意味論の夢を⾒るか。内容がほぼ理解出来ない俺は悪夢を見た気がする。とりあえず、おすすめ書籍をポチるか・・。記憶しているセッションで一番の衝撃だった #AWSDevDay
— Makoto Tezuka (@tezu33) 2022年11月10日
参考文献
- Abhinav Jangda, Donald Pinckney, Yuriy Brun, and Arjun Guha. 2019. "Formal foundations of serverless computing." Proc. ACM Program. Lang. 3, OOPSLA, Article 149 (October 2019), 26 pages.
- Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, Fabrizio Montesi, Marco Peressotti and Stefano Pio Zingaro. 2019. "No more, no less - A formal model for serverless computing." COORDINATION.
- Matthew Obetz, Anirban Das, Timothy Castiglia, Stacy Patterson, and Ana Milanova. 2020. “Formalizing Event-Driven Behavior of Serverless Applications.” In Service-Oriented and Cloud Computing, 19–29. Springer International Publishing.
- 五十嵐淳 (2011). プログラミング言語の基礎概念. サイエンス社.
- 小林直樹, 住井英二郎 (2020). プログラム意味論の基礎. サイエンス社.
- Tom Stuart (2013). Understanding Computation. O'Reilly Media, Inc. 邦訳あり
