Si nous pouvions voyager dans le temps jusqu’en 1974, peut-être aurions-nous trouvé Leslie Lamport dans sa boulangerie de quartier très fréquentée, aux prises avec le problème suivant. La boulangerie avait plusieurs caissières, mais si plus d’une personne s’approchait d’une seule caissière en même temps, celle-ci essayait de leur parler à toutes en même temps et devenait confuse. M. Lamport s’est rendu compte qu’il devait y avoir un moyen de garantir que les personnes s’approchent des caissières une par une. Ce problème a rappelé à Lamport une question posée dans un article antérieur par l’informaticien Edsger Dijkstra sur un autre problème banal : comment partager les ustensiles de table autour d’une table à manger. L’un des défis de coordination était de garantir que chaque ustensile était utilisé par au plus un diner à la fois, ce qui a été généralisé sous le nom de problème d’exclusion mutuelle, exactement le défi auquel Lamport a été confronté à la boulangerie.

Un matin de 1974, une idée est venue à Lamport sur la façon dont les clients de la boulangerie pourraient résoudre l’exclusion mutuelle entre eux, sans compter sur l’aide de la boulangerie. Cela fonctionnait à peu près comme suit : les gens choisissent des numéros lorsqu’ils entrent dans la boulangerie, et sont ensuite servis à la caisse en fonction de leur commande de numéros. Pour choisir un numéro, une cliente demande le numéro de toutes les personnes qui l’entourent et choisit un numéro plus élevé que tous les autres.

Cette idée simple est devenue un algorithme élégant pour résoudre le problème de l’exclusion mutuelle sans nécessiter d’opérations indivisibles de niveau inférieur. C’était aussi une riche source d’idées futures, puisque de nombreux problèmes devaient être résolus. Par exemple, certains clients de la boulangerie prenaient beaucoup de temps pour vérifier d’autres numéros, et pendant ce temps, d’autres clients arrivaient et sélectionnaient d’autres numéros. Une autre fois, le gérant de la boulangerie voulait avoir un aperçu de tous les numéros des clients afin de préparer suffisamment de pâtisseries. Lamport a déclaré plus tard : « Pendant les quelques années qui ont suivi ma découverte de l’algorithme de la boulangerie, tout ce que j’ai appris sur la concurrence est venu de son étude. »

L’algorithme de la boulangerie et les autres travaux pionniers de Lamport — dont beaucoup ont des noms amusants et des paraboles associées — sont devenus des piliers de l’informatique. Sa collection constitue le fondement de vastes domaines de la concurrence, et a influencé la spécification, le développement et la vérification des systèmes concurrents.

Après avoir obtenu un doctorat en mathématiques de l’Université Brandeis en 1972, Lamport a travaillé comme informaticien chez Massachusetts Computer Associates de 1970 à 1977, chez SRI International de 1977 à 1985, et au centre de recherche sur les systèmes de Digital Equipment Corporation (plus tard propriété de Compaq) de 1985 à 2001. En 2001, il a rejoint Microsoft Research à Mountain View, en Californie.

Passer sa carrière de chercheur dans des environnements de recherche industrielle n’était pas un accident. « J’aime travailler dans un laboratoire de recherche industrielle, en raison de l’apport », a déclaré Lamport. « Si je travaillais seul et que je trouvais des problèmes, je trouverais un petit nombre de choses, mais si je vais dans le monde, où les gens travaillent sur de vrais systèmes informatiques, il y a un million de problèmes. Quand je regarde en arrière sur la plupart des choses sur lesquelles j’ai travaillé – les généraux byzantins, Paxos – ils sont venus de problèmes du monde réel. »

