Pichonas

Le problème

Pichonas est un logiciel de Liant qui répartit des calculs d'intelligence artificielle, appelés calculs d'inférence, entre plusieurs machines. Un client dépose une demande, qui est découpée en tâches ; des machines de calcul, les exécuteurs, viennent chercher ces tâches, les calculent et rendent leur résultat.

Or ces machines ne sont pas fiables. L'une tombe en panne au milieu d'un calcul, une autre perd le réseau, une troisième est simplement lente. Pour ne pas perdre la tâche, le système la confie alors à une autre machine, si bien qu'elle peut être calculée deux fois. Dans une file de tâches ordinaire, le résultat retenu dépend alors de l'ordre d'arrivée : un résultat tardif peut écraser le bon, et rien ne permet au client de savoir lequel fait foi. Pour un service qui facture et livre un résultat par tâche, c'est une erreur silencieuse, même quand chaque machine a correctement fait son travail.

Ce que Pichonas garantit

Les garanties ci-dessous sont des théorèmes : elles sont démontrées mathématiquement sur une description exacte du fonctionnement de Pichonas, et un logiciel de vérification de preuves contrôle chaque démonstration.

• Aucune tâche perdue. Une tâche déposée reste connue du système jusqu'à sa fin, avec un seul état à la fois : en attente, confiée à une machine, réussie ou échouée. Une tâche terminée ne change plus.
• Un seul résultat retenu par tâche. Chaque fois qu'une tâche est confiée à une machine, elle reçoit un numéro de version plus grand que le précédent. Seul le résultat qui porte le numéro en cours, rendu par la machine qui détient la tâche, est accepté, et une seule fois. Un résultat tardif ou rendu par une autre machine est refusé, sans rien modifier.
• Reprise d'une machine disparue. Une tâche dont la machine ne donne plus signe de vie redevient disponible dans un délai borné, fixé par la configuration (de l'ordre d'une minute).
• Cloisonnement entre clients. Une tâche n'est confiée qu'à une machine autorisée pour ce client et capable de faire tourner le modèle demandé. Un client ne voit et n'annule que ses propres tâches.
• Fin de chaque tâche. Si le service fonctionne normalement, c'est-à-dire si l'horloge avance, si la surveillance des délais tourne et si une machine autorisée vient chercher du travail, toute tâche finit par se terminer. Elle réussit dès qu'une machine rend un résultat accepté, et sinon elle est déclarée en échec après un nombre de tentatives fixé par la configuration.
• Reprise après une réponse perdue. Une machine qui n'a pas reçu la réponse à sa demande de travail peut la renouveler et retrouve la même tâche, sans consommer de tentative.

Ces démonstrations portent sur le cœur du système. Le reste, c'est-à-dire la communication réseau chiffrée, l'écriture sur disque et la lecture de l'horloge, est testé mais non démontré. La démonstration ne dit pas non plus si un résultat est juste : une machine autorisée qui rend un résultat faux n'est pas détectée. Enfin, le serveur central est aujourd'hui un point unique de défaillance, puisqu'il n'est pas encore répliqué.

Comment c'est construit

Le comportement de Pichonas est d'abord décrit règle par règle dans Rocq, un logiciel qui vérifie des démonstrations mathématiques. Les garanties ci-dessus sont démontrées sur cette description, sans aucune hypothèse admise sans preuve. Le programme qui calcule chaque décision du serveur est ensuite produit automatiquement à partir de cette description, et l'intégration continue vérifie à chaque modification que le code livré est bien celui-là.

Autour de ce cœur, une enveloppe écrite à la main assure la communication, la journalisation sur disque et la lecture de l'heure ; elle est couverte par des tests, pas par des démonstrations. Restent à croire sans démonstration la production automatique du code, la correspondance des nombres entre les deux langages et la fidélité de la description formelle au cahier des charges, dont les écarts sont consignés.

Une demande suit toujours le même chemin :

1. Le frontal vérifie le certificat de la machine ou du client et transmet son identité au serveur.
2. Le serveur lit la demande, contrôle l'identité et note l'heure.
3. Il déclare d'abord expirées les tâches dont le délai est dépassé.
4. Il écrit la demande dans son journal sur disque.
5. Le cœur, issu de la démonstration, calcule la décision.
6. La réponse ne part qu'une fois l'écriture terminée. Après un arrêt, le serveur relit son journal et retrouve exactement le même état.

Démonstration : Pichonas face à Celery et Redis

Pour mesurer ce que ces garanties changent en pratique, nous avons joué les mêmes situations difficiles sur Pichonas et sur Celery avec Redis, une file de tâches très répandue, réglée selon les recommandations de sa documentation pour ne perdre aucune tâche. Chaque situation porte sur 20 tâches. Les machines de calcul y sont supposées non fiables et partagées entre plusieurs clients, ce qui est le cas pour lequel Pichonas est conçu ; Celery, lui, suppose des machines de confiance, et c'est un choix de conception, non un défaut.

Ces chiffres sont des mesures, faites sur une seule machine avec une charge faible et des calculs simulés ; le script qui les produit les rejoue à l'identique. Seuls Celery et Redis ont été mesurés, et non les autres files du marché. Les refus de Pichonas, eux, découlent des théorèmes décrits plus haut : ils ne dépendent pas de la mesure.

En chiffres

• 90 théorèmes, qui couvrent les garanties décrites plus haut. Tous sont vérifiés par Rocq à chaque modification du code, et aucune hypothèse n'y est admise sans preuve.
• Logiciel libre, sous licence Mozilla Public License 2.0.
• Porteur : Pichonas est un projet de recherche de Liant.