微軟科學(xué)家Leslie Lamport榮獲2013年圖靈獎 

編者按：Leslie Lamport，新晉圖靈獎得主，一個在計算機領(lǐng)域擁有輝煌成就的大師，他關(guān)于時間時鐘、面包店算法、拜占庭將軍等問題的思考令人乍舌。親近他的人還會告訴你，他是個年愈古稀仍愛穿旱冰鞋上下班的幽默老頭。全球無數(shù)人受益于他的成就，卻很少聽說他的名字。

Leslie Lamport在讀高中時就已經(jīng)開始涉足計算機科學(xué)。這乍一聽沒有什么了不起——但你要知道，那是20世紀(jì)50年代中期。當(dāng)時Lamport正在就讀紐約布朗士科學(xué)高中，他和一個朋友四處撿破爛，搜尋廢棄真空管來搭建數(shù)字電路。

雖說“科學(xué)要從娃娃抓起”，但對于微軟研究院首席研究員Lamport來說，青少年時代的好奇心至今也仍未泯滅。在隨后的幾十年間，他逐漸成為計算機學(xué)界名副其實的傳奇人物。他的分布式計算理論奠定了這門學(xué)科的基礎(chǔ)。他在1978年發(fā)表的論文《分布式系統(tǒng)內(nèi)的時間、時鐘事件順序（Time, Clocks, and the Ordering of Events in a Distributed System）》成為計算機科學(xué)史上被引用最多的文獻。他為“并發(fā)系統(tǒng)的規(guī)范與驗證”研究貢獻了核心原理。

3月18日，為表彰Lamport為這些寶貴的進步所作出的杰出貢獻，美國計算機協(xié)會（ACM）將2013年度圖靈獎頒發(fā)給了他，這一殊榮被廣泛看作計算學(xué)界的諾貝爾獎。

在許多人心目中，沒有人比他更有資格獲得這個獎項：

Bill Gates

“作為一名偉大的科學(xué)家，這項榮譽他當(dāng)之無愧。作為一名帶頭人，他界定了分布式計算的許多關(guān)鍵概念，并讓今天執(zhí)行關(guān)鍵任務(wù)的計算機系統(tǒng)成為可能，萊斯利的偉大不僅局限于計算機科學(xué)領(lǐng)域，而且還體現(xiàn)在努力讓世界變得更加安全。世界各地?zé)o數(shù)人受益于他的工作，卻從未聽說過他的名字。在我看來，這個獎項也是對微軟研究院非凡工作的認可，這里已經(jīng)成為立志克服業(yè)內(nèi)最難挑戰(zhàn)的科學(xué)家和工程師們的理想家園。當(dāng)我們鼓勵全球最強大腦都來超越未知的可能時會發(fā)生什么？Lamport就是一個很好的例子。”

微軟新英格蘭研究院技術(shù)院士、1992年圖靈獎得主Butler Lampson

“Lamport對并發(fā)系統(tǒng)理論和實踐在質(zhì)量、范圍和重要性上的貢獻都是難以超越的。它們完全可以和Dijkstra、Hoare、Milner和Pneuli等所有前輩圖靈獎得主的成就相提并論。雖然他能像這些前輩一樣做好理論研究，，但他最大的優(yōu)點是作為一名應(yīng)用數(shù)學(xué)家，十分了解如何利用數(shù)學(xué)工具來解決具有非凡現(xiàn)實意義的問題。”

微軟公司技術(shù)和研究執(zhí)行副總裁沈向洋

“我到必應(yīng)團隊工作時，才開始真正意識到他對我們所處行業(yè)，尤其是對云計算和分布式系統(tǒng)所做出的令人難以置信的貢獻。在必應(yīng)團隊，我們研究了他有關(guān)Paxos的論文，并應(yīng)用他的技術(shù)構(gòu)建了分布式系統(tǒng)，直至今天我們?nèi)栽谑褂谩?rdquo;

