編譯 苦山

萊斯利·蘭波特徹底改變了計(jì)算機(jī)之間的交流方式。如今，他正致力于研究工程師如何與自己的機(jī)器交流。

計(jì)算機(jī)科學(xué)家萊斯利·蘭波特的成果使得現(xiàn)代計(jì)算機(jī)能夠有效地相互協(xié)調(diào)。從那以來，他將注意力轉(zhuǎn)向了提高編程本身的效率

萊斯利·蘭波特（Leslie Lamport）也許不是一個(gè)家喻戶曉的名字，但對于計(jì)算機(jī)科學(xué)家而言，他是以下成果的幕后功臣：排版程序LaTeX，以及使谷歌和亞馬遜的云基礎(chǔ)設(shè)施成為可能的研究。他還引領(lǐng)人們對一些問題給予了更多關(guān)注，給這些問題起了具有特點(diǎn)的名字，比如“面包店算法”和“拜占庭將軍問題”。這絕非偶然。這位81歲的計(jì)算機(jī)科學(xué)家對于人們?nèi)绾问褂煤涂创浖兄惡鯇こ５目b密考量。

2013年，他因在分布式系統(tǒng)方面的工作獲得了圖靈獎(jiǎng)，它被認(rèn)為是計(jì)算機(jī)領(lǐng)域的諾貝爾獎(jiǎng)。分布式系統(tǒng)是指不同網(wǎng)絡(luò)上的多個(gè)組件協(xié)同工作以實(shí)現(xiàn)共同目標(biāo)的系統(tǒng)?；ヂ?lián)網(wǎng)搜索、云計(jì)算和人工智能都涉及協(xié)調(diào)強(qiáng)大的計(jì)算機(jī)集群共同工作。當(dāng)然，這種協(xié)作會帶來更多的問題。

蘭波特曾經(jīng)說過：“在分布式系統(tǒng)中，若有一臺你甚至不知其存在的計(jì)算機(jī)出現(xiàn)故障，就可能導(dǎo)致你自己的計(jì)算機(jī)無法使用?！?/p>

其中最大的問題來源是“并發(fā)系統(tǒng)”，該系統(tǒng)中，多個(gè)計(jì)算操作會發(fā)生在重疊的時(shí)間片段上，致使模糊發(fā)生：哪臺計(jì)算機(jī)的時(shí)鐘才是正確的？在1978年一篇開創(chuàng)性的論文中，蘭波特利用狹義相對論中的某個(gè)觀點(diǎn)，引入了“因果關(guān)系”的概念來解決這個(gè)問題。兩個(gè)觀察者可能對事件的順序存在分歧，但是如果一個(gè)事件導(dǎo)致另一個(gè)事件，那么模糊性就得到了消除。發(fā)送或接收消息可以在多個(gè)進(jìn)程之間建立因果關(guān)系。邏輯時(shí)鐘——現(xiàn)在也稱為蘭波特時(shí)鐘——提供了一種推斷并發(fā)系統(tǒng)的標(biāo)準(zhǔn)方法。

有了這個(gè)工具，計(jì)算機(jī)科學(xué)家們接下來想知道他們?nèi)绾文軌蛳到y(tǒng)地?cái)U(kuò)大這些連接的計(jì)算機(jī)的規(guī)模，同時(shí)不增加錯(cuò)誤數(shù)量。蘭波特提出了一個(gè)優(yōu)雅的解決方案：Paxos，一種允許多臺計(jì)算機(jī)執(zhí)行復(fù)雜任務(wù)的“共識算法”。如果沒有Paxos及其算法家族，現(xiàn)代計(jì)算就不可能存在。

在20世紀(jì)80年代早期，蘭波特在開發(fā)這一領(lǐng)域時(shí)還創(chuàng)建了LaTeX，這是一個(gè)文檔準(zhǔn)備系統(tǒng)，它為復(fù)雜公式的排版和科學(xué)文檔的格式編排提供了精密巧妙的方式。LaTeX不僅在數(shù)學(xué)和計(jì)算機(jī)科學(xué)領(lǐng)域，而且在大多數(shù)科學(xué)領(lǐng)域都已成為論文格式編排的標(biāo)準(zhǔn)。

