Philosophie de l'ingénierie : Leslie Lamport, réfléchir avant de coder

Points clés

• Réfléchissez avant de coder, et couchez votre réflexion par écrit. Une spécification est l’équivalent logiciel du plan d’un architecte — « ne pas réfléchir garantit que nous » commettrons des erreurs.
• Le temps n’est pas global ; la causalité est ce qui est réel. En l’absence d’horloge partagée fiable, vous cessez de demander quand un événement s’est produit pour demander ce qui a causé quoi.
• La relation « happened-before » et les horloges logiques formalisent la causalité. L’ordre partiel de Lamport — et le compteur par processus qui l’implémente — est le germe des horloges vectorielles et de la résolution de conflits moderne.
• Définissez la correction avec précision, puis prouvez-la. La sûreté et la vivacité, le consensus Paxos, la tolérance aux fautes byzantines et le langage de spécification TLA+ découlent tous du fait de traiter l’informatique distribuée comme une mathématique, et non comme un folklore.

Le principe

« Un système distribué est un système dans lequel la défaillance d’un ordinateur dont vous ne soupçonniez même pas l’existence peut rendre le vôtre inutilisable. » — Leslie Lamport¹

Il a envoyé cette phrase à un tableau d’affichage de son laboratoire en 1987, et c’est la phrase la plus citée de l’informatique distribuée parce qu’elle nomme ce que l’intuition se refuse à croire.¹ Vous pensez exécuter un programme sur votre ordinateur. Ce n’est pas le cas. Vous l’exécutez sur une population de machines dont vous n’avez pas dénombré l’existence, dont les horloges divergent, et dont n’importe laquelle peut défaillir à l’instant précis où cela compte. Le système que vous pouvez tenir dans votre tête et celui qui s’exécute réellement sont deux systèmes différents, et c’est dans l’écart entre les deux que se loge chaque bug distribué.

L’œuvre d’une vie de Lamport, c’est le refus de masquer cet écart par de l’optimisme. Sa conviction est que les systèmes concurrents et distribués sont trop subtils pour qu’on les raisonne par intuition ; on les raisonne donc avec des mathématiques, sur le papier, avant d’écrire la moindre ligne de code. « Réfléchir ne garantit pas que nous ne commettrons pas d’erreurs », a-t-il déclaré à Wired en 2013. « Mais ne pas réfléchir garantit que nous en commettrons. »² Cette réflexion doit être couchée par écrit, car c’est dans l’écriture que la pensée bâclée se révèle : « Pour réfléchir, il faut écrire. Si vous réfléchissez sans écrire, vous croyez seulement réfléchir. »³ Les architectes dessinent un plan avant qu’on pose la première brique ; l’équivalent logiciel est une spécification, et Lamport a passé la seconde moitié de sa carrière à soutenir que si nos systèmes cassent, c’est parce que nous la sautons.⁴

Le geste le plus profond porte sur le temps lui-même. Dans le monde physique, il n’existe aucune horloge globale digne de confiance pour ordonner les événements entre machines — il faut donc cesser de demander quand une chose s’est produite et commencer à demander ce qui a causé quoi. La causalité, et non l’horloge murale, est la véritable structure d’un calcul distribué.⁵ Presque tout ce que Lamport a construit découle du fait d’avoir pris ce seul fait au sérieux, et c’est la même conviction qui sous-tend la barrière des preuves : vous n’avez pas le droit de présumer l’ordonnancement que vous aimeriez voir vrai ; vous devez l’établir.

Contexte

Leslie Lamport est né le 7 février 1941 à New York.⁶ Il obtient une licence de mathématiques au MIT en 1960, puis un master et — en 1972 — un doctorat de mathématiques à Brandeis, avec une thèse sur les singularités des équations aux dérivées partielles.⁶ Il n’a pas été formé comme informaticien. Il a été formé comme mathématicien, et il n’a jamais cessé de se comporter comme tel. Le trait déterminant de sa carrière, c’est qu’il a apporté les exigences des mathématiques — définitions précises, hypothèses énoncées, preuves plutôt que tests — à un domaine qui programmait surtout au feeling.

