Skip to content
Published on

型検査を通った二つのサービスが互いを待って止まるとき — コレオグラフィという別のアプローチ

🇰🇷KO🇺🇸EN🇯🇵JA🇨🇳ZH
Split View필사 모드
シェア
Authors

二つのサービスが互いを待って止まります

メモリ安全な言語でサービスを二つ作りました。両方ともコンパイルがきれいに通ります。ヌル参照も、データ競合も、解放後使用もありません。

ところがデプロイすると、ときどき二つが一緒に止まります。サーバーはクライアントが送るはずの二つ目のメッセージを待っており、クライアントはサーバーが先に応答するものと思って待っています。プロトコルが食い違ったのです。

このバグの特徴は、どちらのコードにも誤りがない点です。それぞれを別々に読めば両方とも合理的です。誤りは二つのあいだにあり、どのコンパイラもそのあいだを見ません。

問題の根は、コードが二つに分かれているという事実です

型システムが守ってくれる境界がどこまでなのかを考えると、理由は明白です。型検査器はひとつのコンパイル単位のなかで値の流れを見ます。その単位の外へ出た瞬間、すなわちバイトがソケットに載った瞬間からは、何も保証できません。反対側がそのバイトをどんな順序で期待しているのかは、検査器には知りようのない情報です。

そこで私たちはそのあいだを人の規律で埋めます。文書にシーケンス図を描き、スキーマを共有し、結合テストを書きます。三つとも有用で、三つとも検査ではなく慣行です。片方のコードを直しながら図を一緒に直さなくても、コンパイルは通ります。

この地点に別の答えを出す系統があります。あいだを検査するのではなく、そもそも二つに分けるなというものです。

コレオグラフィ — システム全体をひとつのプログラムとして書く

コレオグラフィプログラミングは、分散システムをプロセスごとに別々に書く代わりに、相互作用の全体をひとつの大域的な記述として書きます。クライアントがこれを送り、サーバーがあれを計算して返し、クライアントがそれを受け取るという流れが、ひとつのプログラムのなかで順に読めます。

この名前はFabrizio Montesiの2013年の博士論文で付き、以後いくつもの言語とライブラリがこの発想を実装してきました。概念の核心は視点の転換です。いま私たちが書くコードはひとつのノードの視点から書かれます。コレオグラフィはシステムの外から見下ろす視点で書きます。シーケンス図が実行可能になったものだと考えれば、おおむね当たっています。

エンドポイント射影がすること

大域的な記述をそのまま実行することはできません。実際に走るのは各ノードのプロセスだからです。そこでコンパイルの段階に手続きがひとつ足されます。エンドポイント射影です。

射影は、ひとつのコレオグラフィからノードごとのコードを機械的に取り出します。クライアント用のバイナリにはクライアントがすべき送信と受信と計算だけが残り、サーバー用のバイナリも同様です。二つの成果物は互いを知りませんが、同じ原本から出たので順序が食い違いようがありません。

ここで重要なのは、私たちがずっと手でやってきた作業がコンパイラの仕事になった点です。これまでクライアントのコードとサーバーのコードを合わせる作業は、人が図を見て両側に書き写すことでした。書き写す二度の作業が、ひとつの自動変換に変わります。

なぜデッドロックが設計上消えるのか

ここで誤解しやすい部分を押さえます。デッドロックが消えるのはコンパイラが賢いからではありません。そういうプログラムを書けないからです。

大域的な記述では、通信はひとつの構文で表現されます。誰が何を誰に送るという一行が、送信と受信を同時に生みます。送信だけあって受信がない状況や、双方が受信から始める状況を、ソースコードに書く方法がありません。ですから射影の結果にもそんな組み合わせは出てきません。

この性質は、CarboneとMontesiの2013年の仕事以降、設計上のデッドロック不在という表現で知られています。ただし範囲を正確に知っておく必要があります。この保証はプロトコルの食い違いから来るデッドロックについてのものです。ノードが死ぬ、ネットワークが切れる、無限ループに陥る、外部資源でロックが掛かるといった状況は別の問題です。

Wyzerがここに載せたもの

最近公開されたWyzerは、この発想をシステムプログラミングの側へ持ってこようとする試みです。READMEはこの言語を、静的型でコンパイルされる資源指向の言語として紹介し、コレオグラフィとPerceusのメモリモデルを結合したと述べています。

