デッドロックは実行時の問題であるはずだ。だからこそ厄介なのだ。コードはきれいにコンパイルされ、テストも通過し、そしてプロダクションでプロセスAがプロセスBを待ち、プロセスBがプロセスAを待つために動きを止めてしまう。

セッション型はこれを覆す。プロセス間の通信プロトコルを型システム自体にエンコードする。特定のクラスのデッドロックは、実行時の驚きではなくコンパイルエラーになり始める。デッドロックするコードを文字通り書くことができないのだ。

セッション型とは実際には何か

セッション型は通信チャネルのための型規律である。チャネルが、読み書きする型付けされていないパイプであるのではなく、セッション型付けされたチャネルは、その上で許可される操作の正確な順序を記述する型を持つ。

整数を送信し、次に文字列を受信し、最後に閉じる。コンパイラはこの順序を各ステップで追跡する。それから逸れると、実行時のデッドロックではなく型エラーが発生する。

このアイデアはプロセス計算から来ており、Haskell、Scala、OCaml、Rustに実装がある。Rustの所有権システムとアフィン型は、これを特に自然な適合にするが、この概念は言語に依存しない。

メッセージパッシングのデッドロックが実際に起こる仕組み

データを交換する必要のある2つのプロセスを考えてみよう。よくある間違いは次のようになる：

// Process A
tx1.send(data_a)?;
let result_a = rx2.recv()?;

// Process B
tx2.send(data_b)?;
let result_b = rx1.recv()?;

両方のプロセスが最初に送信を試みる。チャネルバッファがいっぱいの場合、両方とも送信でブロックされる。どちらもrecvに到達しない。これは古典的な通信ミスマッチによるデッドロックだ。

「単にそうしない」と思うかもしれない。しかし、数十のチャネル、条件ロジック、そして6か月後にリファクタリングされるコードが存在する実際のシステムでは、このパターンは常に忍び込む。型チェッカーは、送信と受信の順序が一貫しているかどうかについて意見を持たない。

セッション型がデッドロックを表現不可能にする方法

核心的なトリックは、セッション型がすべての操作後に変化することだ。チャネルは静的な型を持たない。使用後に別のものになる型を持つ。

以下は、このアイデアを実証するRustの最小限の実装だ：

use std::marker::PhantomData;

struct Send<T, Next>(PhantomData<(T, Next)>);
struct Recv<T, Next>(PhantomData<(T, Next)>);
struct Close;

struct Chan<P>(PhantomData<P>);

impl<P> Chan<P> {
    fn new() -> Self {
        Chan(PhantomData)
    }
}

impl Chan<Close> {
    fn close(self) {}
}

impl<T, Next> Chan<Send<T, Next>> {
    fn send(self, value: T) -> Chan<Next> {
        drop(value);
        Chan(PhantomData)
    }
}

impl<T: Default, Next> Chan<Recv<T, Next>> {
    fn recv(self) -> (T, Chan<Next>) {
        (T::default(), Chan(PhantomData))
    }
}

Chan<Send<i32, Recv<String, Close>>>型のチャネルは：まずi32を送信しなければならず、次にStringを受信できるチャネルを持ち、最後に閉じることのみができるチャネルを持つことを意味する。

sendメソッドは古いチャネルを消費し、更新された型を持つ新しいチャネルを返す。Rustの所有権システムがselfが消費されることを保証するため、古いチャネルを再度使用することはできない。コンパイラは2回送信したり、順序を無視して受信したり、閉じるのを忘れたりすることを許可しない。

デッドロックのシナリオでは、2つのエンドポイントを相補的な型で定義する：

type Client = Send<i32, Recv<String, Close>>;
type Server = Recv<i32, Send<String, Close>>;

fn client(ch: Chan<Client>) {
    let ch = ch.send(42);
    let (msg, ch) = ch.recv();
    println!("{}", msg);
    ch.close();
}

fn server(ch: Chan<Server>) {
    let (req, ch) = ch.recv();
    println!("{}", req);
    let ch = ch.send("hello".to_string());
    ch.close();
}

プロセスAは送信してから受信する。プロセスBは受信してから送信する。プロトコル型がこの順序を強制する。

誰かがプロセスBをリファクタリングして最初に送信しようとすると、コンパイラは即座に拒否する：

// This will NOT compile:
fn bad_server(ch: Chan<Server>) {
    // error: no method named `send` found for struct `Chan<Recv<...>>`
    let ch = ch.send("hello".to_string());
}