Son travail s’est déployé dans quatre institutions. À Massachusetts Computer Associates, dans les années 1970, il accomplit la réflexion fondatrice sur l’ordonnancement des événements. Au SRI International (1977-1985), il produit les travaux sur les généraux byzantins. Au Systems Research Center de Digital Equipment Corporation (à partir de 1985, en continuant à travers le rachat par Compaq jusqu’en 2001), il écrit Paxos et entame le travail de spécification. De 2001 jusqu’à sa retraite, début 2025, il est chez Microsoft Research.⁶ Tout au long, la méthode reste constante : trouver dans l’informatique distribuée ou concurrente un problème que tout le monde traitait comme un folklore, le définir assez précisément pour énoncer un théorème, puis prouver le théorème.

L’œuvre

Le temps, les horloges et la relation « happened-before »

« Time, Clocks, and the Ordering of Events in a Distributed System » paraît dans Communications of the ACM en 1978, et figure parmi les articles les plus cités de toute l’informatique — il remporte en 2000 le prix Dijkstra récompensant l’œuvre la plus influente de l’informatique distribuée.⁵⁶ Son intuition est d’une petitesse trompeuse. Dans un système distribué, il n’existe aucune horloge partagée et fiable ; on ne peut donc pas ordonner deux événements en comparant des estampilles temporelles. Ce que l’on peut savoir, c’est si un événement aurait pu en causer un autre : l’événement A précède (happened-before) l’événement B si A et B sont sur le même processus avec A en premier, ou si A est l’envoi d’un message et B sa réception. Enchaînez ces relations et vous obtenez la relation « happened-before » — la causalité rendue formelle.⁵

La conséquence cruciale et contre-intuitive, c’est que « happened-before » n’est qu’un ordre partiel, et non total. Deux événements sur des processus différents, sans aucune chaîne de messages entre eux, sont véritablement concurrents : il n’existe aucun fait quant à savoir lequel est venu en premier, et tout système qui prétend le contraire invente un ordonnancement qui n’existe pas.⁵ Lamport donne ensuite l’algorithme qu’on appelle aujourd’hui universellement l’horloge de Lamport : chaque processus maintient un compteur, l’incrémente à chaque événement et l’appose sur chaque message sortant ; un récepteur porte son compteur à une unité de plus que le maximum entre sa propre valeur et l’estampille du message.⁷ Cette règle simple produit des estampilles cohérentes avec la causalité, et c’est le germe des horloges vectorielles, des vecteurs de version et de toute la machinerie de résolution de conflits des bases de données distribuées modernes.

Si cet article compte au-delà de son algorithme, c’est qu’il a changé la question. Avant Lamport, on supposait que « à quelle heure cela s’est-il produit ? » avait une réponse dans un système distribué. Après Lamport, la réponse honnête était « mauvaise question — demandez plutôt ce qui l’a causé ». C’est ce recadrage qui lui vaut d’être crédité d’avoir fait de l’informatique distribuée une science plutôt qu’un artisanat.

Paxos, le consensus et les machines à états répliquées

S’il n’existe pas d’horloge globale et que les machines défaillent, comment un groupe d’ordinateurs parvient-il jamais à s’accorder sur quoi que ce soit — quelle transaction a été validée, qui détient le verrou, quelle est la prochaine entrée du journal ? Cette question est le problème du consensus, et la réponse de Lamport est Paxos, l’algorithme au cœur de presque tout système tolérant aux fautes construit depuis. Il l’a associé à l’approche des machines à états répliquées : si chaque réplique part du même état et applique la même séquence de commandes dans le même ordre, elles restent identiques — de sorte que tout le problème du maintien de la cohérence d’un système distribué se réduit à s’accorder sur l’ordre des commandes, ce que Paxos fournit précisément.⁶