麻省理工學(xué)院計算機科學(xué)和人工智能實驗室分布式系統(tǒng)理論研究組負責(zé)人Nancy Lynch

“欣聞Lamport榮膺今年的圖靈獎。其實，我覺得這個獎項已經(jīng)姍姍來遲了。他從20世紀(jì)70年代起就對分布式計算領(lǐng)域做出了許多基礎(chǔ)性貢獻。”

華盛頓大學(xué)計算機科學(xué)與工程系教授Ed Lazowska

“談及Lamport的影響，我首先想到的是他所設(shè)計的算法，當(dāng)時從許多角度上看，它只是一種理論興趣，而現(xiàn)在它已經(jīng)成為我們Web規(guī)模系統(tǒng)構(gòu)建方法的基石——也就是我們所有人每天都在使用的系統(tǒng)。如果沒有萊斯利的創(chuàng)新，就不會有我們今天所使用的計算環(huán)境。”

施樂帕洛阿爾托研究中心創(chuàng)始人兼經(jīng)理，以及此后的數(shù)字設(shè)備公司系統(tǒng)研究中心創(chuàng)始人兼經(jīng)理Bob Taylor

“互聯(lián)網(wǎng)建立在分布式系統(tǒng)技術(shù)的基礎(chǔ)知識之上，而后者又建立在萊斯利所發(fā)明的理論基礎(chǔ)之上。所以，如果你喜歡使用互聯(lián)網(wǎng)，那么你就該感謝萊斯利。”

 

圖靈獎得主Chuck Thacker（左）和Leslie Lamport最近小聚。

請注意在背景中的旱冰鞋。Lamport現(xiàn)在仍喜歡使用它作為上下班的交通工具。

Lamport現(xiàn)年73歲，他成為微軟研究院第五位榮獲圖靈獎的科學(xué)家，此前的獲獎?wù)哌€有Tony Hoare（1980年）、Butler Lampson（1992年）、Jim Gray（1998年）和Chuck Thacker（2009年）。盡管坐擁40多年的絕倫成就，Lamport的自我評價卻不是那么光輝奪目。

“我并不太善于尋找解決方案，”他說：“但我確實很善于提出問題。”

在了解他的人中，很少有人會同意這個說法。微軟硅谷研究院的微軟杰出工程師兼院長Roy Levin就是其中之一——Lamport目前就在那里工作。

“我們開始籌備實驗室時，”Levin說：“Lamport就是最早加入的人之一。我們知道自己正在建立一個分布式系統(tǒng)實驗室，還有什么比請到分布式計算原理之父更好的事情呢——而且Lamport最有資格。我們很高興能夠與他共事。”

微軟的產(chǎn)品組也不例外——他們曾多次獲益于Lamport的專業(yè)知識。他的Paxos研究成果已經(jīng)在多個產(chǎn)品中使用，其中包括Windows Azure存儲、Azure的REST可用性代理（Rest Availability Proxy）和Cosmos數(shù)據(jù)存儲及查詢系統(tǒng)。他還對Windows服務(wù)器會話協(xié)議（Transaction Protocol）的正確性做出了貢獻，而且針對模型驅(qū)動應(yīng)用的奧斯陸平臺（Oslo platform）的構(gòu)筑靈感也來自于他在動作時序邏輯（TLA）的研究。此外，微軟公司的許多工作人員都曾受益于Lamport一手創(chuàng)建的LaTeX系統(tǒng)。

Lamport對微軟的貢獻是無法度量的，關(guān)于這一點， David Langworthy能夠證明。

“Lamport教會了我如何思考，”作為微軟首席開發(fā)主管之一的Langworthy說：“使用在高中時學(xué)到的簡單數(shù)學(xué)，我竟然從自己的程序中發(fā)現(xiàn)了一旦用于在線服務(wù)器后就幾乎不可能調(diào)試的缺陷——幸好提前幾年就發(fā)現(xiàn)，給我們留出足夠的時間來解決這些問題。”

輝煌履歷

