AWS Dev Day 2022 Japan に「サーバーレスは操作的意味論の夢を見るか？」というタイトルで登壇してきました

こんにちは、チェシャ猫です。

先日開催された AWS Dev Day 2022 Japan で、サーバーレスコンピューティングの形式化について発表してきました。公募 CFP 枠です。

www.youtube.com

ちなみに会場は観葉植物が生い茂る Amazon 品川オフィスで、講演者向けには個室の楽屋が用意されており（滞在時間は講演直前の 15 分程度ですが）、全体的にとてもゴージャスな感じでした。配信設備も本格的でしたが、話す側としては照明が眩しくてやりづらかったです。

講演概要

AWS Lambda を初めとするサーバーレスコンピューティング基盤には、

複数の関数が同時に実行され共有リソースにアクセスしうる、本質的に並行システムである
Warm Start により関数インスタンスが内部状態を残したまま再利用されうる
一つのリクエストに対して複数回の実行が行われうる、いわゆる At-Least-Once 特性

といった特性があり、通常のプログラムと比較して実行モデルが複雑かつアンコントローラブルな要素を多く含みます。関数を実装する側はこのような「プラットフォームの都合」を考慮して冪等性など細かい挙動に気を配りつつプログラムを書くことになり、これは一般にかなりの実装コストになります。また、アンコントローラブルな要素は、関数の実装から実際の挙動を静的に検査することを難しくしています。

このような問題に対して、Jangda らは 2019 年、サーバーレスコンピューティング自体に形式的な基礎付けを与えた論文 "Formal Foundations of Serverless Computing" を発表しました。今回の講演はこの論文、特に前半部分に焦点を当てたものです。上記の「プラットフォームの都合」を織り込んだサーバーレスの意味論、およびより直感的な挙動を表現した単純化された意味論の 2 種類を定義し、両者が弱双模倣の関係となる条件を記述するところまでを解説しました。

今回の講演の主眼は論文紹介ではありますが、あくまでも計算機科学に馴染みがない参加者に向けたものであり、「操作的意味論とは」といった入門者向けの内容も含め解説しています。参加者の次のステップにつなげてもらおうという意図から、最後には「次に読む本」としてプログラム意味論関係の参考書をいくつか挙げました。

スライド冒頭でも述べていますが、普段この分野に縁遠い方が、講演をきっかけに「ちょっと本でも読んでみるか」となればチェシャ猫の勝利です。以上、よろしく。