L’histoire de la publication de Paxos est la mise en garde la plus célèbre du domaine. Lamport l’a rédigée sous le titre « The Part-Time Parliament », présentant l’algorithme comme la procédure législative d’une île grecque antique fictive nommée Paxos, jusqu’aux législateurs portant des translittérations pseudo-grecques des noms de ses collègues.⁸ La plaisanterie fut une catastrophe. Les évaluateurs ont cru qu’il n’était pas sérieux ; l’article fut rejeté comme insignifiant ; les personnes qui assistaient à ses conférences se rappelaient l’enrobage à la Indiana Jones, mais pas l’algorithme.⁸ Il est resté inédit pendant des années. L’éditeur de Communications of the ACM l’a finalement publié dans ACM Transactions on Computer Systems en 1998 — toujours enveloppé dans la parabole.⁸ Comme le domaine continuait de l’ignorer, Lamport a fini par capituler et a écrit « Paxos Made Simple » en 2001, dépouillant l’habillage grec pour révéler ce qu’il affirmait être un algorithme réellement simple en dessous.⁸ La leçon qu’il en a tirée n’était pas « les gens sont bêtes ». C’était que même une idée correcte et importante échoue si l’on en obscurcit la réflexion — la présentation fait partie du travail, elle n’en est pas séparée.

Le problème des généraux byzantins

En 1982, avec Robert Shostak et Marshall Pease, Lamport publie « The Byzantine Generals Problem », qui a donné au domaine son vocabulaire pour le type de défaillance le plus difficile.⁶ Un composant qui plante est facile à côté d’un composant byzantin — un composant qui ne s’arrête pas mais ment, envoyant des informations différentes et contradictoires à différents pairs, que ce soit par bug, corruption ou malveillance. La mise en scène de l’article : des divisions d’une armée, chacune menée par un général, doivent s’accorder sur un plan unique — attaquer ou battre en retraite — par messager, tandis qu’un sous-ensemble inconnu de généraux sont des traîtres cherchant activement à empêcher l’accord. Lamport a prouvé le seuil précis du nombre de traîtres qu’un système peut tolérer tout en parvenant à un accord, transformant « et si un nœud ment ? » d’une vague inquiétude en un théorème assorti d’une borne énoncée.

Ce théorème est la racine intellectuelle de tout système qui doit continuer à fonctionner alors que certains de ses participants sont adverses — et c’est pourquoi, des décennies plus tard, le mot byzantin trône au cœur du consensus de la blockchain. Lamport n’avait pas pour but de rendre possibles les cryptomonnaies ; il avait pour but de définir, exactement, ce que signifie la tolérance aux fautes lorsque « faute » inclut la trahison.

TLA+ et la spécification (et, oui, LaTeX)

Le fil conducteur de la carrière de Lamport est la conviction qu’il faut spécifier avant de coder, et TLA+ est cette conviction incarnée dans un outil. La Temporal Logic of Actions est un langage permettant d’écrire une description mathématique précise de ce qu’un système est censé faire — ses états, les pas qui les relient, et les propriétés qu’il doit toujours satisfaire (sûreté : rien de mauvais n’arrive jamais) et finir par atteindre (vivacité : quelque chose de bon finit par arriver), deux concepts qu’il a formalisés.⁶ Vous écrivez la spécification, et un model checker explore l’espace des états pour trouver l’entrelacement subtil qui brise votre invariant — le bug que vous n’auriez jamais trouvé par les tests, parce qu’il n’apparaît que lorsque trois machines font trois choses dans un ordre que vous n’avez jamais imaginé. Son argument est celui du plan de l’architecte : on dessine le bâtiment avant de couler le béton, et une spécification logicielle est ce même plan, écrit en mathématiques parce que les mathématiques sont le langage le plus précis dont nous disposions.⁴