那樣的影響力并不足為奇。Lamport的職業(yè)生涯充滿了眾多令人咋舌的榮譽，讓他榮獲圖靈獎這件事顯得“順理成章”。

·1991年入選美國國家工程院院士。

·2000年憑借《時間、時鐘》論文獲得ACM分布式計算原理研討會首屆有影響力論文獎。

·2004年憑借與計算機科學(xué)有關(guān)的信息處理領(lǐng)域突出貢獻榮獲IEEE Emanuel R. Piore 獎。

·2005年榮獲Edsger W. Dijkstra分布式計算獎。

·三次獲得ACM SIGOPS榮譽大獎。該獎項旨在表彰發(fā)表至少10年、在操作系統(tǒng)領(lǐng)域最有影響力的論文。該獎項成立于2005年，而Lamport曾分別于2007年、2012年和2013年贏得這一殊榮。

·2008年榮獲IEEE計算機科學(xué)邏輯研討會（LICS）最經(jīng)得起時間考驗獎。該獎項每年頒發(fā)一次，旨在表彰20年以前發(fā)表并經(jīng)得住時間考驗的LICS論文。

·2008年榮獲IEEE約翰·馮·諾依曼獎?wù)隆?/p>

·2011年當(dāng)選美國國家科學(xué)院院士。

·2013年榮獲Jean-Claude Laprie可信計算獎。

出版物

·《時間、時鐘和分布式系統(tǒng)中的事件排序》

·《復(fù)制數(shù)據(jù)庫的維護》

·《Dijkstra并行編程問題新解》

·《拜占庭將軍問題》

·《兼職議會》

·《Paxos化繁為簡》

·《規(guī)范系統(tǒng)：硬件和軟件工程師的TLA+語言及工具》

Lamport于1972年獲得布蘭迪斯大學(xué)博士學(xué)位，2003年獲得法國德雷恩大學(xué)榮譽博士學(xué)位，2003年獲得德國基爾大學(xué)榮譽博士學(xué)位，2004年獲得瑞士洛桑聯(lián)邦高等理工學(xué)院榮譽博士學(xué)位，2006年獲得瑞士提契諾大學(xué)榮譽博士學(xué)位，2007年獲得法國亨利·龐加萊大學(xué)榮譽博士學(xué)位。

時間、時鐘和相對論

這項重要的成果，最早發(fā)端于1978年他廣有影響力的《時間、時鐘》論文的發(fā)表，在一定程度上要歸功于Lamport惡作劇式的幽默感。當(dāng)時，Lamport正在馬薩諸塞州計算機合伙人公司（又名Compass）任職，他為 Robert Thomas和Paul Johnson共同撰寫的論文《復(fù)制數(shù)據(jù)庫的維護（The Maintenance of Duplicate Databases）》作序。這篇論文認為，對于兩個完全相同的數(shù)據(jù)庫，如果其中之一發(fā)生改變，那么對它們更新時需要用到時間戳。

   

Lamport榮獲2013年圖靈獎

   Lamport的《LaTeX》一書已被翻譯成多種語言。

“我意識到，”Lamport回憶說：“它沒有保留因果關(guān)系。事件按照完成時間的順序出現(xiàn)在系統(tǒng)中，但其在邏輯上并不與命令發(fā)出的順序相一致。我意識到，如果改變時間戳的產(chǎn)生方法，這個問題可能會很容易得到糾正。”

他的洞察力源自對物理學(xué)和狹義相對論的興趣。他意識到，確定兩個事件時間順序的工作存在問題，除非兩者之間有因果聯(lián)系——也就是說，除非它們之間傳遞過信息。他由此認識到，如果這種訊息的時間戳可以用來確定事件的順序，則該系統(tǒng)中發(fā)生的所有事件都可以按單一順序排列。推而廣之，一個計算系統(tǒng)內(nèi)的任何事物都可以用狀態(tài)機加以描述（狀態(tài)機保持著特定狀態(tài)，接收輸入后產(chǎn)生一個輸出，同時改變其自身的狀態(tài)。Lamport推論，這個概念可以適用于更加復(fù)雜的系統(tǒng)，如銀行或航空票務(wù)預(yù)訂。

