데드락은 실행 시간 문제여야 한다. 그것이 데드락을 짜증나게 만드는 이유다. 코드는 깨끗이 컴파일되고, 테스트는 통과하며, 그런 다음 프로덕션에서 프로세스 A가 프로세스 B를 기다리고 프로세스 B가 프로세스 A를 기다리면서 멈춰 버린다.

세션 타입은 이를 뒤집는다. 프로세스 간 통신 프로토콜을 타입 시스템 자체에 인코딩한다. 특정 클래스의 데드락은 실행 시간의 놀라움이 아닌 컴파일러 오류가 되기 시작한다. 말 그대로 데드락을 일으키는 코드를 작성할 수 없다.

세션 타입이 실제로 무엇인가

세션 타입은 통신 채널을 위한 타입 규율이다. 채널이 읽고 쓰는 타입 없는 파이프가 아니라, 세션 타입이 지정된 채널은 허용되는 연산의 정확한 순서를 기술하는 타입을 가진다.

정수를 보내고, 문자열을 받고, 닫는다. 컴파일러는 이 순서를 매 단계에서 추적한다. 이에서 벗어나면 실행 시간 데드락이 아닌 타입 오류가 발생한다.

이 아이디어는 프로세스 계산에서 유래했으며 Haskell, Scala, OCaml, Rust에 구현이 있다. Rust의 소유권 시스템과 아핀 타입은 이를 특히 자연스러운 적합으로 만들지만, 개념 자체는 언어에 독립적이다.

메시지 전달 데드락이 실제로 발생하는 방식

데이터를 교환해야 하는 두 프로세스를 고려하라. 흔한 실수는 다음과 같다:

// 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가 소비되도록 보장하기 때문에 이전 채널을 다시 사용할 수 없다. 컴파일러는 두 번 보내거나, 순서를 무시하고 받거나, 닫는 것을 잊는 것을 허용하지 않는다.

데드락 시나리오에서는 두 엔드포인트를 보완적인 타입으로 정의한다:

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>>),
}

클라이언트가 선택을 제시하고 서버가 하나를 선택한다. 두 엔드포인트는 선택에 동의해야 하며, 그렇지 않으면 타입이 일치하지 않는다.

메뉴로 되돌아가는 지속 연결과 같은 재귀적 프로토콜은 재귀적 타입 정의를 필요로 한다. 여기가 대부분의 언어가 어려움을 겪는 곳이다. Rust는 이를 지원하지만 장황해진다.

다자 문제도 있다. 위의 세션 타입은 이진적이다: 두 엔드포인트. 세 개 이상의 프로세스가 조율하면 다자 세션 타입이 필요한데, 이는 훨씬 더 복잡하고 성숙한 구현이 적다.

알아야 할 트레이드오프

세션 타입은 한 클래스의 오류를 제거하지만 모든 데드락을 제거하지는 않는다. 모든 프로세스가 외부 리소스를 기다리는 전역 데드락이나, 진행 없이 회전하는 라이브락은 여전히 가능하다. 세션 타입은 구체적으로 통신 불일치를 대상으로 한다.

또한 컴파일 시간 오버헤드도 도입한다. 깊은 타입 스택의 오류 메시지는 불가해할 수 있다. 단순한 채널 타입 오류가 컴파일러 출력에서 50줄의 중첩된 제네릭으로 확장될 수 있다. Rust 생태계는 여기서 개선되었지만, 세션 타입 불일치를 디버깅하는 것은 여전히 습득이 필요한 기술이다.

동적 토폴로지도 또 다른 골칫거리다. 세션 타입은 통신 그래프가 정적이고 컴파일 시간에 알려져 있을 때 가장 잘 작동한다. 가변 수의 참가자가 있는 채팅방처럼 런타임 데이터에 기반하여 채널을 생성하는 경우, 세션 타입의 적용이 훨씬 어려워진다.

오늘 이것을 시도하는 방법

Rust에서 세션 타입을 실험하고 싶다면 session_types 크레이트가 원래 이론에 기반한 성숙한 구현을 제공한다. 더 인체공학적인 API를 위해 sesh가 대안적 접근법을 제공한다.

Haskell에서는 session-types가 Haskell의 타입 수준 프로그래밍으로 유사한 보장을 제공한다. 산업 사용에 더 가까운 것을 찾는다면 생성된 클라이언트 스텁이 있는 Protocol Buffers를 살펴보라. 형식적 의미의 세션 타입은 아니지만, 생성된 코드는 동일한 원칙을 강제한다: 프로토콜은 외부에서 정의되고 컴파일러는 사용을 대해 검사한다.

고정된 통신 프로세스 집합으로 분산 시스템을 구축하고 있다면, 통신 그래프를 그리는 것부터 시작하라. 모든 메시지에 화살표를 그려라. 그래프가 불일치를 걱정할 만큼 복잡하다면, 그곳이 세션 타입이 보상되는 곳이다.

FAQ

세션 타입이 모든 데드락을 방지합니까?

아니다. 둘 다 보내기를 기다리는 두 프로세스와 같은 통신 불일치로 인한 deadlock을 방지한다. 리소스 deadlock, 라이브락, 또는 외부 시스템을 포함하는 deadlock은 방지하지 않는다.

세션 타입과 상태 머신의 차이는 무엇입니까?

세션 타입은 타입 시스템에 인코딩된 상태 머신이다. 상태 전환은 런타임에 검사되는 것이 아니라 모든 채널 연산에서 컴파일러에 의해 강제된다.

세션 타입이 프로덕션에서 사용됩니까?

이진 세션 타입은 연구 시스템과 전문 분야에서 사용된다. 다자 세션 타입은 여전히 주로 학문적이다. 이러한 개념은 생성된 gRPC 클라이언트와 Rust의 타입 상태 패턴을 포함한 현대 API 설계에 영향을 준다.

Rust 없이 세션 타입을 사용할 수 있습니까?

예. Haskell, Scala, OCaml 모두 세션 타입 라이브러리를 가지고 있다. 아핀 타입이 없는 언어에서도 선형 타입 검사기나 런타임 어서션으로 패턴을 근사할 수 있다.

데드락은 이제 타입 문제다

데드락은 타입 문제로 만들기 전까지는 실행 시간 문제다. 세션 타입은 은탄이 아니지만, 잘 정의된 프로토콜을 가진 메시지 전달 시스템에서는 버그의 전체 클래스를 “프로덕션에서 잡기”에서 “컴파일 시간에 잡기”로 이동시킨다. 다음에 새로운 서비스 아키텍처를 스케치할 때 고려할 가치가 있는 트레이드오프다.