Et il existe un monument plus discret. Au début des années 1980, s’appuyant sur le TeX de Donald Knuth, Lamport écrit LaTeX — le système de macros devenu la façon par défaut dont les scientifiques et les mathématiciens composent leurs documents, la raison pour laquelle toute une génération d’articles et de thèses a l’allure qu’on lui connaît.⁶ C’est un artefact typiquement lamportien : il avait besoin de coucher son propre travail par écrit avec précision, alors il a construit l’outil qui a permis à chacun de le faire. L’instinct qui a produit TLA+ — une notation qui force la précision — est le même que celui qui a produit LaTeX.

La méthode

La méthode est une seule idée appliquée sans relâche pendant cinquante ans : la réflexion est le travail, et la réflexion doit être couchée par écrit avant le code.

Raisonnez sur la causalité, pas sur le temps. Il n’existe aucune horloge globale digne de confiance ; cessez donc d’ordonner les événements selon le moment où ils se sont produits et ordonnez-les selon ce qui a causé quoi. La relation « happened-before », et non l’horloge murale, est la véritable structure — et accepter que deux événements soient véritablement concurrents est plus honnête qu’inventer un ordre.⁵

Spécifiez avant de coder. Pour tout ce qui n’a pas de solution établie, arrêtez-vous et réfléchissez d’abord ; la réflexion est indépendante du codage. Écrivez le plan — la spécification — en mathématiques, car les mathématiques sont simples et précises là où la prose est vague.⁴ « Ne pas réfléchir garantit que nous » commettrons des erreurs.²

Écrivez pour découvrir si vous réfléchissez vraiment. L’écriture est l’épreuve de la réalité d’une pensée. « Si vous réfléchissez sans écrire, vous croyez seulement réfléchir. »³ Une spécification que vous ne pouvez pas coucher par écrit est une idée que vous n’avez pas encore réellement.

Définissez la défaillance avec exactitude. « Et si un nœud ment ? » reste du folklore tant que vous ne l’énoncez pas sous la forme des généraux byzantins et que vous ne prouvez pas la borne de tolérance. Les définitions précises transforment les inquiétudes en théorèmes.⁶

La présentation fait partie de la correction. Paxos était correct pendant des années avant que quiconque puisse s’en servir, parce que la parabole grecque enfouissait l’idée. Un résultat correct que personne ne peut comprendre n’a pas fini d’être conçu.⁸

Chaîne d’influence

Qui l’a façonné

Les mathématiques elles-mêmes. La formation de Lamport était un doctorat de mathématiques, et non d’informatique, et toute la forme de sa contribution est l’importation des exigences mathématiques — définitions, axiomes, preuves — dans un domaine qui programmait par intuition.⁶ (Influence formatrice)

Les problèmes de tolérance aux fautes des systèmes réels des années 1970. Les travaux du SRI sur les systèmes fiables pour l’aéronautique et l’horreur concrète des machines qui défaillent au milieu d’un protocole lui ont fourni des problèmes concrets — fautes byzantines, consensus — qui exigeaient le traitement formel qu’il était fait pour apporter.⁶ (Influence directe)

Edsger Dijkstra. La conviction que la correction s’établit par la preuve plutôt que par le test, et que les programmes concurrents doivent être raisonnés formellement, est celle de Dijkstra avant d’être celle de Lamport. Le prix que Lamport a remporté pour son article sur les horloges porte le nom de Dijkstra. (Influence directe)

Qui il a façonné

Toute base de données distribuée, plateforme cloud et blockchain. Les horloges logiques sous-tendent la résolution de conflits dans les magasins distribués ; Paxos (et son descendant Raft) est le cœur du consensus de Chubby et Spanner chez Google, de ZooKeeper, d’etcd et de la couche de coordination de pratiquement tout cloud. Le résultat sur les généraux byzantins est le socle théorique de Bitcoin et de tout protocole de consensus tolérant aux fautes depuis.

