Les deadlocks sont censés être un problème d’exécution. C’est ce qui les rend si agaçants. Votre code compile proprement, vos tests passent, et puis il se coince en production parce que le Processus A attend le Processus B et le Processus B attend le Processus A.

Les types de session inversent cela. Ils encodent le protocole de communication entre processus dans le système de types lui-même. Certaines classes de deadlocks cessent d’être des surprises à l’exécution et deviennent des erreurs de compilation. Vous ne pouvez littéralement pas écrire le code qui se bloque.

Ce que sont réellement les types de session

Les types de session sont une discipline de types pour les canaux de communication. Au lieu qu’un canal soit un tube non typé duquel vous lisez et auquel vous écrivez, un canal typé par session porte un type qui décrit la séquence exacte des opérations qui lui sont permises.

Envoyez un entier, puis recevez une chaîne, puis fermez. Le compilateur suit cette séquence à chaque étape. Déviez de celle-ci, et vous obtenez une erreur de type, pas un deadlock à l’exécution.

Cette idée vient des calculs de processus et a des implémentations en Haskell, Scala, OCaml et Rust. Le système de propriété de Rust et ses types affines en font un ajustement particulièrement naturel, mais le concept est indépendant du langage.

Comment les deadlocks de passage de messages se produisent réellement

Considérez deux processus qui doivent échanger des données. Une erreur commune ressemble à ceci :

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

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

Les deux processus essaient d’envoyer en premier. Si les channel buffers sont pleins, les deux bloquent sur l’envoi. Aucun n’atteint jamais recv. C’est un deadlock classique d’inadéquation de communication.

Vous pourriez penser “ne faites simplement pas cela.” Mais dans un système réel avec des dizaines de canaux, une logique conditionnelle et du code qui est refactorisé six mois plus tard, ce motif s’insère constamment. Le vérificateur de types n’a pas d’opinion sur la cohérence de votre séquence d’envoi et de réception.

Comment les types de session rendent le deadlock irrépresentable

L’astuce centrale est qu’un type de session change après chaque opération. Un canal n’a pas de type statique. Il a un type qui devient autre chose après que vous l’ayez utilisé.

Voici une implémentation minimale en Rust qui démontre l’idée :

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

Un canal avec le type Chan<Send<i32, Recv<String, Close>>> signifie : vous devez envoyer un i32, puis vous aurez un canal qui peut recevoir un String, puis vous aurez un canal qui ne peut être que fermé.

La méthode send consomme l’ancien canal et retourne un nouveau avec le type mis à jour. Parce que le système de propriété de Rust assure que self est consommé, vous ne pouvez pas réutiliser l’ancien canal. Le compilateur ne vous laissera pas envoyer deux fois, ou recevoir hors ordre, ou oublier de fermer.

Pour notre scénario de deadlock, vous définissez les deux extrémités avec des types complémentaires :

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();
}

Le Processus A envie puis reçoit. Le Processus B reçoit puis envoie. Les types de protocole imposent cet ordre.

Si quelqu’un refactorise le Processus B pour envoyer en premier, le compilateur le rejette immédiatement :

// 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());
}

Le système de types dit que ce canal est dans un état de réception. Vous ne pouvez pas envoyer. Le deadlock devient impossible à exprimer.

Où la théorie devient compliquée : branchement et récursion

Les protocoles réels ne sont pas des séquences linéaires. Ils ont des choix. Un serveur pourrait proposer authenticate ou register. Les types de session gèrent cela avec des types de choix internes et externes.

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

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

Le client offre un choix, et le serveur en sélectionne un. Les deux extrémités doivent s’accorder sur le choix, ou les types ne correspondent pas.

Les protocoles récursifs, comme une connexion persistante qui reboucle vers un menu, nécessitent des définitions de types récursifs. C’est là que la plupart des langages peinent. Rust supporte cela, mais cela devient verbeux.

Il y a aussi le problème multipartite. Les types de session ci-dessus sont binaires : deux extrémités. Si trois processus ou plus se coordonnent, vous avez besoin de types de session multipartites, qui sont significativement plus complexes et ont moins d’implémentations matures.

Trade-offs que vous devriez connaître

Les types de session éliminent une classe d’erreurs, mais ils n’éliminent pas tous les deadlocks. Un deadlock global où chaque processus attend une ressource externe, ou un livelock où les processus tournent sans progrès, restent possibles. Les types de session ciblent spécifiquement les inadéquations de communication.

Ils introduisent aussi une surcharge à la compilation. Les messages d’erreur de piles de types profondes peuvent être inscrutables. Une simple erreur de type de canal pourrait s’étendre en 50 lignes de génériques imbriqués dans la sortie du compilateur. L’écosystème Rust s’est amélioré ici, mais déboguer les inadéquations de types de session reste une compétence acquise.

Les topologies dynamiques sont un autre point de douleur. Les types de session fonctionnent mieux quand le graphe de communication est statique et connu à la compilation. Si vous générez des canaux basés sur des données d’exécution, comme une salle de chat avec un nombre variable de participants, les types de session deviennent beaucoup plus difficiles à appliquer.

Comment essayer cela aujourd’hui

Si vous voulez expérimenter avec les types de session en Rust, le crate session_types fournit une implémentation mature basée sur la théorie originale. Pour une API plus ergonomique, sesh offre une approche alternative.

En Haskell, session-types vous donne des garanties similaires avec la programmation au niveau des types de Haskell. Pour quelque chose de plus proche de l’usage industriel, regardez Protocol Buffers avec des stubs client générés. Bien que ce ne soient pas des types de session au sens formel, le code généré impose le même principe : le protocole est défini extérieurement, et le compilateur vérifie votre usage contre lui.

Si vous construisez un système distribué avec un ensemble fixe de processus communicants, commencez par dessiner le graphe de communication. Dessinez des flèches pour chaque message. Si le graphe est suffisamment complexe pour que vous vous inquiétiez des inadéquations, c’est là que les types de session portent leurs fruits.

FAQ

Les types de session préviennent-ils tous les deadlocks ?

Non. Ils préviennent les deadlocks causés par des inadéquations de communication, comme deux processus attendant tous deux d’envoyer. Ils ne préviennent pas les deadlocks de ressources, les livelocks ou les deadlocks impliquant des systèmes externes.

Quelle est la différence entre les types de session et les machines à états ?

Les types de session sont des machines à états encodées dans le système de types. Les transitions d’état sont imposées par le compilateur à chaque opération de canal, pas vérifiées à l’exécution.

Les types de session sont-ils utilisés en production ?

Les types de session binaires sont utilisés dans des systèmes de recherche et des domaines spécialisés. Les types de session multipartites sont encore largement académiques. Les concepts influencent la conception moderne d’API, incluant les clients gRPC générés et les patterns type-state de Rust.

Puis-je utiliser les types de session sans Rust ?

Oui. Haskell, Scala et OCaml ont toutes des bibliothèques de types de session. Même dans des langages sans types affines, vous pouvez approximer le pattern avec des vérificateurs de types linéaires ou des assertions à l’exécution.

Les deadlocks sont maintenant un problème de types

Les deadlocks sont un problème d’exécution jusqu’à ce que vous en fassiez un problème de types. Les types de session ne sont pas une balle d’argent, mais pour les systèmes de passage de messages avec des protocoles bien définis, ils déplacent une classe entière de bugs de “attraper en production” à “attraper à la compilation.” C’est un trade-off qui vaut la peine d’être considéré la prochaine fois que vous esquissez une nouvelle architecture de services.