蘭波特參觀加利福尼亞州山景城的計(jì)算機(jī)歷史博物館

自20世紀(jì)90年代以來，蘭波特的工作主要集中在“形式驗(yàn)證”上，即利用數(shù)學(xué)證明來驗(yàn)證軟件和硬件系統(tǒng)的正確性。值得注意的是，他創(chuàng)建了一種名為行為時(shí)序邏輯（TLA+）的“規(guī)范語言”。軟件規(guī)范就像是程序的藍(lán)圖或配方，它描述了軟件在高層次上應(yīng)該如何運(yùn)行。這并非總是必需的，因?yàn)榫帉懸粋€(gè)簡單的程序就和煮雞蛋一樣輕松。但是，一個(gè)更加復(fù)雜、風(fēng)險(xiǎn)更高的任務(wù)——相當(dāng)于一場九道菜的宴席——?jiǎng)t要求更高的精確度。你需要準(zhǔn)備好每道菜的每個(gè)組成部分，將它們以一種精確的方式組合起來，隨后按照正確的順序提供給每位客人。這就需要用明確簡潔的語言寫出準(zhǔn)確的食譜和說明，但用英語寫出的描述可能會留下誤解的空間。TLA+采用精確的數(shù)學(xué)語言來防止錯(cuò)誤、避免設(shè)計(jì)缺陷。

一個(gè)叫做“模型檢查器”的程序會把你的“食譜”——也就是規(guī)范——當(dāng)作輸入，以檢查食譜是否有意義、是否按照預(yù)期的方式工作，從而按照廚師的要求生產(chǎn)出一道菜。蘭波特抱怨道，程序員時(shí)常先拼湊出一個(gè)系統(tǒng)，然后才編寫正確的規(guī)范，然而廚師若不事先知道他們的食譜可行，是絕不會為宴會提供食物的。

《量子雜志》與蘭波特討論了他在分布式系統(tǒng)方面的工作、計(jì)算機(jī)科學(xué)教育中的問題，以及使用TLA+如何能幫助程序員構(gòu)建更好的系統(tǒng)。為了清晰起見，下述訪談內(nèi)容經(jīng)過了整理簡編。

讓我們從Paxos開始聊吧，因?yàn)樗且粋€(gè)影響力如此之大的算法。你最初是出于什么理由著手開發(fā)它的？

人們用一些代碼建立了一個(gè)系統(tǒng)，而我有預(yù)感，他們的代碼想要完成的事情是不可能做到的。所以我決定嘗試證明這一點(diǎn)，并且想出了一種算法——人們理應(yīng)在他們的系統(tǒng)中使用這種算法。

他們原來的算法有什么問題？

這個(gè)嘛，他們原有的其實(shí)并非算法，而只是一堆代碼。很少有程序員從算法層面思考問題。在嘗試編寫并發(fā)系統(tǒng)時(shí)，如果只是編寫代碼而不使用算法，那么你的程序里必然全是錯(cuò)誤。

介紹Paxos的那篇論文起初并沒有得到廣泛的閱讀。為什么會這樣？

令人們無法閱讀這篇論文的原因是我喜歡用故事來解釋事物，而且我還為角色起了一些偽希臘字母的名字。例如，在論文中有一個(gè)奶酪檢查員名叫Γωδα。作為一個(gè)數(shù)學(xué)家，我整天和希臘字母打交道，也就沒有意識到非數(shù)學(xué)家會被這些字母嚇到。顯然，它們對讀者來說是個(gè)問題，因此讀這篇論文的人比預(yù)計(jì)的要少了許多。