“最經(jīng)典的當(dāng)數(shù)他有關(guān)時鐘的論文，”Levin說：“里面介紹了有關(guān)分布式計算、同步和異步實體（asynchronous entities）之間溝通的原理思維新途徑，它在當(dāng)時令人耳目一新，后來成為各種并發(fā)系統(tǒng)行為推理的基礎(chǔ)。它是一篇開山之作。”

在Lamport的回憶中，所收到的反饋在性質(zhì)上略有不同。

“《時間、時鐘》論文發(fā)表后不久，”Lamport回憶道：“Jim Gray告訴我，他曾聽到對這篇文章的兩種反應(yīng)：有些人認為它很有見地，也有人認為它微不足道。

“我認為他們可能都是對的，但我不愿意否定那些夸我的人。”

面包店算法

Lamport在Compass工作期間的另一個成果是面包店算法，見于《Dijkstra并行編程問題新解》一文，旨在解決互斥問題：排除多個線程試圖對相同存儲位置寫入時發(fā)生數(shù)據(jù)損壞的現(xiàn)象，以及一個線程完成對特定位置寫入之前另一個線程無法讀取該位置的現(xiàn)象。其名稱暗指到面包店常用的排序系統(tǒng)：客戶在進入店面時需要選擇一張有編號的票。

“我還在Compass工作時，在《ACM通訊》上讀到一篇關(guān)于互斥算法的論文，”Lamport回憶道。“這是我第一次接觸互斥問題，我看了文章，覺得這似乎并不十分困難。”

于是，他撰寫了一個快速算法和簡短論文，并將它們寄給刊物編輯，后者立即回復(fù)并解釋了為什么Lamport的算法行不通。

“這給了我一個教訓(xùn)，”他回憶道：“我不應(yīng)該編寫并行算法而不驗證其正確性。”

這件事激勵他回過頭去，徹底解決這個問題，時至今日，他仍然對自己在面包店算法上的成就感到自豪。

他說：“我感覺自己發(fā)現(xiàn)了一種算法，而不是發(fā)明了它。”

拜占庭將軍

1972年，Lamport搬到灣區(qū)，充當(dāng)Compass西海岸計劃前哨基地的先鋒，但這個分支機構(gòu)最終未能落實。另外，在長達五年的時間內(nèi)，他曾是Compass總部派駐加州的唯一員工。最后，他收到撤回東海岸的指令。但是，他決定加入斯坦福國際研究院（SRI），其前身是斯坦福研究所。

SRI有一個項目，旨在美國航空航天局建立容錯型航電計算機系統(tǒng)（fault-tolerant avionics computer system）。考慮到系統(tǒng)的工作性質(zhì)，故障是不允許發(fā)生的。這段經(jīng)歷孕育了兩篇旨在解決拜占庭故障的論文，由Lamport和SRI同事Marshall Pease 及Robert Shostak合作完成。

用計算學(xué)術(shù)語說，“普通”故障可能會導(dǎo)致信息丟失或過程停止，但它們不會遭到損壞——即便如此，也能通過冗余的使用來丟棄損壞的訊息。過程可能會停止，但它們不會給出錯誤答案。

然而，拜占庭故障卻可能犯錯誤，或給出錯誤訊息。

當(dāng)時常用的技術(shù)被稱為“三重模塊冗余（ triple modular redundancy）”，使用三個獨立的計算機按照某種少數(shù)服從多數(shù)的原則“投票”，即使其中一臺機器提供了錯誤結(jié)果，其他兩臺仍然會提供正確答案。但是為了證明其有效，必須拿出證據(jù)，而在編寫證據(jù)過程中，研究人員遇到了一個問題：“錯誤”計算機可能給其他兩臺機器發(fā)送互不相同的錯誤值，而后者卻不會知道。這就需要使用第四臺計算機來應(yīng)對這個故障。

