{"id":284843,"date":"2014-03-18T06:00:34","date_gmt":"2014-03-18T13:00:34","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?p=284843"},"modified":"2016-09-09T09:52:57","modified_gmt":"2016-09-09T16:52:57","slug":"leslie-lamport-receives-turing-award","status":"publish","type":"post","link":"https:\/\/www.microsoft.com\/en-us\/research\/blog\/leslie-lamport-receives-turing-award\/","title":{"rendered":"Leslie Lamport Receives Turing Award"},"content":{"rendered":"<div id=\"attachment_284852\" style=\"width: 310px\" class=\"wp-caption alignleft\"><img loading=\"lazy\" decoding=\"async\" aria-describedby=\"caption-attachment-284852\" class=\"size-full wp-image-284852\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/Leslie-Lamport.jpg\" alt=\"Leslie Lamport\" width=\"300\" height=\"450\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/Leslie-Lamport.jpg 300w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/Leslie-Lamport-200x300.jpg 200w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><p id=\"caption-attachment-284852\" class=\"wp-caption-text\">Leslie Lamport<\/p><\/div>\n<p><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/lamport\/\" target=\"_blank\">Leslie Lamport<\/a> first began dabbling in computers while he was still in high school. Nothing too unusual about that\u2014until you consider that this was in the mid-1950s. Lamport was attending the Bronx High School of Science in New York, and he and a friend used to scrounge around, looking for discarded vacuum tubes to build a digital circuit.<\/p>\n<p>The path to greatness begins with baby steps, and for Lamport, a principal researcher with Microsoft Research, that teenage curiosity has yet to be quenched. Over the ensuing decades, he has become a veritable legend in computing circles. His work in the theory of distributed computing is foundational. His 1978 paper <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/time-clocks.pdf\" target=\"_blank\"><em>Time, Clocks, and the Ordering of Events in a Distributed System<\/em><\/a> is one of the most cited in the history of computer science. And he has contributed core principles to the field of specification and verification of concurrent systems.<\/p>\n<p>On March 18, in recognition of these invaluable advances, the Association for Computing Machinery (ACM) <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.acm.org\/news\/featured\/awards\/turing-award-2013\" target=\"_blank\">named Lamport the 2013 winner<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> of the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/amturing.acm.org\/\" target=\"_blank\">A.M. Turing Award<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, widely regarded as the Nobel Prize of computing.<\/p>\n<p>For many, such recognition couldn\u2019t be more deserved:<\/p>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"https:\/\/news.microsoft.com\/exec\/bill-gates\/#sm.0000gqo4eo15xzcr2xpufp6krucav\" target=\"_blank\">Bill Gates<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>: \u201cThis is well-deserved recognition for a remarkable scientist. As a leader in defining many of the key concepts of distributed computing that enable today\u2019s mission-critical computer systems, Leslie has done great things not just for the field of computer science, but also in helping make the world a safer place. Countless people around the world benefit from his work without ever hearing his name. I like to think this award is also recognition of the amazing work of Microsoft Research, which has become a great home for scientists and engineers who want to tackle the industry\u2019s most difficult challenges. Leslie is a fantastic example of what can happen when the world\u2019s brightest minds are encouraged to push the boundaries of what\u2019s possible.\u201d<\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/blampson\/\" target=\"_blank\">Butler Lampson<\/a>, a technical fellow at <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/lab\/microsoft-research-new-england\/\" target=\"_blank\">Microsoft Research New England<\/a> and the Turing winner in 1992: \u201cLeslie\u2019s contributions to both the theory and the practice of concurrent systems are unsurpassed for quality, scope, and importance. They are on a par with those of Dijkstra, Hoare, Milner, and Pneuli, all previous winners of the Turing Award. Although he can prove theorems with the best of them, his greatest strength is as an applied mathematician with an extraordinary sense of how to apply the tools of mathematics to problems of great practical importance.\u201d<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"https:\/\/news.microsoft.com\/exec\/harry-shum\/#sm.00000ps1d7lkg5e8owbo91rvt5j5y\" target=\"_blank\">Harry Shum<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, Microsoft executive vice president of Technology and Research: \u201cI really started to appreciate the incredible contribution his work has made to our industry, especially in cloud computing and distributed systems, when I worked at <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.bing.com\/\" target=\"_blank\">Bing<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>. At Bing, we studied his paper on Paxos and applied his technology to build the distributed systems that we still use today.\u201d<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"https:\/\/academic.microsoft.com\/#\/detail\/2180706138\" target=\"_blank\">Nancy Lynch<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, head of the Theory of Distributed Systems research group for the Computer Science and Artificial Intelligence Laboratory at the Massachusetts Institute of Technology: \u201cI\u2019m very delighted that Leslie was selected for the Turing Award this year. In fact, I think the award is very long overdue. He has made many foundational contributions to the field of distributed computing, starting in the 1970s.\u201d<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.cs.washington.edu\/people\/faculty\/lazowska\" target=\"_blank\">Ed Lazowska<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, Bill & Melinda Gates Chair in the Computer Science & Engineering department in the Computer Science & Engineering department at the University of Washington: \u201cWhen I think about Leslie&#8217;s impact, I think about the fact that the algorithms that he designed, which in many cases were viewed as only of theoretical interest, are now fundamental to the way we build web-scale systems, the systems that all of us use every day. Without Leslie&#8217;s innovations, we wouldn&#8217;t have the computing environment that we have today.\u201d<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/en.wikipedia.org\/wiki\/Robert_Taylor_(computer_scientist)\" target=\"_blank\">Bob Taylor<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, founder and manager of the Xerox Palo Alto Research Center and then founder and manager of Digital Equipment Corp.\u2019s Systems Research Center: \u201cThe Internet is based on distributed-systems technology, which is, in turn, based on a theoretical foundation invented by Leslie. So if you enjoy using the Internet, then you owe Leslie.\u201d<\/li>\n<\/ul>\n<div id=\"attachment_284861\" style=\"width: 410px\" class=\"wp-caption alignleft\"><img loading=\"lazy\" decoding=\"async\" aria-describedby=\"caption-attachment-284861\" class=\"size-full wp-image-284861\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/Turing-Award-winners.jpg\" alt=\"Tu ring Award winners Chuck Thacker and Leslie Lamport\" width=\"400\" height=\"273\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/Turing-Award-winners.jpg 400w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/Turing-Award-winners-300x205.jpg 300w\" sizes=\"auto, (max-width: 400px) 100vw, 400px\" \/><p id=\"caption-attachment-284861\" class=\"wp-caption-text\">Turing Award winners Chuck Thacker (left) and Leslie Lamport convene for a chat recently. Note the rollerblades in the background. Lamport has a penchant for using them to commute to work.<\/p><\/div>\n<p>Lamport, 73, becomes the fifth scientist from Microsoft Research to have won the Turing Award, joining previous recipients Tony Hoare (1980), Lampson, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/gray\/\" target=\"_blank\">Jim Gray<\/a> (1998), and <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/cthacker\/\" target=\"_blank\">Chuck Thacker<\/a> (2009). But despite more than 40 years of nonpareil achievements, Lamport\u2019s self-assessment is not quite so glowing.<\/p>\n<p>\u201cI wasn\u2019t that good at finding solutions,\u201d he states, \u201cbut I was really good at asking questions.\u201d<\/p>\n<p>Few who know him would agree. Take <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"https:\/\/academic.microsoft.com\/#\/detail\/2178361666\" target=\"_blank\">Roy Levin<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, a Microsoft distinguished engineer and managing director of Microsoft Research Silicon Valley, where Lamport now works.<\/p>\n<p>\u201cWhen we started the lab here,\u201d Levin says, \u201cLeslie was one of the early people to join. We knew we were building a distributed-systems lab, and what better than to get the person who is the father of principled distributed computing, which Leslie most certainly is. We were delighted to get him.\u201d<\/p>\n<p>So have been Microsoft\u2019s product groups, which have repeatedly reaped the benefits of Lamport\u2019s expertise. His work on Paxos has been implemented in many products, in uses such as <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"https:\/\/azure.microsoft.com\/en-us\/\" target=\"_blank\">Microsoft Azure<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> storage, Azure\u2019s Rest Availability Proxy, and the Cosmos data storage and query system. He has contributed to the correctness of the Windows Server Transaction Protocol, and the modeling in the Oslo platform for model-driven applications was inspired by his work on Temporal Logic of Actions (<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/research.microsoft.com\/en-us\/um\/people\/lamport\/tla\/tla.html\" target=\"_blank\">TLA<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>). And many at Microsoft have benefited from the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/latex-project.org\/intro.html\" target=\"_blank\">LaTeX<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> document-preparation system, created by Lamport.<\/p>\n<p>But his contributions to Microsoft are not merely measured in bytes, a fact to which David Langworthy can attest.<\/p>\n<p>\u201cLeslie taught me how to think,\u201d says Langworthy, a principal development lead for Microsoft. \u201cUsing simple math that I learned in high school, I found flaws in my programs that would have been next to impossible to debug on a live server\u2014and found them years earlier, when we still had plenty of time to fix them.\u201d<\/p>\n<h2>A Glorious R\u00e9sum\u00e9<\/h2>\n<p>That sort of influence is not surprising. Lamport\u2019s career is littered with glittering honors, making his Turing Award seem merely inevitable. Consider:<\/p>\n<ul>\n<li>Election to the National Academy of Engineering, 1991<\/li>\n<li>Winner of the inaugural Influential Paper Award, for the <em>Time, Clocks<\/em> paper, from the ACM Symposium on Principles of Distributed Computing, 2000.<\/li>\n<li>The IEEE Emanuel R. Piore Award for outstanding contributions in the field of information processing in relation to computer science, 2004.<\/li>\n<li>The Edsger W. Dijkstra Prize in Distributed Computing, 2005.<\/li>\n<li>Three Hall of Fame Awards from the ACM Special Interest Group on Operating Systems. The awards recognize the most influential operating-systems papers published at least 10 years in the past. The award was established in 2005; Lamport won in 2007, 2012, and 2013.<\/li>\n<li>The Test of Time Award from the IEEE Symposium on Logic in Computer Science (LICS), 2008. The award is given annually to the best of the 20-year-old LICS papers that have best met the test of time.<\/li>\n<li>The IEEE John von Neumann Medal, 2008.<\/li>\n<li>Election to the National Academy of Sciences, 2011.<\/li>\n<li>The Jean-Claude Laprie Award in Dependable Computing, 2013.<\/li>\n<\/ul>\n<p>In addition, Lamport, who received his Ph.D. from Brandeis University in 1972, has been bestowed with honorary doctorates from France\u2019s Universit\u00e9 de Rennes in 2003, Germany\u2019s Christian-Albrechts-Universit\u00e4t zu Kiel in 2003, Switzerland\u2019s \u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne in 2004, the Universit\u00e0 della Svizzera italiana in 2006, and France\u2019s Universit\u00e9 Henri Poincar\u00e9 in 2007.<\/p>\n<h2>Time, Clocks, and Relativity<\/h2>\n<p>This eventful legacy, forged in part by Lamport\u2019s puckish sense of humor, began to take shape in 1978, when his massively influential <em>Time, Clocks<\/em> paper was published. Written when Lamport was working for Massachusetts Computer Associates, known as Compass, it resulted from his introduction to a paper called <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.rfc-archive.org\/getrfc.php?rfc=677\" target=\"_blank\"><em>The Maintenance of Duplicate Databases<\/em><span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, by Robert Thomas and Paul Johnson, that argued that keeping identical databases updated when a change is made to one of them requires the use of timestamps.<\/p>\n<p>\u201cI realized,\u201d Lamport recalls, \u201cthat it did not preserve causality. Things would appear in the system as if they were done in an order that was not logically consistent with the order of the events in which the commands were being issued. And I realized this could be corrected fairly easily by changing the way these timestamps were being generated.\u201d<\/p>\n<div id=\"attachment_284864\" style=\"width: 310px\" class=\"wp-caption alignright\"><img loading=\"lazy\" decoding=\"async\" aria-describedby=\"caption-attachment-284864\" class=\"size-full wp-image-284864\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/Lamports-LaTeX-book.jpg\" alt=\"Lamport's LaTeX book\" width=\"300\" height=\"154\" \/><p id=\"caption-attachment-284864\" class=\"wp-caption-text\">Lamport&#8217;s LaTeX book has been translated into multiple languages.<\/p><\/div>\n<p>His insight, stemming from his interest in physics and special relativity, was that it is problematic to identify the temporal order of two events unless there is a causal connection between them\u2014if a message passed between them. That led to an understanding that if the timestamps of such messages could be used to generate an order of events, then all events that occurred in the system could be placed in an order. It then followed that anything that a computing system does could be described with a state machine\u2014something that has a certain state, receives an input, then produces an output and changes its state. This concept, Lamport deduced, could be applied to complex systems, such as banking or airline reservations.<\/p>\n<p>\u201cThe classic paper, of course, is his paper on clocks,\u201d Levin says, \u201cwhich introduced a new way of principled thinking about distributed computation, synchronization, and communication among asynchronous entities that was new at the time and became the basis for any attempt to reason about how parallel systems behave. It\u2019s one of the seminal papers.\u201d<\/p>\n<p>Lamport recalls feedback of a slightly different nature.<\/p>\n<p>\u201cShortly after the <em>Time, Clocks<\/em> paper was published,\u201d Lamport recalls, \u201cJim Gray told me that he had heard two reactions to the paper: Some people thought that it was brilliant, and some people thought that it was trivial.<\/p>\n<p>\u201cI think they\u2019re both right, but I\u2019m disinclined to disagree with people who think it\u2019s brilliant.\u201d<\/p>\n<h2>The Bakery Algorithm<\/h2>\n<p>Another product of Lamport\u2019s Compass years was the bakery algorithm, described in his <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/dl.acm.org\/citation.cfm?id=361093&CFID=834903379&CFTOKEN=38390386\" target=\"_blank\"><em>A New Solution of Dijkstra\u2019s Concurrent Programming Problem<\/em><span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, which aimed to tackle the problem of mutual exclusion: making sure that data corruption doesn\u2019t result from multiple threads trying to write to the same memory location or that one thread doesn\u2019t read that location before another is finished writing to it. The name was an allusion to the ordering system commonly used in a bakery, in which customers select a numbered ticket when they enter.<\/p>\n<div id=\"attachment_284867\" style=\"width: 410px\" class=\"wp-caption alignleft\"><img loading=\"lazy\" decoding=\"async\" aria-describedby=\"caption-attachment-284867\" class=\"size-full wp-image-284867\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/Lamport-at-a-whiteboard.jpg\" alt=\"Lamport at a whiteboard\" width=\"400\" height=\"242\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/Lamport-at-a-whiteboard.jpg 400w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/Lamport-at-a-whiteboard-300x182.jpg 300w\" sizes=\"auto, (max-width: 400px) 100vw, 400px\" \/><p id=\"caption-attachment-284867\" class=\"wp-caption-text\">A common sight over the years: Lamport at a whiteboard.<\/p><\/div>\n<p>\u201cWhen I was at Compass, I read a paper in <em>Communications of the ACM<\/em> about a mutual-exclusion algorithm,\u201d Lamport recalls. \u201cIt was the first time I had seen the mutual-exclusion problem, and I looked at it and said, \u2018Well, that doesn\u2019t seem very difficult.\u2019\u201d<\/p>\n<p>So he wrote a quick algorithm and a brief paper and sent them to the editor, who promptly responded by explaining why Lamport\u2019s algorithm wouldn\u2019t work.<\/p>\n<p>\u201cThat taught me a lesson,\u201d he now says, \u201cthat I should not write a concurrent algorithm without having a proof of its correctness.\u201d<\/p>\n<p>It also encouraged him to go back and fully solve the problem, and he remains proud today of what he achieved with the bakery algorithm.<\/p>\n<p>\u201cThat,\u201d he says, \u201cis the one algorithm that I have the feeling that I discovered, rather than invented.\u201d<\/p>\n<h2>Byzantine Generals<\/h2>\n<p>In 1972, Lamport moved to the Bay Area as the vanguard of what Compass planned to be a West Coast outpost, but that office never materialized, and for five years, he was the only Compass employee based in California. Finally, he was asked to return to the East Coast. Instead, he decided to join SRI International, founded as the Stanford Research Institute.<\/p>\n<p>SRI had a project to build a fault-tolerant avionics computer system for NASA. Given the nature of the system, failures had to be avoidable, and that led to a pair of papers, co-written by Lamport and SRI colleagues Marshall Pease and Robert Shostak, to address Byzantine failures.<\/p>\n<p>In computing terms, \u201cordinary\u201d failures might result in lost messages or halted processes, but they don\u2019t get corrupted\u2014and if they do, the use of redundancy enables the corrupted message to be discarded. Processes might stop, but they don\u2019t give an incorrect answer.<\/p>\n<p>Byzantine failures, though, can make mistakes or send incorrect messages.<\/p>\n<p>The commonly used technique, called triple modular redundancy, uses three separate computers to \u201cvote,\u201d in a sort of majority rule, and even if one delivers an incorrect result, the other two still will provide the right answer. To prove that this worked, though, a proof was needed, and in trying to write a proof, the researchers encountered a problem: The \u201cwrong\u201d computer could send a different, incorrect value to each of the other two, and neither of those would know. That would necessitate the use of four computers to tackle one fault.<\/p>\n<p>\u201cExcept if you use digital signatures,\u201d Lamport says. \u201cThen you can do it with three, because if the bad computer sends one incorrect value with a signature to one computer and a different incorrect value with a signature to the other, the other two computers will exchange the messages and see what\u2019s happening, because two different values have been sent and signed.\u201d<\/p>\n<p>Lamport had heard Gray talk about another problem of the same general nature called the Chinese Generals Problem. That got Lamport to thinking about generals giving orders and generals being traitors, and he dubbed the problem and its solution with the name <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/dl.acm.org\/citation.cfm?id=357176&CFID=834903379&CFTOKEN=38390386\" target=\"_blank\"><em>The Byzantine Generals Problem<\/em><span class=\"sr-only\"> (opens in new tab)<\/span><\/a>.<\/p>\n<p>\u201cI remember sitting at a caf\u00e9 in Berkeley with Whit Diffie, a friend of mine, when he described the problem of constructing a digital signature,\u201d Lamport recalls. \u201cHe said, \u2018This would be really useful if people could do it.\u2019 I said, \u2018That doesn\u2019t sound very difficult,\u2019 and, on a napkin, I sketched to him what was the first digital-signature algorithm. It wasn\u2019t very practical at the time, although these days, it turns out that it is feasible.\u201d<\/p>\n<p>That napkin, alas, has been lost to the sands of time.<\/p>\n<h2>Greek Comedy<\/h2>\n<p>\u201cLeslie\u2019s schemes for dealing with faults was a major area of investigation in distributed computing,\u201d Levin says. \u201cHis work was fundamental there. Then it led to work on agreement protocols, a key part of the notion of getting processes to converge on a common answer. This is what has come to be known as Paxos.\u201d<\/p>\n<p>Incidently, that work was independently invented at about the same time by Barbara Liskov, Turing Award winner in 2008, and her student Brian Oki.<\/p>\n<p>\u201cLamport\u2019s paper [<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/lamport-paxos.pdf\" target=\"_blank\"><em>The Part-Time Parliament<\/em><\/a>],\u201d Levin adds, \u201cexplained things through the use of a mythical Greek island and its legislative body. Partly because he chose this metaphor, it was not appreciated for quite some time what was really going on there.\u201d<\/p>\n<p>Lamport has a less diplomatic assessment.<\/p>\n<p>\u201cWith the success of Byzantine Generals, I thought, \u2018We need a story.\u2019 I created a story, and that was an utter disaster.<\/p>\n<p>\u201cIt was also an attempt to add some humor. It\u2019s the same problem: implementing a state machine to handle the presence of failures. The state machine, in this case, was a parliament passing a series of laws. What\u2019s different is this was not for handling Byzantine faults, but for handling ordinary, simple failures, but in an asynchronous setting. You weren\u2019t dealing with malicious failures. Some things were simple engineering problems, so instead of bothering to go into that, I would simply say, \u2018The archeological records don\u2019t say exactly how they did this.\u2019 In another case, to illustrate how a particular optimization could be done, I used the story of a cheese merchant, illustrating how you could make it more efficient. In all the stories, I gave the characters in them Greek names, written in a pseudo-Greek, using transliterated names of computer scientists. The cheese merchant was a computer scientist named Gouda [for Mohamed Gouda].\u201d<\/p>\n<div id=\"attachment_284870\" style=\"width: 310px\" class=\"wp-caption alignright\"><img loading=\"lazy\" decoding=\"async\" aria-describedby=\"caption-attachment-284870\" class=\"size-full wp-image-284870\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/Universit\u00e0-della-Svizzera-italiana.jpg\" alt=\"students from Universit\u00e0 della Svizzera italiana\" width=\"300\" height=\"244\" \/><p id=\"caption-attachment-284870\" class=\"wp-caption-text\">Lamport (left) and his wife (second from right) with students from the Universit\u00e0 della Svizzera italiana in 2006.<\/p><\/div>\n<p>It also gave Lamport a chance to have a joke at the expense of one of his buddies at Digital Equipment Corp. (DEC), at whose Systems Research Center Lamport worked from 1985 until joining Microsoft Research in 2001.<\/p>\n<p>\u201cThe ending of the paper was that there was something that could happen to cause the system to crash, just completely disintegrate. You could use the system to reconfigure itself, but if you did it carelessly, you could run into a situation where no more laws could be passed. So in the story, this is what happened, and a general named Lampson took over power and became dictator.<\/p>\n<p>\u201cIt turned out that computer scientists weren\u2019t as familiar with the Greek alphabet as mathematicians. \u2026 Butler Lampson was the only person who got it and understood that it was about how to build distributed systems.\u201d<\/p>\n<p>The paper eventually was published\u2014a decade later, updated to account for intervening advancements. Lamport later wrote <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/paxos-simple.pdf\" target=\"_blank\"><em>Paxos Made Simple<\/em><\/a> to explain the simplicity of the algorithm\u2014without employing Greek wordplay. Over time, the work has become known as a true advance.<\/p>\n<p>\u201cPaxos has become a primary piece of technology in modern distributed systems,\u201d Levin says. \u201cNo one would think of building a large-scale distributed system that has to be robust and reliable without having Paxos or something very similar to it at the core.\u201d<\/p>\n<h2>Abstracted Correctness<\/h2>\n<p>Lamport also introduced the properties of safety and liveness as the best ways to generalize about partial correctness and termination in concurrent systems. \u201cSafety\u201d means that nothing bad happens in a system, \u201cliveness\u201d that something good happens.<\/p>\n<p>\u201cI believed that all you needed was safety and liveness,\u201d Lamport says. \u201cAbout a decade later, Fred Schneider and his student Bowen Alpern formally defined these concepts and proved that my hunch was correct.<\/p>\n<p>\u201cShortly after I introduced the concepts of safety and liveness, Amir Pnueli [Turing Award winner in 1996] showed how to use temporal logic to reason about programs. You could represent the program and its properties in the same logic. Proving correctness simply became a matter of saying that a program logically implied its specification.\u201d<\/p>\n<p>Lamport and Susan Owicki showed that temporal logic was good for reasoning about liveness. But the idea of representing the program in temporal logic didn\u2019t work.<\/p>\n<p>\u201cIt was a wonderful idea,\u201d Lamport says, \u201cbut it just didn\u2019t work in practice.\u201d<\/p>\n<p>Some thought the solution was to add more complicated temporal-logic operators, but Lamport took a different direction.<\/p>\n<p>\u201cThe original logic Amir Pneuli used had one temporal operator: always,\u201d Lamport says. \u201cSomething\u2019s always true. People added different, complicated temporal operators, such as \u2018until something is true,\u2019 \u2018until something else is true.\u2019\u201d<\/p>\n<p>Things got unwieldy, and they weren\u2019t easy to understand.<\/p>\n<div id=\"attachment_284873\" style=\"width: 260px\" class=\"wp-caption alignleft\"><img loading=\"lazy\" decoding=\"async\" aria-describedby=\"caption-attachment-284873\" class=\"size-full wp-image-284873\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/Specifying-Systems.jpg\" alt=\"Specifying Systems\" width=\"250\" height=\"313\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/Specifying-Systems.jpg 250w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/Specifying-Systems-240x300.jpg 240w\" sizes=\"auto, (max-width: 250px) 100vw, 250px\" \/><p id=\"caption-attachment-284873\" class=\"wp-caption-text\">The front cover of Lamport&#8217;s book Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers.<\/p><\/div>\n<p>\u201cI had the brilliant idea of sticking to that one temporal operator but changing the basic non-temporal formulas to which that operator was applied,\u201d he says. \u201cInstead of using basic formulas that just talked about one state, I added formulas that talk about a pair of states, a current state and a next state. By adding those formulas that talked about two states, I was able to describe a state machine in this logic. If I could describe the state machine in the logic and I could describe the liveness properties as temporal formulas, then I could describe the entire program or the entire specification as a single formula, one that really worked. That was TLA.\u201d<\/p>\n<p>TLA underlies the TLA+ specification language, the PlusCal algorithm, and the tools associated with them. TLA and TLA+ are explained in a book written by Lamport and published in 2002: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/research.microsoft.com\/en-us\/um\/people\/lamport\/tla\/book.html\" target=\"_blank\"><em>Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers<\/em><span class=\"sr-only\"> (opens in new tab)<\/span><\/a>. The basic tenet is that the best way to describe things formally is with simple mathematics, with the corollary that a specification language should contain as little as possible beyond what is needed to write simple mathematics precisely.<\/p>\n<h2>From DEC to Microsoft<\/h2>\n<p>During Lamport\u2019s time at DEC, he had the opportunity of working with other giants of the computing industry\u2014many of whom had worked at Xerox\u2019s legendary Palo Alto Research Center. Among Lamport\u2019s DEC colleagues were Levin, Thacker, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/luca\/\" target=\"_blank\">Luca Cardelli<\/a>, Gray, and Lampson, all of whom eventually found their way to Microsoft after DEC\u2019s research labs withered following the sale of the company to Compaq. Lamport retains a particular fondness for his manager at DEC, <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/en.wikipedia.org\/wiki\/Robert_Taylor_(computer_scientist)\" target=\"_blank\">Bob Taylor<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>.<\/p>\n<div id=\"attachment_284876\" style=\"width: 410px\" class=\"wp-caption alignright\"><img loading=\"lazy\" decoding=\"async\" aria-describedby=\"caption-attachment-284876\" class=\"size-full wp-image-284876\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/Bob-Taylor-and-Roy-Levin.jpg\" alt=\"Bob Taylor and Roy Levin\" width=\"400\" height=\"316\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/Bob-Taylor-and-Roy-Levin.jpg 400w, https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2014\/03\/Bob-Taylor-and-Roy-Levin-300x237.jpg 300w\" sizes=\"auto, (max-width: 400px) 100vw, 400px\" \/><p id=\"caption-attachment-284876\" class=\"wp-caption-text\">Leslie Lamport has worked for two managers over the past 30 years: Bob Taylor (left) and Roy Levin.<\/p><\/div>\n<p>\u201cThe thing I think is so remarkable about Bob is his lack of ego,\u201d Lamport says. \u201cThis is something that he taught to Roy Levin, that it was his job to make us happy and productive. He was working for us; we weren\u2019t working for him, in a sense.<\/p>\n<p>\u201cIn the 10 years I worked for Bob, his door was always open, and I would quite often wander in there and chat with him. There was one time during that period when he said: \u2018Can you come back later? I\u2019m busy now.\u2019 I remember that because it was so extraordinary.\u201d<\/p>\n<p>But nothing in Lamport\u2019s storied career prepared him for what he encountered when he joined Microsoft.<\/p>\n<p>\u201cThe whole corporate attitude toward research was just so completely different at Microsoft than anyplace else,\u201d he says. \u201cMicrosoft realizes that it\u2019s the researchers who have to generate the research ideas.<\/p>\n<p>\u201cWhat the corporation can do is to provide the communication channels between the researchers and the engineers, so the engineers will know what the researchers are doing and the researchers will know what the engineers\u2019 problems are. Microsoft has set up its program-manager system as a mechanism to do that.\u201d<\/p>\n<p>And Lamport, who in recent years has been collaborating with the scientists at the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.msr-inria.inria.fr\/\" target=\"_blank\">Microsoft Research-Inria Joint Centre<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, certainly has the perspective to appreciate Microsoft\u2019s research approach.<\/p>\n<p>\u201cI like working in an industrial research lab, because of the input,\u201d he says. \u201c[French film director] Jean Renoir wrote in his autobiography that when someone asked his father, [Impressionist painter] Pierre-Auguste, why he painted from life, taking his easel outdoors rather than painting in a studio, he said: \u2018If I were to paint a tree in the studio, I would be able to paint five or six different kinds of leaves. That\u2019s all that would come to me. But when I go out in nature, there are millions of different kinds of leaves. I need nature for that inspiration.\u2019<\/p>\n<p>\u201cIt\u2019s the same with me. If I just work by myself and come up with problems, I\u2019d come up with some small number of things, but if I go out into the world, where people are working on real computer systems, there are a million problems out there. When I look back on most of the things I worked on\u2014Byzantine Generals, Paxos\u2014they came from real-world problems.\u201d<\/p>\n<p>On February 13, Lamport again found himself in the real world, delivering a tribute to close LampsonFest, an event held at Microsoft Research New England to celebrate the 70th birthday of another computing legend, Lamport\u2019s colleague and friend, Butler Lampson.<\/p>\n<p>At the outset of his talk, Lamport displayed a slide with a photo of himself, followed by one of Lampson.<\/p>\n<p>\u201cThis is me,\u201d Lamport said, \u201cand this is Butler.<\/p>\n<p>\u201cI realized that there was some confusion about this when someone sent me email asking about my Turing Award lecture. So you should learn to distinguish us. I\u2019m the one with the beard. Butler\u2019s the one with the Turing Award.\u201d<\/p>\n<p>Savor the joke. We won\u2019t be hearing that one anymore.<\/p>\n<p><strong>Learn more<\/strong><\/p>\n<ul>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/video\/turing-award-winner-leslie-lamport\/\">Turing Award winner Leslie Lamport<\/a> (video)<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Leslie Lamport first began dabbling in computers while he was still in high school. Nothing too unusual about that\u2014until you consider that this was in the mid-1950s. Lamport was attending the Bronx High School of Science in New York, and he and a friend used to scrounge around, looking for discarded vacuum tubes to build [&hellip;]<\/p>\n","protected":false},"author":39507,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr-author-ordering":[],"msr_hide_image_in_river":0,"footnotes":""},"categories":[194466,194475,194477],"tags":[194534,210983,212045,186604,212048,212051,187230,196219,212054,212042],"research-area":[13561,13547],"msr-region":[],"msr-event-type":[],"msr-locale":[268875],"msr-post-option":[],"msr-impact-theme":[],"msr-promo-type":[],"msr-podcast-series":[],"class_list":["post-284843","post","type-post","status-publish","format-standard","hentry","category-algorithms","category-database-data-analytics-platforms","category-distributed-systems","tag-a-m-turing-award","tag-association-for-computing-machinery-acm","tag-bakery-algorithm","tag-bing","tag-byzantine-failures","tag-chinese-generals-problem","tag-computer-science","tag-leslie-lamport","tag-temporal-logic-of-actions-tla","tag-theory-of-distributed-computing","msr-research-area-algorithms","msr-research-area-systems-and-networking","msr-locale-en_us"],"msr_event_details":{"start":"","end":"","location":""},"podcast_url":"","podcast_episode":"","msr_research_lab":[199563],"msr_impact_theme":[],"related-publications":[],"related-downloads":[],"related-videos":[],"related-academic-programs":[],"related-groups":[],"related-projects":[],"related-events":[],"related-researchers":[],"msr_type":"Post","byline":"","formattedDate":"March 18, 2014","formattedExcerpt":"Leslie Lamport first began dabbling in computers while he was still in high school. Nothing too unusual about that\u2014until you consider that this was in the mid-1950s. Lamport was attending the Bronx High School of Science in New York, and he and a friend used&hellip;","locale":{"slug":"en_us","name":"English","native":"","english":"English"},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/284843","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/users\/39507"}],"replies":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/comments?post=284843"}],"version-history":[{"count":16,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/284843\/revisions"}],"predecessor-version":[{"id":290024,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/284843\/revisions\/290024"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=284843"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/categories?post=284843"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/tags?post=284843"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=284843"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=284843"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=284843"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=284843"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=284843"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=284843"},{"taxonomy":"msr-promo-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-promo-type?post=284843"},{"taxonomy":"msr-podcast-series","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-podcast-series?post=284843"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}