文法で目につくのは、型にノードが付くという点です。

role @Client;
role @Server;

fn fetch_data(query: str@Client) -> str@Client {
    // クライアントがサーバーへ query を渡す
    let server_query: str@Server = query;

    // サーバーが処理する
    let server_result: str@Server = db_lookup(server_query);

    // サーバーが結果をクライアントへ返す
    let client_result: str@Client = server_result;

    return client_result;
}

ここでネットワーク転送は別の関数呼び出しではなく別のノード型への代入です。そしてこの言語はその代入を線形な移動として扱います。すなわち渡した値は元の場所で消滅します。READMEが載せているエラーメッセージがその結果です。移したあとにもう一度使うと、移動した変数を使ったというコンパイルエラーが出ます。

この設計が狙っている地点は明白です。分散システムでよくあるバグのひとつが、すでに送ったデータをローカルでも最新であるかのように使い続けることであり、転送を移動にすればその間違いが型エラーになります。

借用検査器なしで所定位置の更新を得る側

メモリ側の選択も併せて見る価値があります。Wyzerはガベージコレクタも借用検査器も置かず、Perceusを選んだと述べています。

Perceusは2021年のPLDIで発表された技法で、参照カウントの増減命令をコンパイラが精密に挿入し、循環のないプログラムでゴミが残らないようにします。ここに再利用解析が載ると、ある値の参照がひとつだけのときに、新しく割り当てる代わりに既存のメモリをそのまま書き換えられます。関数型のスタイルで書いたコードが所定位置の更新へコンパイルされるこの方式をFBIPと呼びます。Koka言語に実装されています。

なぜこの組み合わせが自然なのかも押さえておく価値があります。コレオグラフィにおいて値がノードのあいだを移動するというのは所有権が移るという意味であり、所有権を数えることは参照カウントがすでにやっている仕事です。メモリとネットワークに同じ規則を使うというREADMEの設計原則はここから出ます。ただしこれは言語が掲げる設計意図であり、実際にその規則が両方の領域でうまく動くのかは、実装が出てから判断する問題です。

この言語の現在の状態をありのままに書けば

成熟度を誇張しないために、確認したことだけを書きます。リポジトリはApache-2.0ライセンスで、主要言語はOCamlです。確認した時点でリリースがひとつも上がっていません。 そして著者本人が公開記事で、五か月の研究と数週間の開発を経ており、まもなく0.1.0を出す予定だと述べています。つまり最初の版がまだ出ていない状態です。

ですからこの言語で何かを作る計画を立てる段階ではありません。それでも読む価値があると見る理由は、このプロジェクトがなぜ作ったのかを問題として記述しているからです。著者はRustへの不満から出発したと述べ、型検査はメモリを守ってくれるが分散デッドロックとサービス間のプロトコル不一致は守ってくれないという点を理由に挙げます。この診断は言語の完成度と関係なく正しいものです。そしてその診断への答えとして十年以上積み上がった学術的な系譜が存在するという事実こそ、このプロジェクトを見て得られるもっとも実用的な情報です。

まとめと出典

私たちがサービス間のプロトコルを文書とテストで合わせているなら、それは道具がないからではなく、私たちが使う言語がノードひとつしか見ないからです。コレオグラフィはその視野を変えるアプローチであり、視野を変えると一部のバグは直す対象ではなく表現できないものになります。

  • Choreographic Programming — Fabrizio Montesi本人の定義。用語が2013年の博士論文から出たという点、エンドポイント射影の役割、設計上のデッドロック不在がCarboneとMontesiの2013年の仕事で知られているという点を、この文書で確認しました。
  • Wyzer-Lang/wyzerリポジトリ — 文法の例、設計原則、エラーメッセージの形。本文のWyzerに関する記述とコードは、このリポジトリのREADMEから持ってきたものです。
  • リポジトリのメタデータで確認した事項: ライセンスApache-2.0、言語OCaml、リリースなし。0.1.0をまだ出していないという記述は、著者が公開した紹介記事の内容です。
  • Perceus: Garbage Free Reference Counting with Reuse — Reinking, Xie, de Moura, Leijen, PLDI 2021。FBIPと再利用解析の出典です。
  • 私はWyzerのコンパイラをビルドしたり実行したりしていません。本文のコードはREADMEに載っている例であり、動作を直接確認したものではありません。
Discuss on Twitter • View on GitHub