「サーバーレスは操作的意味論の夢を見るか？ #AWSDevDay / AWS Dev Day 2022 Japan - Speaker Deck」

AWS Dev Day 2022 Japan で使用したスライドです。 AWS Lambda を初めとするサーバーレスコンピューティング基盤には、 * 複数の関数が同時に実行され共有リソースにアクセスしうる、本質的に並行システムである * Warm Start により関数インスタンスが内部状態を残したまま再利用されうる * 一つのリクエストに対して複数回の実行が行われうる、いわゆる At-Least-One 特性といった特性があり、通常のプログラムと比較して実行モデルが複雑かつアンコントローラブルな要素を多く含みます。関数を実装する側はこのような「プラットフォームの都合」を考慮して冪等性など細かい挙動に気を配りつつプログラムを書くことになり、これは一般にかなりの実装コストになります。また、アンコントローラブルな要素は、関数の実装から実際の挙動を静的に検査することを難しくしています。このような問題に対して、Jangda らは 2019 年、サーバーレスコンピューティング自体に形式的な基礎付けを与えた論文 "Formal Foundations of Serverless Computing" を発表しました。今回の講演はこの論文、特に前半部分に焦点を当てたものです。上記の「プラットフォームの都合」を織り込んだサーバーレスの意味論、およびより直感的な挙動を表現した単純化された意味論の 2 種類を定義し、両者が弱双模倣の関係となる条件を記述するところまでを解説しました。

AWS Dev Day 2022 Japan で使用したスライドです。 AWS Lambda を初めとするサーバーレスコンピューティング基盤には、 * 複数の関数が同時に実行され共有リソースにアクセスしうる、本質的に並行システムである * Warm Start により関数インスタンスが内部状態を残したまま再利用されうる * 一つのリクエストに対して複数回の実行が行われうる、いわゆる At-Least-One 特性といった特性があり、通常のプログラムと比較して実行モデルが複雑かつアンコントローラブルな要素を多く含みます。関数を実装する側はこのような「プラットフォームの都合」を考慮して冪等性など細かい挙動に気を配りつつプログラムを書くことになり、これは一般にかなりの実装コストになります。また、アンコントローラブルな要素は、関数の実装から実際の挙動を静的に検査することを難しくしています。このような問題に対して、Jangda らは 2019 年、サーバーレスコンピューティング自体に形式的な基礎付けを与えた論文 "Formal Foundations of Serverless Computing" を発表しました。今回の講演はこの論文、特に前半部分に焦点を当てたものです。上記の「プラットフォームの都合」を織り込んだサーバーレスの意味論、およびより直感的な挙動を表現した単純化された意味論の 2 種類を定義し、両者が弱双模倣の関係となる条件を記述するところまでを解説しました。

Webページ

コンテンツ文字数：0 文字

見出し数（H2/H3タグ）：0 個

閲覧数：81 件

2022-11-11 08:04:33

オリジナルページを開く

タグ一覧