Les méthodes formelles dans l’industrie. Amazon Web Services utilise notoirement TLA+ pour spécifier et vérifier S3, DynamoDB et d’autres services centraux avant de les livrer — en débusquant des bugs subtils dans la conception, et non en production. L’argument du plan de Lamport est passé de l’hérésie à la pratique.

Le vocabulaire du domaine. « Happened-before », sûreté et vivacité, machines à états répliquées, cohérence séquentielle, faute byzantine — ce ne sont pas des contributions de Lamport au langage des systèmes distribués ; elles sont en grande partie ce langage.

Le fil conducteur

Edsger Dijkstra soutenait que l’on raisonne la correction d’un programme avant de l’exécuter — que le test montre la présence des bugs, jamais leur absence —, et Lamport en est l’héritier direct, portant la preuve-avant-exécution des programmes séquentiels vers le monde bien plus difficile de la concurrence, où le bug que l’on ne peut pas tester est la règle plutôt que l’exception. Barbara Liskov a fait du raisonnement formel sur le comportement d’un programme une primitive opérationnelle, avec l’abstraction de données et la substituabilité ; Lamport a fait du raisonnement formel sur le comportement d’un système dans le temps la norme, en spécifiant non pas ce qu’un objet garantit mais ce qu’un système concurrent tout entier doit toujours et finalement faire. Et Donald Knuth a apporté la rigueur mathématique à l’analyse des algorithmes et, presque incidemment, a construit TeX pour que ce travail puisse être couché par écrit avec précision — une rime quasi exacte avec Lamport, qui a bâti LaTeX par-dessus pour la même raison et a fait de la spécification elle-même un acte mathématique. Trois mathématiciens qui ont refusé que « ça a l’air de marcher » tienne lieu de savoir. (Pont de la série)

Ce que j’en retiens

La leçon que je garde, c’est que la réflexion est le travail, et que la réflexion n’est pas réelle tant qu’elle n’est pas couchée par écrit. L’argument du plan de Lamport est inconfortable parce qu’il est juste : si un système casse en production, ce n’est presque jamais parce que le code a été mal saisi — c’est que personne n’a spécifié ce que le système était réellement censé faire sous concurrence et défaillance, de sorte qu’il n’existait aucun énoncé auquel confronter le code. La discipline consiste à écrire la spécification avant l’implémentation, dans un langage assez précis pour que ses contradictions deviennent visibles. C’est exactement la norme selon laquelle la qualité est la seule variable : la question n’est jamais « est-ce que ça passe le chemin heureux ? » mais « ai-je énoncé, exactement, ce qui doit toujours être vrai — et prouvé que la conception l’honore ? ». C’est pourquoi je m’appuie si fort sur l’écriture du PRD avant le code ; un PRD est une spécification de Lamport en habits de travail.

Dans le monde où je construis aujourd’hui — agents, boucles d’outils, systèmes multi-agents —, la leçon de Lamport est celle que presque tout le monde saute, et qu’on paie. Un système d’agents est un système distribué : des processus indépendants, pas d’horloge globale, des messages qui arrivent dans le désordre ou pas du tout, et des composants qui défaillent silencieusement ou, pire, qui mentent. Les bugs ne sont jamais dans le prompt ; ils sont dans l’ordonnancement — deux agents agissant sur un état périmé, un appel d’outil dont le résultat arrive après la décision qui en avait besoin, une paire d’événements « concurrents » que l’orchestrateur a feint d’ordonner. La discipline de Lamport consiste à cesser de se fier à l’intuition de l’horloge murale, à raisonner explicitement sur la causalité et la défaillance, et à coucher par écrit ce qui doit toujours être vrai avant de câbler quoi que ce soit. La conviction que l’on spécifie avant de construire, que l’on raisonne sur un système plutôt que de le tâtonner — voilà le fil conducteur qui relie un article de 1978 sur les horloges à un cadre d’agent de 2026, et c’est précisément pourquoi je traite la performance et la correction d’un système comme une propriété qu’on conçoit dès le départ, jamais comme une propriété qu’on espère débugger après coup.

