Leslie Lamport, prix Turing 2013

Le prix Turing récompense des chercheurs en informatique qui posent des bases sur lesquelles s’appuient non seulement leurs successeurs, mais aussi chacun d’entre nous. Cette année, c’est Leslie qui Lamport (© Shuba) pour ses contributions fondamentales à la théorie et la pratique des systèmes répartis 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éparties, et la cohérence séquentielle.

La suite en seconde partie.

Sommaire

• À la baguette
• Coucou !
• Le petit oiseau va sortir
• Et pourtant il faut vivre…
• Au commencement fut Chaos
• Les généraux byzantins
• Le parlement à temps partiel³
• Fenêtres sur cours

À la baguette

Utilisez‐vous un système qui exploite plusieurs programmes¹ ? Lorsque plusieurs processus s’exécutent simultanément, ils peuvent avoir besoin d’accéder à un même emplacement de mémoire. Tant qu’ils ne font que lire son contenu, il n’y a pas de problème, mais s’ils veulent le modifier, on ne peut pas les laisser le faire n’importe comment, sous peine de voir arriver dans cette zone de mémoire une valeur imprévue. C’est pour résoudre ce problème, appelé exclusion mutuelle, que Lamport a publié l’algorithme de la boulangerie, première solution ne nécessitant pas d’assistance de la part du matériel. De nombreuses solutions à ce problème existent de nos jours, chacune adaptée à un contexte bien particulier.

Coucou !

Prenons maintenant un peu de recul et considérons plusieurs programmes sur des machines différentes reliées en réseau. Nous avons maintenant un nouveau problème, car le temps de communication entre les machines, ajouté à l’inévitable décalage entre leurs horloges internes, rend difficile de dire dans quel ordre leurs opérations se sont produites. De Kevin ou de Jean‐Édouard, qui a tiré le premier dans leur partie de Half‐Halo² ? L’insertion de la valeur 42 dans la liste d’entiers partagée est‐elle arrivée avant ou après l’instruction demandant de supprimer toutes les valeurs paires ? Avec une [[horloge logique]], ce genre de questions prend un nouveau sens. Introduite par Lamport pour donner une fondation au concept de temps dans un système réparti, elle ne fait aucune référence au temps réel (celui de la pendule) et permet de raisonner en termes de causalité. Dans ce modèle, un évènement peut arriver avant un autre (par exemple, si A est l’émission d’un message et B sa réception, A est arrivé avant B) ou deux évènements peuvent être indépendants. Différents types d’horloges logiques existent aujourd’hui, qui donnent plus ou moins d’information sur la relation de causalité dans le système réparti (plus l’information est complète, plus le mécanisme de mise à jour des horloges logiques nécessite d’échanger des messages volumineux).

Le petit oiseau va sortir

Il est clair, à ce stade, qu’un système réparti est un sac de nœuds dans lequel il est difficile de mettre de l’ordre. Par exemple, savoir dans quel état se trouve le système à un moment donné est évidemment impossible. Ou pas. Plus précisément, si on ne peut pas obtenir l’état du système à un instant t (à la pendule), il est tout de même possible d’en obtenir une représentation cohérente (par exemple, dans cette représentation, si B a reçu le message M de A, alors A a envoyé le message M à B). L’algorithme du cliché distribué de Chandy et Lamport fournit une solution à ce problème essentiel, puisque sans cela, on ne pourrait pas savoir si le système a atteint un état satisfaisant les conditions attendues (autrement dit, si le système a bien calculé ce qu’on voulait lui faire calculer).

Et pourtant il faut vivre…

Plus largement, on aimerait bien pouvoir raisonner sur les systèmes répartis avec des outils logiques similaires à ceux que l’on utilise sur les algorithmes classiques afin de prouver leur correction. Ceci nécessite un nouvel outil : la logique temporelle, sur laquelle Lamport a beaucoup travaillé. Elle est basée sur deux types de propriétés la combinaison de propriétés de sûreté (A est toujours vrai) et de « vivacité » (B deviendra vrai dans le futur, on ne sait pas quand). En d’autres termes, une propriété de sûreté indique qu’une mauvaise chose n’arrivera jamais et une propriété de vivacité indique qu’une bonne chose finira par arriver. Toute propriété d’un système réparti peut être exprimée comme une combinaison de propriétés de sûreté et de vivacité. On doit à Lamport la logique TLA (Temporal Logic of Actions), le langage de spécification TLA+ et le langage algorithmique PlusCal, basés sur ces concepts et accompagnés d’outils libres (licence MIT).

Au commencement fut Chaos