Ses travaux ont fait la lumière sur les questions fondamentales des programmes concurrents, pour lesquels il n’y avait pas de théorie formelle à l’époque. Il s’est attaqué à des concepts fondamentaux tels que la causalité et le temps logique, les registres partagés atomiques et réguliers, la cohérence séquentielle, la réplication des machines à états, l’accord byzantin et la liberté d’attente. Il a travaillé sur des algorithmes qui sont devenus des pratiques d’ingénierie standard pour les systèmes distribués tolérants aux pannes. Il a également développé un important corpus de travaux sur la spécification et la vérification formelles des systèmes concurrents, et a contribué au développement d’outils automatisés appliquant ces méthodes. Nous n’aborderons que certaines de ses contributions.

1. Solutions d’exclusion mutuelle et l’algorithme Bakery

Les travaux influents de Lamport des années 1970 et 1980 sont arrivés à un moment où l’on ne comprenait que très peu les problèmes fondamentaux de la programmation pour de multiples processeurs concurrents.

Par exemple, on savait que l’exécution correcte peut exiger que les activités parallèles s’excluent les unes les autres pendant les périodes de « sections critiques » où elles manipulent les mêmes données, afin d’éviter l’imbrication indésirable des opérations. L’origine de ce problème d’exclusion mutuelle remonte aux travaux pionniers d’Edsger Dijkstra, qui a notamment proposé une solution. L’algorithme de Dijkstra, bien que correct, dépend de l’atomicité des accès à la mémoire partagée, c’est-à-dire qu’un processeur qui lit alors qu’un autre écrit devra attendre, plutôt que de renvoyer une valeur éventuellement brouillée. En un sens, il construit une solution de haut niveau à partir de l’exclusion mutuelle de bas niveau déjà implémentée par le matériel.

L’algorithme de la boulangerie de Lamport, remarquablement élégant et intuitif, ne fait pas cela. Sa solution organise les processus en compétition dans une file d’attente implicite en fonction de leur ordre d’arrivée, un peu comme une file d’attente dans une boulangerie. Pourtant, peu importe qu’un processeur lisant des données en cours de mise à jour par un autre processeur reçoive des déchets. L’algorithme fonctionne toujours.

Lamport se souvient de sa découverte de l’algorithme Bakery.

L’algorithme Bakery est devenu un matériau de manuel, et la plupart des étudiants de premier cycle en informatique le rencontrent au cours de leurs études.

2. Fondements de la programmation concurrente

Plusieurs nouveaux concepts importants ont émané du travail sur l’algorithme de Bakery, une tendance qui s’est répétée plusieurs fois dans la carrière de Lamport. L’expérience de la conception d’algorithmes concurrents et de la vérification de leur exactitude l’a amené à se concentrer sur les fondements de base qui permettraient aux multiprocesseurs de se comporter d’une manière sur laquelle les programmeurs peuvent raisonner mathématiquement. Tout en travaillant sur une solution pour un problème concret spécifique, Lamport a inventé des abstractions et des règles générales nécessaires pour raisonner sur sa correction, et ces contributions conceptuelles sont ensuite devenues des piliers théoriques de la programmation concurrente.

