Sites Inria

English version

Prix Turing

Olivier Lapirot - 3/06/2014

Leslie Lamport : un pionnier de l'informatique distribuée

Leslie Lamport Leslie Lamport - © Photo Bernard Lachaud

Le prix Turing 2013 de l'Association for Computing Machinery a été décerné cette année à Leslie Lamport, chercheur du laboratoire commun Inria-Microsoft Research. Retour sur quarante ans de travaux d’un chercheur qui met les mathématiques au service du numérique.

Comment faire travailler sans conflit plusieurs programmes sur un ordinateur ou faire collaborer plusieurs ordinateurs sur un réseau ? Ces problématiques complexes, connues sous le nom d’informatique distribuée, Leslie Lamport y a consacré une grande partie de ses travaux. Une contribution décisive à la recherche  récompensée par le prix Turing 2013, considéré comme le "Nobel de l’Informatique".

Après l'obtention de son doctorat en mathématiques en 1972, Leslie Lamport débute sa carrière dans le monde l’informatique en 1977 au sein de l'institut de recherche américain SRI International, puis, de 1985 à 2001, chez le fabricant d'ordinateurs DEC. Le scientifique intègre ensuite le centre de recherche de Microsoft. « Leslie aimait glisser une touche très personnelle dans ses travaux, en ancrant ses théories dans le réel , raconte Jean-Jacques Lévy , directeur de recherche émérite Inria. Trois algorithmes qui l'ont rendu célèbre portent ainsi des noms très concrets : l'algorithme de la boulangerie, l'algorithme des généraux byzantin et Paxos . »

Dans le premier cas, l’algorithme s'inspire de la file d'attente chez le boulanger : pour s'exécuter, chaque programme doit attendre son tour en fonction de son ordre d'arrivée. Dans les deuxième et troisième cas, il s'agit de permettre à plusieurs ordinateurs de prendre une décision commune malgré la présence de "traîtres" parmi eux ou de parlementaires défaillants... Des analogies que Leslie Lamport affectionne de pousser au maximum afin de couvrir toutes les possibilités. Quant à Paxos : c’est l’algorithme actuellement utilisé pour la synchronisation des serveurs de Bing ou de Google.

Mathématiques et informatique

Autre volet de ses travaux : la programmation. Pour le mathématicien, plutôt que de se lancer dans l'écriture d'instructions, il faut expliciter ce que le programme doit faire. Il invente pour cela un nouveau langage de programmation : TLA (Temporal logic of actions ). L’objectif : créer des instructions pour les programmes grâce à des  formules mathématiques logiques.  En 2006, il rejoint le laboratoire commun Inria-Microsoft Research pour développer une boîte à outils pour TLA+. « Sa boîte à outils voit le jour en 2010 , confie Jean-Jacques Lévy, alors directeur du laboratoire. Il s’agit d’un éditeur graphique dans lequel on peut entrer et modifier les spécifications. En parallèle, un système de démonstration automatique permet de vérifier que les résultats sont cohérents. À 73 ans, Leslie Lamport travaille toujours à son amélioration et passe pour cela trois mois par an en France à collaborer avec les chercheurs du Microsoft Research-Inria Joint Centre.  »

Mais ce n’est pas la seule innovation majeure à mettre à son actif dans le domaine des mathématiques appliquées à l’informatique. Dès 1983, Leslie Lamport crée le logiciel de mise en page LaTeX, version améliorée du programme TeX mis au point quelques années auparavant par Donald Knuth . LaTex permet d'écrire facilement les formules mathématiques les plus compliquées : toute la communauté scientifique l'utilise aujourd'hui pour rédiger les formules qui apparaissent dans les articles de recherche !

La cérémonie officielle de présentation du prix Turing aura lieu le 21 juin à San Francisco.

Mots-clés : Prix Turing Système distribué ACM Microsoft research

Haut de page

Suivez Inria