“如果你使用數(shù)字簽名，”Lamport說：“就可以用三臺機器達成目的，因為如果‘壞’計算機向一臺計算機發(fā)送了帶簽名的錯誤值，并向另一臺發(fā)送了不同的帶簽名錯誤值，另外兩臺計算機就能夠交換消息，以檢查究竟發(fā)生了什么情況，因為兩個不同的值都是簽名發(fā)送的。”

Lamport還聽Jim Gray談?wù)撨^另一個性質(zhì)大體相同的問題，人們稱之為“中國將軍問題”。這引起了Lamport有關(guān)司令將軍和叛徒將軍的聯(lián)想，于是他將這個問題及其解決方案命名為“拜占庭將軍問題”。

“我記得，與我的朋友Whit Diffie坐在伯克利的一間咖啡館里，當(dāng)時他描述了一個構(gòu)建數(shù)字簽名的問題，”Lamport回憶說：“他說：‘如果能辦到的話，會非常有用。’我說：‘這聽起來并不很困難，’于是在一張餐巾紙上，我為他勾畫出了第一種數(shù)字簽名算法。雖然當(dāng)時并不很實用，但目前已經(jīng)變得切實可行。”

只可惜那張餐巾紙已經(jīng)消逝在時間的流沙中。

希臘喜劇

“Lamport應(yīng)對故障的計劃是分布式計算研究的一個重要領(lǐng)域，”Levin說：“他的工作是基礎(chǔ)性的。后來，又延伸至約定協(xié)議的工作，這是‘讓過程收斂于一個共同答案’這個概念的關(guān)鍵部分之一。它就是人們后來所說的Paxos算法。”

無獨有偶，2008年圖靈獎獲得者Barbara Liskov和她的學(xué)生布Brian Oki也獨立發(fā)明了這項技術(shù)。

Levin補充說：“Lamport的論文《The Part-Time Parliament》通過希臘神話中一個島嶼及其立法機構(gòu)的類比來加以解釋。或許在一定程度上由于他所選擇的這個比喻，這篇論文的實際內(nèi)容在相當(dāng)長一段時間沒有得到重視。

對此，Lamport有一個不太注重外交辭令的評價。

“隨著拜占庭將軍問題的成功，我覺得我們需要一個故事來加以說明。我杜撰了一個故事，而那是一次徹底的災(zāi)難。“

“我嘗試添加一些幽默氣氛。還是老問題：借助狀態(tài)機（state machine）來處理存在的故障。在這種情況下，狀態(tài)機像是需要通過一系列法律的議會。所不同的是，我們的目的不是處理拜占庭故障，而是處理普通、簡單的故障，只不過在異步環(huán)境下進行。我們并非處理惡意失敗。有些是單純的工程問題，所以我懶得去探究，就簡單地說：‘考古記錄并未說明他們究竟如何做到這一點的。’在另一個案例中，為了說明如何進行特定優(yōu)化，我引用了一個奶酪 商人的故事，說明如何可以使之更有效率。在所有的故事中，我都給人物取了希臘人的名字，以偽希臘語寫作，并借用計算機科學(xué)家的音譯姓名。案例中的奶酪商人名為Gouda ，實際上是一位計算機科學(xué)家Mohamed Gouda。”

 

2006年，Lamport（左）和他的妻子（右二）與來自瑞士提契諾大學(xué)的學(xué)生合影。

Lamport也因此有機會調(diào)侃數(shù)字設(shè)備公司（DEC）的一位好友，Lamport自1985年起就在該公司的系統(tǒng)研究中心工作，一直到2001年加入微軟研究院。

“論文的結(jié)論是，可能會發(fā)生一些導(dǎo)致系統(tǒng)崩潰——也就是完全瓦解的事件。你可以利用系統(tǒng)來重新自我配置，但是如果你稍有疏忽，就可能會遇到一種情況：議會無法再通過更多的法律。在故事中恰恰發(fā)生了這種情況，而一個名叫Lampson的將軍便接管政權(quán)，成為獨裁者。