Loop-freedom : Les travaux sur l’algorithme Bakery ont introduit un concept important appelé « loop freedom ». Certaines solutions évidentes qui viennent à l’esprit pour le problème de l’exclusion mutuelle pré-attribuent des `tours’ de rotation entre les processus. Mais cela oblige les processus à attendre les autres qui sont lents et n’ont même pas encore atteint le point de discorde. En utilisant l’analogie de la boulangerie, cela reviendrait à arriver dans une boulangerie vide et à devoir attendre un client qui n’est même pas encore arrivé à la boulangerie. En revanche, la liberté de boucle exprime la capacité des processus à progresser indépendamment de la vitesse des autres processus. Comme l’algorithme de la boulangerie attribue des tours aux processus dans l’ordre de leur arrivée, il possède la liberté de boucle. Il s’agit d’un concept crucial qui a été utilisé dans la conception de nombreux algorithmes ultérieurs et dans la conception des architectures de mémoire. La liberté d’attente, une condition exigeant une progression indépendante malgré les échecs, trouve ses racines évidentes dans la notion de liberté de boucle et le concept de porte de boulangerie. Elle a ensuite été largement explorée par d’autres, dont Maurice Herlihy .

Consistance séquentielle : Travailler avec une architecture multi-cœur qui avait une mémoire cache distribuée a conduit Lamport à créer des spécifications formelles pour un comportement cohérent du cache dans les systèmes multiprocesseurs. Ce travail a mis de l’ordre dans le chaos de ce domaine en inventant la cohérence séquentielle , qui est devenue l’étalon-or des modèles de cohérence de la mémoire. Cette notion simple et intuitive fournit juste le bon niveau d' »atomicité » pour permettre aux logiciels de fonctionner. Aujourd’hui, nous concevons des systèmes matériels avec un ordre d’horodatage ou un ordre de stockage partiel, auxquels nous ajoutons des instructions de clôture de mémoire, ce qui permet aux programmeurs de faire en sorte que le matériel semble cohérent sur le plan séquentiel. Les programmeurs peuvent alors mettre en œuvre des algorithmes qui offrent des propriétés de cohérence fortes. C’est la clé des modèles de cohérence de la mémoire de Java et de C++. Nos processeurs multicœurs fonctionnent aujourd’hui sur la base de principes décrits par Leslie Lamport en 1979.

Registres atomiques et réguliers : L’algorithme Bakery a également conduit Lamport à s’interroger sur la sémantique précise de la mémoire lorsque plusieurs processus interagissent pour partager des données. Il lui a fallu près d’une décennie pour la formaliser, et le résultat est l’abstraction des registres réguliers et atomiques .

Sa théorie donne à chaque opération sur un registre partagé une durée explicite, commençant par une invocation et se terminant par un résultat. Les registres peuvent être implémentés par diverses techniques, comme la réplication. Néanmoins, les interactions des processus avec un registre atomique sont censées « ressembler » à des accès en série à la mémoire partagée réelle. La théorie comprend également une sémantique d’interaction plus faible, comme celle d’un registre régulier. Un registre régulier capture les situations dans lesquelles les processus lisent différentes répliques du registre pendant qu’il est mis à jour. À tout moment, certaines répliques peuvent être mises à jour alors que d’autres ne le sont pas, et finalement, toutes les répliques contiendront la valeur mise à jour. De manière importante, cette sémantique plus faible suffit à supporter l’exclusion mutuelle : l’algorithme Bakery fonctionne correctement si un lecteur chevauchant un écrivain obtient en retour n’importe quelle valeur arbitraire.

Lamport décrit son travail pour définir précisément les abstractions pour les registres atomiques, réguliers et sûrs.

Ce travail a initié un sous-domaine distinct de recherche en informatique distribuée qui est toujours florissant. Les objets atomiques de Lamport ne supportaient que les opérations de lecture et d’écriture, c’est-à-dire qu’ils étaient des registres atomiques. La notion a été généralisée à d’autres types de données par Maurice Herlihy et Jeannette Wing, et leur terme « linéarisabilité » est devenu synonyme d’atomicité. Aujourd’hui, essentiellement tous les systèmes de stockage non relationnels développés par des sociétés comme Amazon, Google et Facebook adoptent la linéarisabilité et la cohérence séquentielle pour leurs garanties de cohérence des données.

3. Fondements des systèmes distribués

Un type spécial de système concurrent est un système distribué, caractérisé par le fait d’avoir des processus qui utilisent des messages pour interagir les uns avec les autres. Leslie Lamport a eu un impact énorme sur la façon dont nous pensons au système distribué, ainsi que sur les pratiques d’ingénierie du domaine.

Les horloges logiques : Beaucoup de gens ont réalisé qu’une notion globale du temps n’est pas naturelle pour un système distribué. Lamport a été le premier à rendre précise une notion alternative d' »horloges logiques », qui imposent un ordre partiel aux événements basé sur la relation causale induite par l’envoi de messages d’une partie du système à une autre . Son article intitulé « Time, Clocks, and the Ordering of Events in a Distributed System » est devenu le plus cité des travaux de Lamport, et dans le langage informatique, les horloges logiques sont souvent surnommées timestamps de Lamport. Son article a remporté le 2000 Principles of Distributed Computing Conference Influential Paper Award (plus tard renommé Edsger W. Dijkstra Prize in Distributed Computing), et il a remporté un ACM SIGOPS Hall of Fame Award en 2007.

Lamport décrit son article « Time, Clocks… » et sa relation avec la relativité restreinte.

Pour comprendre pourquoi ce travail est devenu si influent, reconnaissez qu’au moment de l’invention, il n’y avait pas de bon moyen de capturer le retard de communication dans les systèmes distribués, sauf en utilisant le temps réel. Lamport a réalisé que le délai de communication rendait ces systèmes très différents d’un système multiprocesseur à mémoire partagée. L’intuition est venue en lisant un article sur les bases de données répliquées et en réalisant que son ordonnancement logique des commandes pouvait violer la causalité.

L’utilisation de l’ordonnancement des événements comme moyen de prouver la correction du système est principalement ce que les gens font aujourd’hui pour les preuves intuitives des algorithmes de synchronisation simultanée. Une autre contribution puissante de ce travail a été de démontrer comment répliquer une machine d’état en utilisant des horloges logiques, ce qui est expliqué ci-dessous.

Des instantanés distribués : Une fois que vous définissez l’ordre causal, la notion d’états globaux cohérents suit naturellement. Cela a conduit à un autre travail perspicace. Lamport et Mani Chandy ont inventé le premier algorithme pour lire l’état (prendre un `snapshot’) d’un système distribué arbitraire . Cette notion est si puissante que d’autres l’ont ensuite utilisée dans différents domaines, comme les réseaux, l’auto-stabilisation, le débogage et les systèmes distribués. Cet article a reçu le 2013 ACM SIGOPS Hall of Fame Award.