型システムは、このチャネルが受信状態にあると言う。送信はできない。デッドロックは表現不可能になる。

理論が複雑になる場所：分岐と再帰

実際のプロトコルは線形シーケンスではない。選択肢がある。サーバーは認証または登録を提供するかもしれない。セッション型は内部選択と外部選択の型でこれを処理する。

struct Credentials;
struct Token;
struct UserInfo;
struct Account;

enum AuthProtocol {
    Login(Send<Credentials, Recv<Token, Close>>),
    Register(Send<UserInfo, Recv<Account, Close>>),
}

クライアントが選択肢を提供し、サーバーが1つを選択する。両方のエンドポイントは選択に同意しなければならない。そうでなければ型が一致しない。

再帰的なプロトコル、例えばメニューに戻る永続的な接続は、再帰的な型定義を必要とする。ここでほとんどの言語が苦労する。Rustはこれをサポートするが、冗長になる。

多方問題もある。上記のセッション型は2値的だ：2つのエンドポイント。3つ以上のプロセスが調整する場合、多方セッション型が必要になり、これは大幅に複雑で、成熟した実装が少ない。

知っておくべきトレードオフ

セッション型はエラーのクラスを排除するが、すべてのデッドロックを排除するわけではない。すべてのプロセスが外部リソースを待つグローバルデッドロックや、プロセスが進展なしに回転するライブロックは依然として可能だ。セッション型は具体的に通信ミスマッチを対象とする。

また、コンパイル時のオーバーヘッドも導入する。深い型スタックからのエラーメッセージは不可解なことがある。単純なチャネル型のエラーが、コンパイラ出力で50行のネストされたジェネリクスに広がるかもしれない。Rustのエコシステムはここで改善されているが、セッション型のミスマッチのデバッグは依然として習得が必要なスキルだ。

動的トポロジーももう1つの痛みの源だ。セッション型は、通信グラフが静的でコンパイル時に既知である場合に最もうまく機能する。可変数の参加者を持つチャットルームのようなランタイムデータに基づいてチャネルを生成する場合、セッション型は適用がはるかに難しくなる。

今日これを試す方法

Rustでセッション型を試したい場合、session_typesクレートは元の理論に基づく成熟した実装を提供する。より人間工学的なAPIには、seshが別のアプローチを提供する。

Haskellでは、session-typesがHaskellの型レベルプログラミングで同様の保証を与える。産業利用に近いものを探しているなら、生成されたクライアントスタブを持つProtocol Buffersを見てみよう。形式的な意味でのセッション型ではないが、生成されたコードは同じ原則を強制する：プロトコルは外部で定義され、コンパイラは使用をそれに対してチェックする。

固定された通信プロセスのセットを持つ分散システムを構築している場合は、通信グラフを描くことから始める。すべてのメッセージに矢印を描く。グラフが複雑でミスマッチを心配する程度なら、そこでセッション型が報われる。

FAQ

セッション型はすべてのデッドロックを防ぎますか？

いいえ。両方とも送信を待つ2つのプロセスのような、通信ミスマッチによって引き起こされるデッドロックを防ぐ。リソースデッドロック、ライブロック、または外部システムを含むデッドロックは防がない。

セッション型とステートマシンの違いは何ですか？

セッション型は型システムにエンコードされたステートマシンだ。状態遷移は、実行時にチェックされるのではなく、すべてのチャネル操作でコンパイラによって強制される。

セッション型はプロダクションで使用されていますか？

二値セッション型は研究システムや専門分野で使用される。多方セッション型は依然として主に学術的である。これらの概念は、生成されたgRPCクライアントやRustの型状態パターンを含む、現代のAPI設計に影響を与える。

Rust以外でセッション型を使用できますか？

はい。Haskell、Scala、OCamlにはすべてセッション型ライブラリがある。アフィン型を持たない言語でも、線形型チェッカーやランタイムアサーションでパターンを近似できる。

デッドロックは今や型の問題だ

デッドロックは、型の問題にするまで実行時の問題だ。セッション型は万能薬ではないが、よく定義されたプロトコルを持つメッセージパッシングシステムでは、バグのクラス全体を「プロダクションでキャッチ」から「コンパイル時にキャッチ」に移動する。次に新しいサービスアーキテクチャをスケッチするときに検討に値するトレードオフだ。