Certains des défauts les plus dangereux des systèmes peuvent être détectés avant même l’écriture du code, si la conception elle-même est traitée comme un système analysable. C’est l’axe de la présentation de Hillel Wayne, qui explique comment les principes des méthodes formelles permettent d’examiner des systèmes futurs et de détecter des problèmes de résilience, de concurrence et de défaillance avant qu’ils ne se transforment en erreurs opérationnelles.
Wayne commence par un exemple simplifié de ce qu’il appelle un « exécuteur de tâche » : le système vérifie si la tâche a été accomplie, marque ensuite son achèvement, puis exécute la tâche. La séquence semble logique, mais elle s’effondre lorsqu’une défaillance survient pendant l’exécution. Une nouvelle tentative peut être effectuée après que la tâche a été enregistrée comme terminée, si bien que la tâche n’est en réalité jamais exécutée. Si l’enregistrement de l’achèvement est déplacé après l’exécution, un autre problème apparaît : deux exécuteurs concurrents peuvent exécuter la même tâche deux fois avant qu’aucun d’eux n’enregistre son achèvement.
Il ne s’agit pas seulement d’un problème théorique ; la présentation le relie à des exemples tels que les systèmes d’expédition de colis, qui peuvent envoyer deux fois une commande, les systèmes de planification, qui peuvent réserver le même créneau pour deux personnes, et les mécanismes d’installation d’applications, qui peuvent adopter un comportement destructeur lorsqu’une requête est répétée.
Commencer par définir ce que signifie « correct »
Wayne propose de formuler les exigences du système sous la forme de propriétés binaires : elles sont soit vraies, soit fausses. Parmi les exemples figurent le fait que la tâche ne soit pas exécutée plus d’une fois, ce qui constitue une propriété de sûreté empêchant qu’une mauvaise chose se produise, et le fait que la tâche soit exécutée au moins une fois, ce qui constitue une propriété de vivacité garantissant qu’une chose souhaitée se produise.
La présentation insiste sur le fait que les propriétés n’ont pas toutes la même force. Un système capable de traiter 10 000 requêtes par seconde satisfait automatiquement la propriété consistant à traiter deux requêtes par seconde, mais l’inverse n’est pas vrai. Ainsi, la réussite d’une propriété forte peut constituer une preuve de la validité d’un ensemble de propriétés plus faibles, tandis que l’échec d’une propriété plus faible contribue à restreindre la cause du défaut. Wayne relie cette idée à la pyramide des tests : un grand nombre de tests unitaires peut être plus utile pour diagnostiquer une erreur qu’un nombre limité de tests de bout en bout.
Le modèle simplifié révèle le problème fondamental
Au lieu de représenter le système dans tous ses détails, Wayne préconise de construire un modèle abstrait contenant le minimum nécessaire d’état : l’étape actuelle de l’algorithme, le fait que la tâche soit ou non marquée comme terminée, et le nombre de fois où elle a été exécutée. Cela permet d’explorer les états possibles et les chemins que le système peut emprunter, y compris les situations de défaillance et de nouvelle tentative.
Dans les méthodes formelles, ce modèle et ces propriétés peuvent être encodés au moyen de formules logiques, puis vérifiés avec des outils tels que les model checkers et les solveurs SMT. Toutefois, l’idée pratique présentée ne nécessite pas d’utiliser directement ces outils ; l’ingénieur peut adopter la même façon de penser en suivant les états et les transitions possibles.
Le facteur « adversaire » dans la concurrence et les défaillances
Wayne propose de considérer toute source de non-déterminisme, comme les entrées utilisateur, la concurrence, l’aléatoire, les délais d’attente et les interruptions de serveurs, comme un « adversaire » qui choisit toujours le pire résultat possible. Si le système peut effectuer des nouvelles tentatives indéfiniment, cet adversaire choisira l’échec à chaque fois, ce qui révèle que la propriété de vivacité n’est pas garantie, même si la réussite est théoriquement possible.
Il explique également que la présence de deux exécuteurs concurrents exige de représenter certaines variables comme locales à chaque processus, et d’autres comme partagées entre le système et le monde extérieur. En explorant les différents ordres d’exécution, il est possible d’atteindre un état dans lequel la tâche est exécutée deux fois, même lorsque chaque exécuteur semble fonctionner correctement pris isolément.
Les hypothèses font partie de la conception
La correction du système ne dépend pas uniquement de ses propriétés, mais aussi des hypothèses relatives à l’environnement dans lequel il fonctionne. Une conception peut nécessiter l’hypothèse forte que le processus ne tombe jamais en panne, tandis qu’une autre peut fonctionner si la défaillance ne se produit qu’un nombre limité de fois. Wayne indique que la réorganisation des étapes peut réduire les hypothèses de vivacité, mais qu’elle peut accroître les exigences de sûreté, comme la nécessité de garantir qu’un seul exécuteur soit présent à la fois.
La situation change également lorsque l’environnement d’exécution change. Dépendre d’une cohérence forte dans une base de données, puis passer à une cohérence éventuelle, peut rendre non garanties des propriétés qui étaient auparavant correctes, même si le code du système n’a pas changé. Il ne faut donc pas considérer les hypothèses du fournisseur de services ou de la base de données comme des détails externes ; ce sont des conditions directes de la correction de la conception.
Qu’est-ce qui change concrètement ?
La valeur pratique de cette approche ne réside pas dans le remplacement des tests ni dans l’appel à utiliser des outils formels dans chaque projet, mais dans le fait de rendre les questions de conception plus rigoureuses : quels sont les états possibles ? Quel est le pire ordre des événements ? Sur quoi avons-nous réellement prise ? Et quelles sont les hypothèses que l’équipe n’est pas en mesure de garantir ? Plus la propriété requise est forte ou moins l’environnement est prévisible, plus le système doit être conçu de manière complexe, ou plus la propriété requise doit être assouplie, par exemple en transformant la condition « traiter tous les messages » en « traiter les messages ou les envoyer dans une file de messages morts ».
Wayne présente ces idées comme des outils de réflexion issus des méthodes formelles, et non comme un substitut prêt à l’emploi au jugement d’ingénierie. La question ouverte pour chaque système reste le degré de précision du modèle et des hypothèses utilisés ; si un état est omis ou si l’équipe suppose un comportement que l’environnement ne garantit pas, l’analyse peut démontrer la correction d’un modèle qui ne ressemble pas au système réel.