4. Tolérance aux pannes et réplication de la machine d’état

« Un système distribué est un système dans lequel la défaillance d’un ordinateur dont vous ne connaissiez même pas l’existence peut rendre votre propre ordinateur inutilisable » est une célèbre boutade de Lamport. Une grande partie de son travail concerne la tolérance aux pannes.

La réplication des machines à états (SMR) : Peut-être la plus significative des nombreuses contributions de Lamport est le paradigme de la réplication de la machine d’état, qui a été introduit dans le célèbre article sur « Time, Clocks, and the Ordering of Events in a Distributed System », et développé peu après . L’abstraction capture tout service comme une machine d’état centralisée — une sorte de moteur de calcul universel similaire à une machine de Turing. Elle possède un état interne et traite les commandes en séquence, chacune donnant lieu à un nouvel état interne et produisant une réponse. Lamport a réalisé que la tâche décourageante de répliquer un service sur plusieurs ordinateurs peut être rendue remarquablement simple si vous présentez la même séquence de commandes d’entrée à toutes les répliques et qu’elles procèdent à une succession identique d’états.

Ce paradigme perspicace de la SMR est à la base de nombreux systèmes fiables, et est considéré comme une approche standard pour la construction de systèmes distribués répliqués en raison de son élégance. Mais avant que Lamport ne développe une solution complète utilisant pour SMR, il devait aborder un ingrédient de base, l’accord, qui a été abordé dans son travail suivant.

Accord byzantin : Alors que les approches de machine d’état qui sont résilientes aux fautes de crash sont suffisantes pour de nombreuses applications, les systèmes plus critiques, comme pour l’avionique, ont besoin d’un modèle encore plus extrême de tolérance aux fautes qui est imperméable aux nœuds qui pourraient perturber le système de l’intérieur.