所以，起初它的接受度并不高。盡管從長遠(yuǎn)來看，它還是得到了廣泛的認(rèn)可，因?yàn)槿藗儼堰@個(gè)共識算法家族稱為“Paxos”，而非“視圖戳記復(fù)制”（viewstamped replication），后者是計(jì)算機(jī)科學(xué)家芭芭拉·利斯科夫（Barbara Liskov）給同一算法起的另一個(gè)名字。

在從事了這么多年的分布式系統(tǒng)工作之后，又是什么讓你開始研究TLA+的？

在20世紀(jì)70年代，當(dāng)人們還在對程序進(jìn)行推理的時(shí)候，他們在做的是證明程序本身的屬性，并將這些屬性以編程語言的方式表述出來。隨后人們意識到，他們真正應(yīng)該表述的是程序應(yīng)該首先完成的任務(wù)，也就是程序的行為。

在20世紀(jì)80年代早期，我意識到為并發(fā)系統(tǒng)編寫這些高級規(guī)范的一種實(shí)用方法是將它們作為抽象算法來編寫。通過TLA+，我能夠以一種完全嚴(yán)謹(jǐn)?shù)姆绞皆跀?shù)學(xué)層面表達(dá)它們。于是一切都變得順利了。基本而言，這其中所涉及的并非試圖用編程語言來編寫算法：如果你真的想把事情做對，你需要用數(shù)學(xué)的方式來編寫算法。

你曾經(jīng)說過，如果你光思考卻不寫，那你就只是自認(rèn)為在思考罷了。這就是模型檢查的作用嗎？

模型檢查是對系統(tǒng)的小模型的所有執(zhí)行情況進(jìn)行詳盡測試的一種方法。它只顯示模型的正確性，而非算法的正確性。當(dāng)模型檢查測試正確性時(shí)，編碼只生成代碼。它并不測試任何東西。在模型檢查出現(xiàn)之前，確保算法有效的唯一方法是編寫一個(gè)證明。

在實(shí)踐中，模型檢查會檢查算法的一個(gè)小實(shí)例的所有執(zhí)行情況。如果你足夠幸運(yùn)，你可以檢查足夠大的實(shí)例，這會讓你對算法產(chǎn)生足夠的信心。但這一證明可以確證它對于任何規(guī)模的系統(tǒng)和算法的任何應(yīng)用都是正確的。

聽起來，模型檢查與另一種程序驗(yàn)證方法有關(guān)：使用Coq等工具進(jìn)行交互式定理證明。它們有什么不同？

Coq旨在進(jìn)行真正的數(shù)學(xué)運(yùn)算，并能夠捕捉數(shù)學(xué)家所做的推理。例如，喬治·龔提爾（Georges Gonthier）正是用它證明了四色定理。一個(gè)經(jīng)過了機(jī)器檢查的數(shù)學(xué)陳述的證明表明，該陳述幾乎肯定為真。

蘭波特在過去幾十年里開發(fā)的規(guī)范語言TLA+允許工程師以精確的數(shù)學(xué)方式描述程序的目標(biāo)

TLA+不是為數(shù)學(xué)家設(shè)計(jì)的，而是為那些想要證明其系統(tǒng)屬性的工程師設(shè)計(jì)的。20世紀(jì)90年代，在花費(fèi)了大約15年的時(shí)間編寫并發(fā)算法的證明之后，我了解到了需要做哪些事才能證明并發(fā)算法的正確性。TLA是一種允許完全形式化的邏輯。TLA+則是基于此的完整語言。

像TLA+這樣的規(guī)范語言并沒有在行業(yè)中得到廣泛的應(yīng)用，對吧？你認(rèn)為這是為什么呢？

這個(gè)嘛，我盡力而為了。但基本上，程序員和許多計(jì)算機(jī)科學(xué)家（甚至是絕大多數(shù)計(jì)算機(jī)科學(xué)家）都對數(shù)學(xué)心懷恐懼。所以這是一個(gè)很艱難的推廣過程。

