Leslie Lamport remporte le « prix Nobel » de l’informatique

Leslie Lamport, un directeur de la recherche chez Microsoft Research, vient de remporter le prix A.M Turing Award 2013 de l’ACM, Association of Computing Machinery.

Doté de 250 000 $ (180 000 €), ce prix, en l’honneur d’Alan Mathison Turing, le mathématicien, cryptographe et informaticien anglais de génie, qui a profondément influencé le développement de l’informatique, est la plus haute récompense en informatique, l’équivalent de la médaille Fields en mathématiques ou du prix Nobel en physique.

 

Leslie Lamport

LeslieLamport_H500Lamport, né le 7 février 1941 à New-York, est récompensé pour ses contributions dans l’informatique distribuée : algorithmes, modélisation formelle et protocoles de vérification qui ont amélioré la performance, la conformité et la fiabilité des systèmes distribués. Les systèmes informatiques distribués sont à la base du Cloud, de jeux comme World of Warcraft ou de moteurs de recherche comme Google.

Mathématicien de formation (M.I.T., Brandeis University), Lamport a travaillé pour de nombreuses sociétés dont SRI International (née Stanford Research Institute), entreprise de recherche dans différents domaines scientifiques et technologiques au profit du gouvernement américain ou d’entreprises privées ; et Digital Equipment Corporation, l’inventeur du mini-ordinateur puis du processeur Alpha. Il travaille chez Microsoft Research Silicon Valley, où il aime aller en rollerblades, depuis 2001. Il est le cinquième scientifique de Microsoft Research à gagner cette récompense, après Tony Hoare, 1980, Butler W Lampson, 1992, Jim Gray (un homme d’une gentillesse remarquable avec lequel nous avons eu la chance de correspondre), 1998 et Chuck Thacker, 2009.

 

Contributions

Les contributions de Leslie se retrouvent dans tous les domaines clés de l’informatique : sécurité, Cloud, systèmes embarqués, bases de données, systèmes ; sa solution au problème des généraux byzantins contribue à éliminer les pannes dues à des composants défectueux quand ils interagissent avec d’autres composants.

Son langage temporel logic TLA+, qui permet de définir formellement avec les mathématiques, est largement utilisé pour les spécifications de haut niveau des systèmes informatiques distribués. Les outils associés, offerts en open source, permettent de valider des modèles et d’établir des preuves.

Il fait partie du projet Tools for Proof de Microsoft, qui est élaboré en coopération avec l’INRIA à Massy-Palaiseau.

Lamport a aussi développé LaTeX, un langage et un système de composition de documents qui est devenu le standard de fait de la communauté scientifique.

Son algorithme de Paxos, qui permet à un réseau d’ordinateurs de continuer de travailler de façon cohérente en dépit de pannes, sous-tend les moteurs de recherche google, Bing, le stockage de Windows Azure et bien d’autres systèmes.

Son algorithme de la boulangerie, un algorithme d’exclusion mutuelle (mutex) qui permet une utilisation efficace des ressources partagées dans un environnement multiprocesseurs. L’idée lui en est venu en se souvenant de ses visites dans les boulangeries dans sa jeunesse. Les clients prenaient un numéro et restaient dans la file d’attente jusqu’à l’appel de leur numéro. L’élément remarquable de l’algorithme est qu’il fonctionne toujours même si la lecture d’un numéro par un processus chevauche son écriture par un autre processus.

Auteur de plus de 170 papiers, son papier de 1978, Time, Clocks, and the Ordering of Events in a Distributed System, est parmi les plus cités de l’histoire de l’informatique. Il a signé l’an dernier un article pour le magazine Wired, Why We Should Build Software Like We Build Houses, dont l’idée est que quand on programme, il est avantageux de penser avant d’écrire du code. Il fut étonné de constater que l’idée était controversée.

 

Témoignages

Wen-Hann Wang, le vice-président en chef d’Intel en charge d’Intel Labs écrit :

« Son travail novateur sur les algorithmes distribués et simultanés, a amélioré considérablement les systèmes informatiques industriels et grand public, allant de la technologie multiprocesseurs utilisée dans les centres de traitement des données aux réseaux à ordinateurs multiples utilisés par les systèmes de contrôle des avions. En particulier, l’abstraction brillante d’ « horloge logique » qu’il a introduite il y a près de quarante ans, a eu un impact immense dans le secteur. Elle fournit un cadre élégant pour raisonner sur les protocoles distribués, un élément critique du monde interconnecté. »

Alfred Spector, le vice-président de la recherche de Google ajoute :

« Avec le passage à des systèmes distribués toujours plus grands et le Cloud computing, le travail de Lamport a un impact considérablement plus important. Les résultats de ses recherches ont profité à bien des communautés de recherche, notamment dans les systèmes parallèles et hautes performances, les algorithmes simultanés et la fiabilité logicielle. Les répercussions de son travail ne se limitent pas à la théorie, elles touchent les ingénieurs et les programmeurs de bien des systèmes. »

Bob Taylor, le fondateur du mythique Xerox Palo Alto Research Center note que:

« Internet es basé sur une technologie de systèmes distribués, elle même basée sur les fondations théoriques inventées par Leslie. Donc si vous aimez utilisez Internet, vous êtes redevables à Leslie.»

Lamport a déjà reçu plus de 16 récompenses pour ses recherches. Il est notamment Docteur honoris cause des universités de Rennes, de Kiel, de Lugano, de l’université Pointcarré de Nancy et de l’EPFL.

Il est membre de la National Academy of Sciences (Académie nationale des sciences), a reçu la médaille John von Neumann de l’IEEE et fait partie du panthéon du SIGOPS, le pôle d’intérêt commun des systèmes d’exploitation.

Le prix sera présenté lors de la célébration annuelle de l’ACM, le 21 juin 2014, à San Francisco.

 

Présentation vidéo de Leslie Lamport

 

Lamport sur les systèmes distribués sur Channel9

 

Bibliographie