FAQ

Quelle est la philosophie de l’ingénierie de Leslie Lamport ?

La conviction de Lamport est que les systèmes concurrents et distribués sont trop subtils pour qu’on les raisonne par intuition ; il faut donc réfléchir avec des mathématiques, sur le papier, avant d’écrire du code — comme un architecte dessine un plan avant qu’on pose la première brique. Le plan logiciel est une spécification, écrite en mathématiques parce que les mathématiques sont le langage le plus précis disponible.⁴ Sous-jacente à cela se trouve une posture à l’égard du temps : dans un système distribué, il n’existe aucune horloge globale digne de confiance, de sorte que la véritable structure d’un calcul est la causalité — ce qui a causé quoi — et non le moment où les choses se sont produites.⁵ « Réfléchir ne garantit pas que nous ne commettrons pas d’erreurs », disait-il, « mais ne pas réfléchir garantit que nous en commettrons. »²

Qu’est-ce qu’une horloge de Lamport et la relation « happened-before » ?

La relation « happened-before » est la formalisation par Lamport de la causalité dans un système distribué : l’événement A précède l’événement B s’ils sont sur le même processus avec A en premier, ou si A envoie un message et B le reçoit, ou par enchaînement de ces cas.⁵ Ce n’est qu’un ordre partiel — deux événements sur des processus différents, sans message les reliant, sont véritablement concurrents, et aucun système correct ne peut prétendre que l’un est venu en premier.⁵ Une horloge de Lamport implémente cela avec un compteur par processus : incrémentez-le à chaque événement, apposez-le sur chaque message sortant, et à la réception portez votre compteur à une unité de plus que le maximum entre votre propre valeur et l’estampille du message.⁷ Le résultat est un ensemble d’estampilles cohérentes avec la causalité — le fondement des horloges vectorielles et de la résolution de conflits distribuée moderne.

Qu’est-ce que Paxos et le problème des généraux byzantins ?

Paxos est l’algorithme de Lamport pour le consensus — amener un groupe de machines peu fiables, susceptibles de défaillir, à s’accorder sur une valeur unique, telle que la prochaine commande d’un journal répliqué — et il sous-tend la couche de coordination de presque tout système distribué moderne. Fait célèbre, il l’a d’abord publié sous la forme d’une parabole sur un parlement grec fictif (« The Part-Time Parliament », ACM TOCS 1998) ; la plaisanterie a tant obscurci l’idée qu’il a fini par la réécrire sous le titre « Paxos Made Simple » en 2001.⁸ Le problème des généraux byzantins (Lamport, Shostak et Pease, 1982) définit le mode de défaillance le plus difficile — des composants qui ne se contentent pas de planter mais qui mentent, en envoyant des informations contradictoires — sous la forme de généraux tentant de s’accorder sur un plan tandis que des traîtres parmi eux sabotent l’accord, et prouve combien de traîtres un système peut tolérer.⁶ C’est la racine théorique du consensus de la blockchain.

Pourquoi Leslie Lamport a-t-il remporté le prix Turing ?

L’ACM a décerné à Lamport le prix A.M. Turing 2013 « pour des contributions fondamentales à la théorie et à la pratique des systèmes distribués et concurrents, notamment l’invention de concepts tels que la causalité et les horloges logiques, la sûreté et la vivacité, les machines à états répliquées et la cohérence séquentielle. »⁶ La citation rend compte de l’ampleur de son œuvre : il a fait passer l’informatique distribuée du folklore à la science avec des définitions et des preuves précises, a donné au domaine une grande partie de son vocabulaire, a créé le langage de spécification TLA+ pour faire de « spécifier avant de coder » une discipline concrète, et — en s’appuyant sur le TeX de Knuth — a écrit LaTeX, le système de composition devenu standard dans toutes les sciences et les mathématiques.⁶

Sources