其次，每個(gè)項(xiàng)目都必須在匆忙中完成。有句老話說：“永遠(yuǎn)沒有時(shí)間去把事情做對。但總有時(shí)間把事情再做一遍?！庇捎赥LA+涉及一些前期工作，這意味著你在開發(fā)過程中添加了一個(gè)新步驟，這也讓它的推廣變得很難。

這種前期努力是否總是值得？

的確，世界各地的程序員所編寫的大多數(shù)代碼并不需要事先非常精確地說明它應(yīng)該做到什么。但有些的確重要，它們需要是正確無誤的。

蘭波特認(rèn)為，在編程前先行思考和寫作極為重要，這一點(diǎn)需要在本科計(jì)算機(jī)科學(xué)課程中進(jìn)行教授，但實(shí)際并未如此

當(dāng)人們制造芯片的時(shí)候，他們希望芯片能正常工作。當(dāng)人們構(gòu)建云基礎(chǔ)設(shè)施時(shí)，他們不希望出現(xiàn)會丟失人們數(shù)據(jù)的錯(cuò)誤。對于那種精度非常重要的應(yīng)用程序，你需要非常嚴(yán)格，需要類似TLA+這樣的東西，特別是在涉及并發(fā)的情況下，而這些系統(tǒng)中通常都會涉及并發(fā)。

程序員是否傾向于把更多的時(shí)間花在寫代碼上，而非在思考代碼上？

是的，在編程前先行思考和寫作極為重要，這一點(diǎn)需要在本科計(jì)算機(jī)科學(xué)課程中進(jìn)行教授，但實(shí)際并未如此。其原因在于，教授程序設(shè)計(jì)的人和教授程序驗(yàn)證的人之間缺少交流。

在我看來，這一分歧的雙方都有錯(cuò)。教編程的人不了解驗(yàn)證，但他們理應(yīng)了解。教驗(yàn)證的人員則不了解如何在實(shí)踐中應(yīng)用驗(yàn)證。

在這一鴻溝彌合之前，TLA+是不會擁有大量用戶的。我希望我至少能讓教并發(fā)編程的人明白他們需要它。這樣也許才會有一些希望。

我感覺你對最近的計(jì)算機(jī)科學(xué)教育不太滿意。是因?yàn)樗鼪]有給予數(shù)學(xué)足夠的重視嗎？

對數(shù)學(xué)思維的重視不夠，沒錯(cuò)。

蘭波特因其在計(jì)算機(jī)協(xié)作（該領(lǐng)域被稱為分布式系統(tǒng)）方面的成果獲得了2013年的圖靈獎(jiǎng)。他的Paxos算法現(xiàn)已成為行業(yè)標(biāo)準(zhǔn)

那么，換做是你的話，會如何構(gòu)建本科課程呢？

我不是教育工作者，所以我并不清楚怎么教他們數(shù)學(xué)思維。但我知道人們應(yīng)該學(xué)什么。他們不應(yīng)該害怕數(shù)學(xué)。這只是簡單的數(shù)學(xué)，他們可能已經(jīng)上過一門相關(guān)課程，卻不知道如何運(yùn)用它。他們不知道數(shù)學(xué)有什么好處。他們學(xué)到的知識足以通過考試，然后就把學(xué)過的東西忘了。

數(shù)學(xué)家常說他們在數(shù)學(xué)中看到美。你是從這個(gè)領(lǐng)域起步的，那么你看到算法之美了嗎？

我不從美學(xué)的角度考慮。我可能和其他人有同樣的感受，但我會用不同的詞語來表述它們。我不會說算法是“美”的。但“簡潔”是我非?？粗氐臇|西。

最后一個(gè)問題，是關(guān)于你的另一個(gè)具有相當(dāng)大影響力的項(xiàng)目LaTeX的。我想最后和你這位創(chuàng)造者澄清一件事。它的發(fā)音是“LAH-tekh”還是“LAY-tekh”？

哪個(gè)都行。我不建議你花太多時(shí)間思考這件事。

資料來源 Quanta Magazine