Vous ne pouvez pas unit tester un protocole distribué, mais vous pouvez le model checker

Vous ne pouvez pas unit tester un protocole distribué. Un unit test exécute un processus sur une machine dans un ordre. Votre protocole exécute dix processus sur cinq machines dans un ordre que vous ne contrôlez pas. L’écart entre ces deux réalités est là que vivent vos bugs.

Le model checking comble cet écart. Il explore tous les entrelacements possibles de tous les états possibles que votre protocole peut atteindre. S’il existe un moyen pour que deux réplicas divergent, un moyen pour qu’une élection de leader tombe en deadlock, ou un moyen pour qu’un scénario de split-brain émerge, un model checker le trouvera. Et il le trouvera avant que vous n’ayez écrit le premier RPC handler.

Pourquoi les bugs distribués survivent aux tests traditionnels

L’explosion d’états est le problème. Trois nœuds échangeant des messages peuvent produire des milliards de chemins d’exécution. Les integration tests écrits à la main couvrent peut-être une douzaine d’entre eux, généralement le happy path et quelques failure modes évidents. Le bug où le nœud A plante exactement entre l’envoi d’un prepare et un ack ? Bonne chance pour le déclencher en CI.

La vérification formelle ressemble à un exercice académique, mais le model checking est différent. Vous ne prouvez pas que le protocole est correct pour toujours. Vous décrivez le protocole dans un langage de spécification, définissez les propriétés qui vous importent, et laissez un outil chercher exhaustivement dans l’espace d’états jusqu’à une certaine limite. Quand il trouve une violation, il vous fournit une trace minimale. Vous obtenez une recette étape par étape pour reproduire le bug. Pas de heisenbugs. Pas de « ça marche sur ma machine ».

L’outil le plus pratique pour cela est TLA+, développé par Leslie Lamport. Ça ressemble aux maths parce que ce sont des maths. Mais les maths sont plus simples que vous ne l’espérez, et le payoff est de trouver des bugs qui surgiraient sinon à 2 h du matin en production.

Ce que fait le model checking en réalité

Un model checker prend trois entrées : une description de votre système, une description de son environnement, et les propriétés que vous voulez maintenir. La description du système capture la logique de votre protocole. La description de l’environnement capture tout ce que vous ne contrôlez pas : les delays réseau, la perte de messages, les crashes de nœuds, le skew d’horloge. Les propriétés sont généralement des invariants (« le log committed n’est jamais écrasé ») ou des conditions de liveness (« chaque request reçoit éventuellement une response »).

Le checker génère ensuite chaque état accessible et chaque transition valide entre eux. Il le fait de manière exhaustive pour les espaces d’états finis, ou avec une exploration bornée pour les infinis. Si un invariant est violé, il s’arrête et rapporte le chemin le plus court vers le failure.

C’est du brute force, pas de la magie. Le model checker ne comprend pas votre intention. Il essaie simplement tout. C’est exactement le point. Vos integration tests sont biaisés par vos hypothèses. Le model checker n’a pas d’hypothèses.

Spécifier un protocole de consensus simple en TLA+

Regardons un exemple minimal : un protocole de consensus à décret unique où un leader propose une valeur et un quorum d’accepteurs doit l’accepter avant que la valeur ne soit choisie. C’est l’idée centrale derrière Paxos, Raft et chaque autre algorithme de consensus dont vous avez entendu parler.

Voici la spec TLA+ pour le système :

------------------------------ MODULE Consensus ------------------------------
EXTENDS Integers, Sequences, FiniteSets

CONSTANTS Values, Acceptors, Quorum

VARIABLES chosen

Init == chosen = {}

Propose(v) ==
  /\\ v \\in Values
  /\\ chosen = {}
  /\\ chosen' = {v}

Next ==
  \\E v \\in Values : Propose(v)

Spec == Init /\\ [][Next]_chosen /\\ WF_chosen(Next)

ChosenUniqueness ==
  Cardinality(chosen) \\leq 1
=============================================================================

Cette spec dit : initialement, rien n’est choisi. Une action de proposition peut définir chosen sur une valeur unique, mais seulement si rien n’a encore été choisi. L’invariant ChosenUniqueness stipule qu’au plus une valeur peut jamais être choisie.

Le model checker TLA+, TLC, vérifiera qu’aucun execution trace ne viole ChosenUniqueness. Si vous introduisez un bug où deux leaders peuvent proposer simultanément sans vérifier les valeurs précédentes, TLC trouve le contre-exemple en millisecondes.

Ajouter les parties désordonnées : crashes et perte de messages

La spec ci-dessus est trop propre. Les vrais systèmes distribués ne sont pas propres. Les messages sont perdus. Les nœuds redémarrent. Les network partitions isolent des groupes de nœuds les uns des autres. Le modèle ne devient utile que lorsque vous modélisez ces failures.

Voici un fragment plus réaliste qui modélise le message passing avec une perte potentielle :

VARIABLES msgs, acceptorState

Send(m) == msgs' = msgs \\cup {m}

Deliver(m) ==
  /\\ m \\in msgs
  /\\ msgs' = msgs \\ {m}
  /\\ acceptorState' = [acceptorState EXCEPT ![m.to] = @ \\cup {m.value}]