Au Stanford Research Institute (appelé plus tard SRI International) dans les années 1970, Lamport faisait partie d’une équipe qui a aidé la NASA à concevoir un système de contrôle avionique robuste. Les garanties formelles étaient une nécessité absolue en raison de la nature critique de la mission. La sécurité devait être garantie contre les dysfonctionnements les plus extrêmes du système que l’on puisse imaginer. L’un des premiers défis que l’équipe du SRI a dû relever consistait à prouver l’exactitude d’un système de contrôle du cockpit, conçu par la NASA, à l’aide de trois systèmes informatiques qui utilisent le vote majoritaire pour masquer tout composant défectueux.

Le résultat du travail de l’équipe a été plusieurs concepts fondamentaux et des aperçus concernant ces types stricts de systèmes robustes. Il s’agissait notamment d’une définition fondamentale de la robustesse dans ce cadre, d’une abstraction du problème de coordination qui sous-tend tout système répliqué à ce jour, et d’une révélation surprenante que les systèmes avec trois ordinateurs ne peuvent jamais faire fonctionner en toute sécurité un cockpit critique de mission !

En effet, dans deux travaux séminaux (« LPS ») publiés avec Pease et Shostak , l’équipe a d’abord identifié une vulnérabilité quelque peu particulière. LPS postule qu' »un composant défaillant peut présenter un type de comportement souvent négligé — à savoir, envoyer des informations contradictoires à différentes parties du système ». Plus généralement, un composant défaillant pouvait fonctionner d’une manière totalement incompatible avec son comportement prescrit, et pouvait sembler presque malveillant.

Le nouveau modèle de défaillance avait besoin d’un nom. À l’époque, il existait un défi classique connexe consistant à coordonner deux ordinateurs communicants, présenté dans un article de 1975 et désigné par Jim Gray en comme le « Paradoxe des deux généraux ». Cela a conduit Lamport à considérer les ordinateurs de contrôle dans un cockpit comme une armée de généraux byzantins, l’armée essayant de former une attaque coordonnée alors que des traîtres internes envoyaient des signaux contradictoires. Ce modèle de défaillance a été baptisé « défaillances byzantines » et a donné lieu à une multitude de travaux universitaires. Le modèle de défaillance byzantine est toujours utilisé pour capturer le pire type de mésaventures et de failles de sécurité dans les systèmes.

Lamport explique son utilisation d’une histoire sur les « généraux byzantins » pour encadrer un problème dans les systèmes distribués tolérants aux fautes.

Les défaillances byzantines analysent les mauvaises choses qui peuvent se produire. Mais qu’en est-il des bonnes choses qui doivent se produire ? LPS a également donné une formulation abstraite du problème de parvenir à une coordination malgré les échecs byzantins ; ce problème est connu sous le nom d' »accord byzantin ». Cette formulation succincte exprime la tâche de coordination du contrôle comme le problème de la formation d’une décision d’accord pour un bit individuel, en commençant par des bits potentiellement différents en entrée de chaque composant. Une fois l’accord obtenu sur un seul bit, il est possible de l’utiliser de manière répétée afin de maintenir la coordination d’un système complexe entier. L’article montre que quatre ordinateurs sont nécessaires pour se mettre d’accord sur un seul bit face à un seul dysfonctionnement. Trois ne sont pas suffisants, car avec trois unités, une unité défectueuse peut envoyer des valeurs contradictoires aux deux autres unités, et former une majorité différente avec chacune d’elles. Plus généralement, ils ont montré que 3F+1 unités sont nécessaires pour surmonter F composants simultanément défectueux. Pour prouver cela, ils ont utilisé un bel argument de symétrie qui est devenu connu sous le nom d' »argument de l’hexagone ». Cet argument archétype a trouvé d’autres utilisations chaque fois que l’on soutient qu’une unité défectueuse qui envoie des informations conflictuelles à différentes parties du système semble indiscernable d’une situation symétrique dans laquelle les rôles corrects et défectueux sont inversés.

