サーバーレスコンピューティングの形式化 #サーバーレスアーキテクチャ

はじめに

この記事は、OOPの国際学会¹ OOSPLA'19 で発表され、 distinguished paper award を受賞した Formal foundations of serverless computing (Jangda et al.) の解説記事です。
分析ぽい話でも開発っぽい話でも運用っぽい話でもないです。

発表の様子はYoutubeに投稿されています。

なお、この記事は簡単な操作的意味論の知識を前提とします。知らない方はこちらがオススメです → https://www.amazon.co.jp/dp/4781912850

サーバーレスコンピューティングとは

サーバーレスコンピューティングは、プログラマが外部イベントにより動作する関数を書いてデプロイするだけで、クラウド内部でリソースの確保やロードバランシング、スケーリングやリトライを自動で行い、動作環境を提供するプラットフォームで行なわれる計算処理です。大手クラウドでも、AWS Lambda、Google Cloud Functions、Azure Function という名前でサービスが提供されています。

しかしながら、スケーラブルなアプリを簡単に構成できるサーバーレスコンピューティングにも、それ特有の問題があります。たとえば、

関数の実行後にランタイムが破棄されうるので永続的な状態を持てない。→外部のDB等を使う必要がある。
自動スケーリングにより、同一の関数が並列で実行されうる。→ トランザクション等が必要となる。
リトライ機構などにより、一つのイベントに対して関数が複数回呼ばれる可能性がある(at-least-once) → 関数を羃等(idempotent)にする必要がある。

などが挙げられます。

cold vs. warm

1について補足です。サーバーレスプラットフォームでは、レイテンシ削減のため、ランタイム(コンテナ)を使いまわすことがあります。これはキャッシュやコネクションプールなどの実装に有用です。Cloud Functionsのドキュメントにもこう書かれています。

Cloud Function の状態は、将来の呼び出しのために必ずしも保持されるわけではありません。しかし、Cloud Functions が以前の呼び出しの実行環境をリサイクルすることはよくあります。変数をグローバルスコープで宣言すると、その値は再計算せずに後続の呼び出しで再利用できるようになります。

// Global (instance-wide) scope
// This computation runs at instance cold-start
const instanceVar = heavyComputation();

/**
 * HTTP function that declares a variable.
 *
 * @param {Object} req request context.
 * @param {Object} res response context.
 */
exports.scopeDemo = (req, res) => {
  // Per-function scope
  // This computation runs every time this function is called
  const functionVar = lightComputation();

  res.send(`Per instance: ${instanceVar}, per function: ${functionVar}`);
};

ヒントとアドバイス | Cloud Functions のドキュメント

上のコメントにもあるように、ランタイムを生成して初回起動することを cold start、使いまわして起動することをwarm startと呼びます。

操作的意味論 $λ_λ$

上記の性質を反映した操作的意味論 $λ_λ$² を図のように定義します。(図は論文より引用、以降登場する図も同論文より引用)

Serverless Functions

実行される側。サーバーレス関数 $f$ に対する操作は以下の3つの関数で構成される。

ランタイムの初期状態を生成する関数 $\mathsf{init}_f$。
プラットフォームからリクエストを受けとってランタイムの状態を返す関数 $\mathsf{recv}_f$
ランタイムの実行を表す関数³ $\mathsf{step}_f$。プラットフォームにコマンドを送ることができる。ここではレスポンスを返すコマンド $\mathbf{return}(v)$ のみ。

Serverless Platform

実行する側のクラウドプラットフォーム。プラットフォームの状態 $\mathcal{C}$ は、実行中(busy)/待機中(idle)の関数(ランタイムのインスタンス)、待機中のリクエスト、および関数からのレスポンスの集合で表現されます。

推論規則

$λ_λ$ の遷移のルールは6つあります。⁴

REQ: リクエストを「待機中のリクエスト」としてプラットフォームの状態に追加する。
COLD: cold start を行う。リクエストに応じて初期状態 $\sigma$ でインスタンスを生成 (インスタンスID= $y$ ) して実行状態(busy)にする。
WARM: warm start を行う。待機(idle)状態にある既存のインスタンスに対し、入ってきたリクエストに応じた状態 $\sigma'$ に置き換えて実行(busy)状態にする。
HIDDEN: 関数の内部実行(ステップ)はプラットフォームから観測不可能。
RESP: return コマンドが発行されたら、レスポンスを生成し、インスタンスの状態を idle にする。
DIE: ランタイムのインスタンスを破棄。

$λ_λ$ の表現力

この規則により、サーバーレスコンピューティングの以下のような性質を表現できます。