“原來，計算機科學(xué)家們并不像數(shù)學(xué)家那樣熟悉希臘字母。Butler Lampson是唯一讀懂了故事的人，并意識到這是一篇討論如何構(gòu)建分布式系統(tǒng)的論文。”

論文最終發(fā)表，但已經(jīng)是十年之后的事情，而且經(jīng)過增補，納入了對干預(yù)方法進步的思考。Lamport后來寫了一篇題為《Paxos Made Simple》的文章來解釋算法的簡潔性——而且沒有借用希臘文字游戲。隨著時間的推移，人們逐漸認識到這項工作是一個真正的進步。

“Paxos算法已經(jīng)成為現(xiàn)代分布式系統(tǒng)中的一項重要技術(shù)，”Levin說：“如果沒有Paxos或非常類似的技術(shù)為核心，就不會有人想著去建立一個魯棒、可靠的大型分布式系統(tǒng)。”

抽象的正確性

Lamport還引入了安全和活躍度這兩種屬性，并作為對并發(fā)系統(tǒng)的部分正確性和終止加以推廣的最佳途徑。“安全”是指一個系統(tǒng)中沒有發(fā)生任何不好的事情，而“活躍度”則是指有好事發(fā)生。

“我認為，你所需要的就是安全和活躍度，”Lamport說。“大約十年后，F(xiàn)red Schneide和他的學(xué)生Bowen Alpern正式界定了這些概念，并證明了我的預(yù)感是正確的。

“我引入了安全和活躍度概念后不久，Amir Pnueli（1996年圖靈獎獲得者）展示了如何使用時序邏輯（temporal logic ）對程序進行推理。你可以用相同的邏輯來表述程序及其屬性。對正確性的檢驗被簡化成觀察一個程序是否在邏輯上暗合其規(guī)范。”

Lamport和Susan Owicki證明，時序邏輯很適用于對活躍度的推理。但是，以時序邏輯來表述程序的想法并未奏效。

“這是一個絕妙的主意，”Lamport說：“只可惜它在實踐中行不通。”

一些人認為，解決的辦法是增加更多的復(fù)雜時序邏輯運算符，但Lamport卻另辟蹊徑。

“Amir Pneuli原先的邏輯只使用一個時間運算符：始終（always），”Lamport說：“有些事情“始終”是真的。人們加入了不同的復(fù)雜時序運算符，例如‘直到某些事情為真’，或‘直到其他一些事情為真’。”

事情變得尾大不掉，也由此不易理解。

“我有一個很好的點子，堅持使用單一的運算符，但是對運用于該運算符的基本非時序方程式加以變革，”他說：“我沒有使用只關(guān)注單一狀態(tài)的基本方程，而是加入了關(guān)注一對狀態(tài)——當(dāng)前狀態(tài)和未來狀態(tài)的方程。通過加入那些關(guān)注兩種狀態(tài)的方程，我就能夠描述一臺在這個邏輯下工作的狀態(tài)機。如果我能夠描述這個邏輯下的狀態(tài)機，就可以把活動度屬性描述成為時序方程式，進而就可以把整個程序或整個規(guī)范描述成為一個單一方程式——一個真正能夠工作的方程式。這就是TLA。”

TLA是TLA+規(guī)范語言、PlusCal算法以及與之相關(guān)工具的基礎(chǔ)。Lamport在2002年出版的專著中對TLA和TLA+做出了解釋：《規(guī)范系統(tǒng)：硬件和軟件工程師的TLA +語言及工具（Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers）》。其基本原則是，正式描述事物的最好辦法就是用簡單的數(shù)學(xué)，其推論是：一個規(guī)范語言除了精確編寫簡單數(shù)學(xué)算式所需的工具外，應(yīng)盡可能少地包含的其他內(nèi)容。