LPS a également démontré que 3F+1 unités sont suffisantes, et ils ont présenté une solution pour atteindre un accord byzantin entre les 3F+1 unités dans F+1 tours de communication synchrone. Ils ont également montré que si vous utilisez des signatures numériques, seulement 2F+1 unités sont suffisantes et nécessaires.

Le problème de l’accord byzantin et ses solutions sont devenus la marque de fabrique des systèmes tolérants aux pannes. La plupart des systèmes construits avec la redondance l’utilisent en interne pour la réplication et la coordination. Lamport lui-même l’a utilisé plus tard pour former le paradigme de la réplication de la machine d’état discuté ensuite, qui donne la base algorithmique de la réplication.

Le papier de 1980 a reçu le prix Edsger W. Dijkstra 2005 en informatique distribuée, et le papier de 1982 a reçu le prix Jean-Claude Laprie en informatique fiable.

Paxos : Avec une compréhension croissante du problème de l’accord pour l’informatique distribuée, il était temps pour Lamport de revenir à la réplication des machines d’état et d’y traiter les défaillances. La première solution SMR qu’il a présentée dans son article de 1978 suppose qu’il n’y a pas de défaillances, et elle utilise le temps logique pour faire passer les répliques par la même séquence de commandes. En 1989, Lamport a conçu un algorithme tolérant aux pannes appelé Paxos . Poursuivant sa tendance à raconter des paraboles humoristiques, le document présente l’histoire imaginaire d’un parlement gouvernemental sur une ancienne île grecque nommée Paxos, où l’absence d’un nombre quelconque de ses membres, ou peut-être de tous, peut être tolérée sans perdre la cohérence.

Lamport décrit les origines de son algorithme Paxos pour le calcul distribué tolérant aux pannes.

Malheureusement, la mise en place comme une parabole grecque a rendu le papier difficile à comprendre pour la plupart des lecteurs, et il a fallu neuf ans entre la soumission et la publication en 1998. Mais le rapport technique du DEC de 1989 a été remarqué. Le collègue de Lamport, Butler Lampson, a évangélisé l’idée auprès de la communauté de l’informatique distribuée. Peu de temps après la publication de Paxos, le système Chubby de Google et le ZooKeeper open-source d’Apache ont proposé la réplication de la machine d’état comme un service externe largement déployé.

Paxos coud une succession de décisions d’accord en une séquence de commandes de la machine d’état de manière optimisée. Il est important de noter que la première phase de la composante d’accord donnée dans l’article de Paxos (appelée Synode) peut être évitée lorsque le même leader préside à plusieurs décisions ; cette phase ne doit être exécutée que lorsqu’un leader doit être remplacé. Cette percée perspicace explique en grande partie la popularité de Paxos, et a été appelée plus tard Multi-Paxos par l’équipe de Google. L’article de Lamport sur Paxos a remporté le prix Hall of Fame de l’ACM SIGOPS (Special Interest Group on Operating Systems) en 2012.

SMR et Paxos sont devenus le cadre standard de facto pour concevoir et raisonner sur les méthodes de consensus et de réplication. De nombreuses entreprises construisant des systèmes d’information critiques, notamment Google, Yahoo, Microsoft et Amazon, ont adopté les fondements de Paxos.

5. Spécification formelle et vérification des programmes

Dans les premiers jours de la théorie de la concurrence, le besoin est apparu de bons outils pour décrire les solutions et prouver leur exactitude. Lamport a apporté des contributions centrales à la théorie de la spécification et de la vérification des programmes concurrents. Par exemple, il a été le premier à articuler les notions de propriétés de sécurité et de propriétés de lividité pour les algorithmes distribués asynchrones. Il s’agissait de la généralisation des propriétés de « correction partielle » et de « correction totale » précédemment définies pour les programmes séquentiels. Aujourd’hui, les propriétés de sécurité et de lividité forment la classification standard pour les propriétés de correction des algorithmes distribués asynchrones.

