Leslie Lamport est l’auteur d’articles parmi les plus cités dans le domaine de l’informatique. Il a remporté un Turing Award en 2013 pour ses travaux séminaux sur les systèmes concurrents et distribués. Cet article est le résumé d’un entretien que Leslie a accordé à Software Engineering Radio au cours duquel il a évoqué ses premiers travaux sur les systèmes distribués et rappelé l’importance du "Precise Thinking" dans le cadre de la programmation.
Les premières années
Leslie commence l’interview en décrivant sa découverte, du fait que la causalité, c'est-à-dire l’idée qu’un évènement peut affecter un autre évènement si de l’information provenant de cet évènement peut atteindre physiquement cet autre évènement, est aussi importante pour les systèmes distribués qu’elle l’est dans le cadre de la relativité restreinte. Cette intuition a été le point de départ de sa publication, Time, Clocks, and the Ordering of Events in a Distributed System, dans laquelle il arrive à la conclusion que tout système peut être décrit sous la forme de machine à état et dans laquelle il propose un algorithme qui pourrait implémenter une machine à état arbitraire dans un système distribué.
L’étape majeure suivante, telle que définie par Leslie Lamport, fût l’introduction du concept de défaillance dans ses algorithmes. À nouveau, l’intuition l’a conduit à considérer que pour traiter la possibilité de défaillance, il fallait prendre en compte le temps-réel. Ainsi, la notion de défaillance basique correspondait au fait qu’un processus ne réponde pas en temps voulu. Bien sûr, selon les propres mots de Leslie Lamport, cette idée de défaillance était un peu naïve puisqu’elle ne prenait pas en compte la possibilité qu’un processus produise un mauvais résultat. Ceci a donné naissance à la notion de défaillances Byzantines, qui a fondamentalement invalidé l’idée de prendre en charge les défaillances par un vote à la majorité. Avec le vote à la majorité, il faut trois systèmes pour pouvoir voter, et à partir du moment où deux d’entre eux sont d’accord, on obtient notre résultat. Avec les défaillances Byzantines, cette approche ne fonctionne plus car un système peut reporter différents résultats à différents processus.
La publication sur les généraux byzantins a popularisé une allégorie pour décrire des problèmes complexes. Leslie a procédé de la même manière dans sa publication The Part-Time Parliament. Il raconte que cette idée de raconter des histoires vient de Dijkstra et de son "problème du dîner des philosophes", idée qui s’est avérée efficace pour attirer l’attention des gens et rendre un problème populaire.
Malheureusement, la métaphore du parlement à temps-partiel n’a pas fonctionné autant que prévu et a possiblement retardé l’appréciation de l’algorithme Paxos d’une dizaine d’années. Leslie mentionne aussi qu’un des concepts introduit dans ce papier est celui des "leases", c'est-à-dire l’idée d’assigner une ressource à un système pour un temps limité, afin que celle-ci puisse être réclamée et réutilisée même dans le cas où le système s’arrête.
Matière à réflexion pour les programmeurs
Pour introduire le sujet suivant de l’interview, Leslie évoque la session de conférence qu’il a tenue au sujet du "Thinking for programmers". Sa thèse est qu’un grand nombre de problèmes qui existent dans le cadre du développement et de la mise en oeuvre de systèmes est dû à l’absence de réflexion sur la direction à prendre avant de commencer à coder.
Le succès dépend réellement de la nature du problème et de la conception du système, non des détails superficiels.
L’idée que Leslie Lamport essaie de faire passer ici est que pour toutes les tâches où aucune solution établie n’est disponible, "vous devez vous arrêter et réfléchir […] avant de commencer à coder" ; il affirme que "la réflexion est vraiment indépendante du processus d’écriture du code", qu’elle s’applique quelque soit le langage que vous utilisez. Parmi les aspects de la conception à bien considérer, Leslie Lamport cite la complexité algorithmique et la simplicité.
Aucune technique de programmation, ni aucun concept de langage ne vous offrira la simplicité de votre conception. La simplicité doit être atteinte au-delà du code, avant d’arriver au point où vous vous souciez de la façon dont vous allez effectivement implémenter telle ou telle chose.
Ceci nous amène directement au principal sujet auquel Leslie s’intéresse actuellement, à savoir la spécification et la vérification. Une spécification peut être n’importe quoi, "de quelques phrases en anglais à une description mathématique complètement formelle de ce que fait un programme et de comment il le fait". Tout type de spécification peut être utilisé de façon efficace en fonction du contexte. D’après Leslie, la caractéristique la plus importante d’une spécification est sa précision. C’est la raison pour laquelle il utilise les mathématiques et rejette l’utilisation d’UML, "un langage qui a d’abord été inventé, avant que les gens viennent s’y intéresser et essayer d’y ajouter une sémantique".
Une idée au sujet des spécifications formelles que Leslie essaie de dissiper est que celles-ci requièrent des compétences mathématiques qui ne seraient pas accessibles aux programmeurs : "Les mathématiques dont vous avez besoin pour écrire des spécifications sont beaucoup plus simples que n’importe quel langage de programmation […] Quiconque en capacité d’écrire du code en C ne devrait avoir aucun problème pour comprendre les bases mathématiques, car le C est bien plus compliqué que la logique de premier ordre, les ensembles et les fonctions". La part la plus complexe de l’équation est finalement d’acquérir la discipline requise à l’écriture d’une spécification formelle, surtout quand le programmeur n’a jamais réalisé de tâches de cette nature auparavant.
Le bénéfice d’utiliser un langage de spécifications formelles est que cela vous apprend à penser de façon rigoureuse, à réfléchir de façon précise ; c’est le point important. Donc ce que vous devez éviter à tout prix, c’est tout langage où tout est dans la syntaxe, rien dans la sémantique.
Leslie Lamport est employé par Microsoft Research et a récemment travaillé avec TLA+, un système logique qui combine la logique temporelle et une logique des actions, utilisé pour décrire le comportement des systèmes concurrents. Il est aussi le créateur de l’outil de préparation de documents LaTex.