從DEC到微軟

Lamport在DEC任職期間，他曾有機會與計算機行業(yè)內(nèi)許多其他巨匠合作——而其中不少都曾服務(wù)于施樂公司富有傳奇色彩的帕洛阿爾托研究中心（Palo Alto Research Center）。Lamport在DEC任職期間的同事包括Levin、 Thacker、 Luca Cardelli、Gray和Lampson。DEC公司賣給康柏之后，研究實驗室逐漸萎縮，幾乎所有上述人士最后都從DEC轉(zhuǎn)到了微軟，但Lamport仍然很懷念他在DEC的經(jīng)理Bob Taylor。

         

過去30年間，Leslie Lamport曾經(jīng)為兩位經(jīng)理工作：Bob Taylor（左）和Roy Levin。

“我覺得Bob最突出的特點是他不太為自己考慮”，Lamport說：“他是這樣教導(dǎo)Roy Levin的——他的工作就在于讓我們保持快樂和高效。從某種意義上說，他在為我們工作，而不是我們?yōu)樗ぷ鳌?/p>

“在我為Bob工作的10年里，，他的辦公室門總是敞開的，我會經(jīng)常閑逛到那里和他聊天。有段時間，他卻拒絕我說：‘我現(xiàn)在很忙，能不能待會再來？’我至今仍然記得，因為這種情況實在是很少出現(xiàn)。”

但是，Lamport的傳奇生涯并沒有讓他為加入微軟之后的情況做好準(zhǔn)備。

“微軟整個企業(yè)上下對研究的態(tài)度與我曾任職的其他任何地方都不一樣，”他說：“微軟意識到，是研究人員貢獻了那些研究理念。

“公司能做的就是在研究人員和工程師之間架設(shè)溝通渠道，讓工程師知道研究人員正在做什么，而研究人員也能知道工程師面臨的問題是什么。微軟建立了項目經(jīng)理系統(tǒng)，并且將其作為一種常設(shè)機制來實現(xiàn)這一點。”

Lamport的杰出職業(yè)生涯也讓他體會到微軟研究方法的長處。

“我喜歡在一個企業(yè)研究院里工作，正是因為我能跟不同的人在一起，充分地接觸到各類現(xiàn)實的問題，”他說：“法國電影導(dǎo)演Jean Renoir在自傳中寫道，有人問他的父親（印象派畫家）Pierre-Auguste為什么取材于生活，并且把他的畫架拿到戶外而不是在工作室內(nèi)創(chuàng)作，他說：‘如果我在工作室里畫一棵樹，我會畫出五到六個不同種類的樹葉。我能想到的只有這么多。但是，當(dāng)我走進大自然時，發(fā)現(xiàn)了成千上萬種不同的葉子。我需要大自然給我靈感。’

“對我而言也是一樣。如果我靠自己提出問題，我只能拿出很少的東西，但如果我去外面的世界，那里的人們正在努力打造真正的計算機系統(tǒng)，會有100萬個問題等著我。我回顧自己的大部分工作——拜占庭將軍、Paxos等——他們都是來自現(xiàn)實世界的問題。”

2月13日，Lamport再次發(fā)現(xiàn)自己身處現(xiàn)實世界之中——進行LampsonFest的閉幕演說，這是微軟新英格蘭研究院為慶祝另一位計算機業(yè)界傳奇人物、Lamport的同事和朋友Butler Lampson的70歲生日而舉辦的活動。

在他的演講的開端，Lamport通過幻燈展示了自己的照片，緊跟著是一張Lampson照片。

“這就是我，”Lamport說：“而這是Butler。

“有人給我發(fā)電子郵件詢問我有關(guān)圖靈獎演講的事宜，我覺得其中可能存在混淆。所以，你應(yīng)該學(xué)會分辨我們。我是這個長胡子的。Butler是拿圖靈獎的。”

細細品味這個玩笑吧。我們沒有機會再聽到它了。