任意のタイミングでインスタンスが終了する (そして、リトライ実行が行われる)
- DIEルールは無条件で適用されうる。また、DIEしてもリクエストが消えることはない。(再実行可能)
1つのリクエストに対して複数のインスタンスが立つことがある (たとえ既にリクエストが実行中であっても)
- 一度COLD/WARMが適用されても、リクエスト $\mathbb{R}(f,x,v)$ は $\mathcal{C}$ に残っているため、COLD/WARMは何度でも適用できる。
内部状態を使い回したインスタンスの再利用 (warm-start)
- WARMルール
1つのリクエストに対して、1つのレスポンスが返る。
- RESPが一度適用されると、リクエスト $\mathbb{R}(f,x,v)$ は $\mathcal{C}$ から消えるので、リクエストID $x$ については RESP ルールがふたたび適用されることはない。

Naive Semantics

$\lambda_\lambda$ は、サーバーレスプラットフォームの詳細な特性を反映できていますが、cold/warm-startや同時実行などの概念はプログラムを書くうえでは困難となってきます。そこで、それらを排除したもっとシンプルで直感的なサーバーレスコンピューティングの意味論 naive semantics を考えます。

naive semantics は以下のものから構成されます。

実行される関数 $f$
ランタイムの実行/待機状態のモード $m$
関数の内部状態のトレースの配列 $\overrightarrow{\sigma}$
まだ返していないレスポンスのバッファ (キー:インスタンス名) $\mathcal{B}$

また、推論規則は4つになりました。

N-START: 待機(idle)状態にあるランタイムを実行(busy)状態にする。
N-STEP: 実行(busy)状態にある関数の実行を進める。
N-BUFFER-STOP: 実行の結果(レスポンス)を取得しバッファに格納、実行(busy)状態にある関数を待機(idle)状態にする。
N-EMIT-STOP: レスポンスをバッファから出力する。

Naive semantics と $λ_λ$

Naive semantics の世界では、1つの関数が1度に1回のリクエストを処理します。そのため、同じ関数の同時並列実行が起きることがありませんし、at-least-onceではなくexactly-onceを前提とできます。また、インスタンスのcold/warmの区別もなく、ランタイムのライフサイクルについて考える必要もなくなりました。

ただ、残念ながら全てのサーバーレスの関数がこれで意味付けできるわけではありません。関数の内部状態が次に述べる safety relation というものを満たしたとき、 $λ_λ$ は naive semantics の上で"動く"ことができます⁵。

ある内部状態にある関数が、次のステップで同値な内部状態になり、(あれば)同一のコマンドを出力する。
最後の内部状態が最初の内部状態とで同値となる。

ここでいう同値とは、状態同士の同値関係で、プログラムの性質によって自分で定義します。

safety relationの例として、以下のようなキャッシュを用いたログインシステム⁶について考えます。

var cache = new Map();
var USERS = {'hoge': 'pass1', 'fuga': 'pass2', ...};
function auth(req, res) {
    let {user, pass} = req.body;
    if(cache.contains(user, pass)) {
        res.write(true);
    } else if(USERS.get(user) === pass) {
        cache.insert(user, pass);
        res.write(true);
    }else{
        res.write(false);
    }
}

このプログラムの内部状態の同値関係を「キャッシュの状態を無視した状態の同値」と定義すると、safety relationを満たします。というのも、このプログラムの場合、キャッシュヒット/ミスにかかわらず同じ結果を返し(条件の1つ目の後半)、キャッシュを無視しているのでこのプログラムの状態は常に同一と言えるからです(条件の1つ目の前半と2つ目)。

総括すると、上のログインプログラムのような safety relation を満たすプログラムは、$λ_λ$でも naive semantics の性質を満たします。つまり、同時実行や中断によるリトライによる不整合、cold/warmの違いなどを考えることから解放されます。

なお、詳細な形式的な議論については論文を参照ください。

永続化データベースとの統合

サーバーレスプラットフォームでは状態は消失しうるため、永続的にデータを保存する場合は外部のDBサービスを用います。AWSだとDynamoDB、GCPだとDataStoreなどのKey-value storeが候補として挙げられます。
論文の5章では、$\lambda_\lambda$ に KV store とトランザクションのプリミティブ (read, write, begin, commit, rollback) を追加した拡張モデルを定義します。また、naive semantics についても同様の拡張を行い、その上で $\lambda_\lambda$ + KV と naive semantics + KV が特定の条件を満たせば一致するようになることを示しています。

ここでは詳細は割愛しますが、全てのリクエスト $\mathbb{R}(f,x,v)$ に対し、

関数 $f$ は、もし存在するならキー $x$ の値を出力する。
$f$ がトランザクションを完了したら、レスポンスをキー $x$ に保存する
$f$ が停止したら、レスポンスを出力する。

という条件 + safety relation を満たすと、2つのモデルは一致します⁵。簡単にいうと、トランザクションの中でレスポンスをリクエストIDをキーとしてKVSに書けばよい、ということです。⁷