Drop(m) ==
  /\\ m \\in msgs
  /\\ msgs' = msgs \\ {m}
  /\\ UNCHANGED acceptorState

Next ==
  \\E m \\in msgs : Deliver(m) \\/ Drop(m)

Drop est l’ajout important. Il modélise la perte de messages sans changer l’acceptor state. TLC explorera des traces où n’importe quel message est delivered, dropped ou delayed indéfiniment. Quand vous ajoutez un crash et une récupération de leader, l’espace d’états grandit, mais TLC l’explore toujours systématiquement.

C’est la partie qui m’a trompé quand j’ai commencé avec TLA+. Je voulais modéliser seulement la logique du protocole. Mais les bugs n’étaient pas dans la logique. Ils étaient dans l’interaction entre la logique et les failure modes que je n’avais pas considérés. Vous devez modéliser les deux.

Le compromis : explosion de l’espace d’états et abstraction

Le model checking n’est pas gratuit. Le nombre d’états croît exponentiellement avec le nombre de processus et la taille de vos payloads de messages. Une spec avec cinq valeurs et trois accepteurs pourrait générer des millions d’états. Ajoutez un quatrième accepteur et vous entrez dans les milliards. Lancez ceci sur votre laptop et il manquera de mémoire avant de finir.

La solution est l’abstraction. Vous ne modélisez pas vos valeurs réelles de 64 octets. Vous modélisez deux valeurs : V1 et V2. Si le protocole se comporte correctement pour deux valeurs, les valeurs spécifiques n’ont pas d’importance. Vous ne modélisez pas un log de 10 000 entrées. Vous modélisez un log de profondeur 2. Si safety tient pour la profondeur 2, elle tient presque toujours pour une profondeur arbitraire. Cela s’appelle le small-model checking, et c’est la pratique standard dans le domaine.

La compétence clé est d’apprendre quels détails comptent et lesquels non. Les message contents n’ont généralement pas d’importance pour les safety properties. Le message ordering compte presque toujours. Les node identities pourraient ne pas compter, mais le nombre de nœuds dans chaque rôle oui.

Si l’espace d’états est encore trop grand, vous avez d’autres options. Vous pouvez utiliser la symmetry reduction pour traiter des nœuds identiques comme interchangeables. Vous pouvez borner la profondeur de la recherche. Ou vous pouvez passer à un model checker symbolique comme Apalache, qui utilise des SMT solvers pour raisonner sur les états sans tous les énumérer.

De la spec à l’implémentation : les garder synchronisés

Une spec vérifiée ne vaut rien si votre implémentation diverge d’elle. La spec est le blueprint. Le code est le bâtiment. Il n’y a pas de pont automatisé entre les deux, et c’est dans cet écart que les bugs s’infiltrent.

L’approche pratique est de traiter la spec TLA+ comme un design document qui se trouve être exécutable. Faites-la relire avec le code lors des pull requests. Quand l’implémentation gère un edge case, demandez-vous si la spec le gère aussi. Quand vous trouvez un bug en production, vérifiez si la spec l’aurait attrapé. Si non, mettez-la à jour.

Certaines équipes vont plus loin et génèrent des test cases à partir des counterexamples produits par TLC. Une trace TLC montrant comment deux réplicas divergent devient un scénario d’integration test. C’est du travail manuel, mais cela connecte le modèle formel à votre test suite.

Chez Sentry, nous avons utilisé cette approche pour valider un protocole de rate limiting distribué. La spec a attrapé un liveness issue où un nœud en récupération pouvait starver dans un scénario de partition spécifique. Nos integration tests ne l’avaient jamais déclenché parce qu’ils guérissaient toujours les partitions proprement. Le model checker se souciait peu de la propreté. Il a essayé le cas désordonné, trouvé le bug et nous a épargné un incident très déroutant.

Premiers pas : votre premier model check

Si vous voulez essayer cela, commencez par la TLA+ Toolbox. C’est un IDE gratuit pour écrire et vérifier des specs. Travaillez les exemples Paxos et Raft fournis avec. Ils sont plus complexes que le snippet de consensus ci-dessus, mais ils montrent comment de vrais protocoles sont modélisés.

Pour votre première spec, choisissez quelque chose de petit dans votre propre système. Un protocole d’élection de leader. Un schéma de cache invalidation distribué. Une variante de two-phase commit. Écrivez les invariants que vous pensez tenir. Puis laissez TLC vous dire si vous avez raison. Il dit généralement non, et il le dit généralement dans la première heure.

Le model checking ne trouvera pas tous les bugs. Il n’aidera pas pour la performance, il n’attrapera pas les serialization mistakes, et il ne vérifiera pas que votre implémentation correspond à votre spec. Ce qu’il fait, c’est trouver les bugs profonds de protocole que les integration tests manquent, et il les trouve au moment de la conception, quand les corrections ne coûtent rien.

C’est le bug fix le moins cher dans les systèmes distribués. Pas un meilleur debugger. Pas plus de monitoring. Attraper le bug avant même que le code n’existe.