Microsoft Researcher Leslie Lamport has been named as the recipient of the 2013 ACM A.M. Turing Award (aka the computer science Nobel prize) for his work in distributed computing. 

The ACM A.M Turing Award is widely considered the "Nobel Prize in Computing", and carries a $250,000 prize, with financial support provided by Intel and Google.

The annual winner, an individual or two- or three-person team, is selected from among those nominated by a committee that is currently chaired by Adele Goldberg and includes two recent Turing Award winners, Leslie Valiant (2010) and Barbara Liskov (2008) among its eight member. Nominations close in November, the recipient is announced in March the following year and the award is presented at the ACM Annual Awards Banquet in June.

The citation for Leslie Lamport reads:

For fundamental contributions to the theory and practice of distributed and concurrent systems, notably the invention of concepts such as causality and logical clocks, safety and liveness, replicated state machines, and sequential consistency.

In this video current colleagues and past luminaries at Microsoft Research explain why Lamport deserves this award and congratulate him on its achievement.

According to the ACM he is being honored

for imposing clear, well-defined coherence on the seemingly chaotic behavior of distributed computing systems, in which several autonomous computers communicate with each other by passing messages. He devised important algorithms and developed formal modeling and verification protocols that improve the quality of real distributed systems. These contributions have resulted in improved correctness, performance, and reliability of computer systems.

Although it isn't specifically listed by the ACM the Bakery Algorithm, which Lamport devised in 1979 is perhaps the one that is best known and most widely used - at least in teaching Computer Science. It is the starting point for this 2010 Channel 9 video in which he talks with Erik Meijer about Mathematical Reasoning and Distributed Systems.

The discussion moves on to  Lamport Clocks, and here Lamport explains how it was influenced by Einstein's concept of Special Relativity. Later it covers TLA, the Temporal Logic of Actions,is a logic for specifying and reasoning about concurrent and reactive systems. TLA+, the latest incarnation of this formal specification toolset, open sourced last year.

As well as algorithms and tools for distributed systems Lamport has devised solutions for Byzantine Fault Tolerance that contribute to failure prevention in a system component that behaves erroneously when interacting with other components.

He is also the original author of LaTeX, the document preparation system and markup language that that is the de facto standard for  publishing scientific and academic papers.

Leslie Lamport's website has a list of 179 references as his "Collected Works" with PDFs of most of them. It's a portal to some fascinating reading.

Comments

Make a Comment or View Existing Comments Using Disqus

or email your comment to: comments@i-programmer.info