Un autre travail, avec Martin Abadi , a introduit une abstraction spéciale appelée variables de prophétie à un modèle d’algorithme, pour gérer une situation où un algorithme résout un choix non déterministe avant que la spécification ne le fasse. Abadi et Lamport ont mis en évidence des situations où de tels problèmes se posent, et ont développé la théorie nécessaire pour soutenir cette extension de la théorie. De plus, ils ont prouvé que lorsqu’un algorithme distribué rencontre une spécification, où les deux sont exprimés en tant que machines à états, la correspondance entre eux peut être prouvée en utilisant une combinaison de variables de prophétie et de notions précédentes telles que les variables d’histoire. Ce travail a remporté le prix LICS Test-Of-Time 2008.

Langages de modélisation formelle et outils de vérification : En plus du développement des notions de base ci-dessus, Lamport a développé le langage TLA (Temporal Logic of Actions) et l’ensemble d’outils TLA+, pour la modélisation et la vérification des algorithmes et des systèmes distribués.

Lamport décrit TLA et sa connexion à la cartographie de raffinement.

TLA et TLA+ supportent la spécification et la preuve des propriétés de sécurité et de lividité, en utilisant une notation basée sur la logique temporelle. Lamport a supervisé le développement d’outils de vérification basés sur TLA+, notamment le model checker TLC construit par Yuan Yu. TLA+ et TLC ont été utilisés pour décrire et analyser des systèmes réels. Par exemple, ces outils ont été utilisés pour trouver une erreur majeure dans le protocole de cohérence utilisé dans le matériel de la Xbox 360 de Microsoft avant sa sortie en 2005. Chez Intel, il a été utilisé pour l’analyse d’un protocole de cohérence du cache de l’Intel Quick Path Interconnect tel qu’implémenté dans le processeur central Nehalem. Pour apprendre aux ingénieurs à utiliser ses outils de spécification formelle, Lamport a écrit un livre . Plus récemment, Lamport a développé le langage formel PlusCAL et des outils pour une utilisation dans la vérification des algorithmes distribués ; ce travail s’appuie sur TLA+.

6. LaTeX

Lorsqu’on crée une si vaste collection d’articles percutants, il est naturel de souhaiter un outil de composition pratique. Lamport ne s’est pas contenté d’en souhaiter un, il en a créé un pour toute la communauté. En dehors du domaine de la concurrence, Lamport a créé le système Latex, un ensemble de macros à utiliser avec le système de composition TeX de Donald Knuth. LaTeX a ajouté trois choses importantes à TeX :

1. Le concept d' »environnement de composition », qui avait pris naissance dans le système Scribe de Brian Reid.
2. Une forte insistance sur le balisage structurel plutôt que typographique.
3. Une conception de document générique, suffisamment flexible pour être adéquate pour une grande variété de documents.

Lamport n’est pas à l’origine de ces idées, mais en les poussant aussi loin que possible, il a créé un système qui fournit la qualité de TeX et beaucoup de sa flexibilité, mais qui est beaucoup plus facile à utiliser. Latex est devenu la norme de facto pour la publication technique en informatique et dans de nombreux autres domaines.

Il existe de nombreux autres articles importants de Leslie Lamport — trop nombreux pour être décrits ici. Ils sont listés par ordre chronologique sur la page d’accueil de Lamport , accompagnés de notes historiques qui décrivent la motivation et le contexte de chaque résultat.

Chaque fois que vous accédez à un ordinateur moderne, vous êtes susceptible d’être impacté par les algorithmes de Leslie Lamport. Et tout ce travail a commencé par la quête de comprendre comment organiser une file d’attente dans une boulangerie locale.

Auteur : Dahlia Malkhi
Contributeurs supplémentaires : Martin Abadi, Hagit Attiya, Idit Keidar,
Nancy Lynch, Nir Shavit,
George Varghese, et Len Shustek

.