Jouons un peu avec nos processus. Ils ont chacun un programme, auquel on ne touche pas, et une mémoire contenant des variables. Écrivons maintenant n’importe quoi dans ces variables. Que se passe‐t‐il ? Sans doute rien de bon. Sauf, peut‐être, si l’auteur du programme s’appelle Dijkstra, qui a introduit l’auto‐stabilisation en informatique. Son article de 1974 donne quelques programmes capables, après une période de convergence, de fonctionner malgré ces conditions radicales : essentiellement, ils sont capables de récupérer après n’importe quelle défaillance, au prix d’un manque de sûreté (on parle alors plutôt de sûreté inéluctable : on aura des propriétés de sûreté, mais on ne sait pas quand).

Ce résultat avait amusé quelques chercheurs à l’époque, puis était retombé dans l’oubli jusqu’à une présentation de Lamport, dix ans plus tard. Intitulée Solved Problems, Unsolved Problems and NonProblems in Concurrency, elle fait le point sur l’état de l’art dans ce domaine et, entre autres, déterre l’article de Dijkstra, suscitant l’intérêt d’autres chercheurs, ce que Lamport considère comme une de ses plus importantes contributions à l’informatique.

Les généraux byzantins

Constantinople, IX^e siècle. Les 101 généraux dalmatiens de l’armée byzantine doivent repousser l’envahisseur. Mais leurs troupes de Macédoine risquent de mal se mélanger, et donc d’attaquer sans se concerter. Les généraux doivent pourtant se mettre d’accord pour attaquer ou non. Cependant, certains d’entre eux sont des traîtres qui n’hésiteront pas, par exemple, à s’allier de façon à faire croire à un autre général que l’attaque est décidée pour la seule raison de l’envoyer tout seul au casse‐pipe.

Ce problème se retrouve en informatique dans un système comportant plusieurs processeurs dont certains fonctionnent mal, un type de défaillance plus pervers que l’arrêt définitif car beaucoup plus difficile à détecter. Un mauvais fonctionnement peut être dû à un défaut de fabrication, mais aussi à de mauvaises conditions (chaleur, rayons cosmiques…). Le problème des généraux byzantins est donc un bloc de construction fondamental pour la mise au point de tout système dans lequel une défaillance peut avoir des conséquences graves. Lamport, Pease et Shostak en ont apporté les premiers éléments théoriques : la preuve que le problème n’est résoluble que si le nombre de traîtres est strictement inférieur au tiers de l’effectif, ou à la moitié, si des signatures numériques sont utilisées, et les algorithmes correspondants.

Le parlement à temps partiel³

Reprenons le consensus, cette fois en présence de défaillances par arrêt définitif et dans un système asynchrone, c’est‐à‐dire qu’aucune condition n’est imposée sur le temps de transmission des messages. Un petit détail technique chagrine les chercheurs dans ce domaine : ce problème est insoluble (théorème de Fischer, Lynch et Paterson, 1985). Comme la recherche ne s’arrête pas pour si peu, de nombreux algorithmes existent pour résoudre le consensus dans des conditions proches de l’asynchronisme. On doit à Lamport l’algorithme (ou, si l’on préfère, le concept duquel on peut tirer des algorithmes) de Paxos, dans lequel le système reste toujours cohérent et qui garantit la progression vers le consensus dès lors qu’une majorité des processus fonctionnent correctement. Cet algorithme est également connu pour la mise en scène de son auteur sur le thème d’une cité grecque fictive, avec des présentations en costume d’archéologue, et par son utilisation par Google dans Chubby, dont dépendent notamment le Google File System et BigTable. Plusieurs versions étendues ont été proposées, dont une qui résout le consensus byzantin.

Fenêtres sur cours

Lamport est employé par Microsoft Research, ce qui ne signifie pas qu’il travaille sur la prochaine version de Windows. Ce francophone est membre du laboratoire INRIA-Microsoft de Palaiseau, dans l’Essonne, et collabore régulièrement avec des chercheurs français qui participent à la formation des futures générations d’informaticiens qui sauront, grâce à Lamport, qu’un système réparti est un système dans lequel la défaillance d’un ordinateur dont vous ne saviez même pas qu’il existait peut rendre le vôtre inutilisable.

NdM : Leslie Lamport est aussi à l’origine de LaTeX — disons  — en 1983.

⁽¹⁾ Et sinon, comment êtes‐vous arrivé(e) sur LinuxFr.org ?
⁽²⁾ D’accord, mauvais exemple : on sait que c’est Han Solo qui a tiré le premier.
⁽³⁾ Ceci n’est pas un appeau à trolls politiques.

Aller plus loin

• Page personnelle de Leslie Lamport (681 clics)
• Publications de Leslie Lamport, avec ses commentaires (154 clics)
• Page de l’ACM sur l’attribution du prix Turing à Lamport (81 clics)