サーバーレス関数の合成

サーバーレスと同時に言及されがちなのが、「マイクロサービス」という言葉です。小さな独立した関数を作り、それらを合成して大きな処理とするのは良いアイデアで、サーバーレスアーキテクチャと親和性が高いです。

関数の合成の一番簡単な方法としては、関数の中で他の関数を呼ぶことですが、これは多くのサーバーレスプラットフォームでは二重の課金が発生してしまいます。

function main(){
   sub(123);
   sub(456);
}
のような関数では、以下のようなフローになる。$$$$の部分が課金される。

sub:       +$$$$$$$$$+        +$$$$$+
          /           \      /       \
main: +$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$+

これを回避する方法としては、メッセージングサービスを利用して他の関数を呼び出したり(invoke後に自身が終了すれば課金されない)、Step functionのようなコーディネーションサービスを用いるというものがあります。ただ、この方法は時間的なオーバーヘッドが生じる上、そのサービス自体の追加の課金が発生します。

かといって、全ての関数を一つのソースに手動でまとめるというのも、当初のマイクロサービスの発想に反してしまいます。そこで、サーバーレスプラットフォーム自体に合成する機能を追加するアイデアが出てきます。

SPL: Serverless Platform Language

ここで、SPL というドメイン特化言語が登場します。これは、関数プログラミングの概念である Arrow をコンセプトに作られました。
SPL自体は、関数のソースコードとは別に、設定ファイルのように書かれる言語です。サーバーレスプラットフォームはそれを認識して関数呼び出しを行います。
SPL を $\lambda_\lambda$ に導入してみましょう。

SPLには3つの式があります。

$\mathsf{invoke}\,f$: $f$ を実行する
$\mathsf{first}\,e$: タプルの1番目を実行し、2番目をそのまま返す。
- first (v1,v2) = (f v1, v2)
$e_1 \ggg e_2$: 順次実行

後に出てくる実装では、これの他にもループや分岐などが実装されているらしいです。

上の図はSPLで拡張したルールです。詳細は述べませんが、この定義はSPLのインタプリタ⁸となっており、サーバーレスプラットフォーム自体が言語を解釈し実行を行なっていることが分かります。

ただ、実用上の問題から、これらに加えてJSONの式を解釈/構成できるようなものをSPLにサブ言語として導入しています。(論文 Fig.12 を参照)

これらを踏まえSPLの例を見てみます。

first(invoke f) >>> [in[1], in[0]] >>> first(invoke g)

これは、入力として長さ2の配列 [in_1, in_2] を取り、それぞれに関数 f, g を適用させた結果を返す処理を記述しています。

一方、Haskellを知ってる方はご存知かもしれませんが、Arrow syntax⁹を用いれば以下のように書けます。

x <- invoke f(in[0]);
y <- invoke g(in[1]);
ret [y,x];

こちらの方が直感的ですね。

実装

実際にSPLがOpenwhiskというOSSのサーバーレスプラットフォームに実装されています。

https://github.com/plasma-umass/openwhisk
https://github.com/plasma-umass/spl

論文の最後では、Openwhiskに元々あるコーディネーション機能のConductorと比較しており、レスポンス時間がSPLが良いという結果となっています。

おわりに

プログラミング言語の研究、とくに意味論や型理論などの理論寄りの研究は、普通のプログラマがその成果を享受できるのか疑問に思っている方もいらっしゃるのではないでしょうか。この論文は「サーバーレスコンピューティング」という産業上重要な要素を理論的に分析した上で、それを実装に落としこみ優れたパフォーマンスを発揮している点で「プログラミングにおける実用的な理論研究」として非常に興味が魅かれるものと思っています。

参考文献

Formal foundations of serverless computing Jangda et al., OOPSLA’19
Formal foundations of serverless computing - the morning paper

OOP といいつつ、プログラミングシステム全体のテーマを扱っています。 ↩
実際はsubscriptがAWSのロゴっぽくなってます。 ↩
正確には、関数と状態を受けとり、新しい状態とコマンド(optional)を返す関数。 ↩
$C \Rightarrow C\mathbb{R}(f,x,v)$ は $C \Rightarrow C \cup \lbrace \mathbb{R}(f,x,v) \rbrace$ のことだと考えられます。$\Rightarrow$ の上にいるのは、 transition label です。 ↩
naive semantics と $λ_λ$ が弱双模倣的(weakly bisimilar)である。 ↩
セキュリティ的なアレは無視してください ↩
extended naive semantics を見ると、1txが終了すると停止するように見えます(要検証) ↩
CK machine で、$\mathbb{E}(e, \kappa)$ における $\kappa$ が継続です。変数がないのでCEKのE抜き。 ↩
https://www.haskell.org/arrows/syntax.html ↩