--- id: "U719vQz-WFs" title: "图灵奖得主 Leslie Lamport：清晰思考、Paxos 与 Raft，以及与 Dijkstra 共事" channel: "Ryan Peterman" host: ["Ryan Peterman"] guests: ["Leslie Lamport"] date: "2026-02-23" updated: "2026-08-26" duration: "1:10:19" duration_seconds: 4219 source_type: "youtube" youtube: "https://www.youtube.com/watch?v=U719vQz-WFs" canonical: "https://pod-exp.pages.dev/U719vQz-WFs/" transcript_jsonl: "https://pod-exp.pages.dev/U719vQz-WFs/transcript.jsonl" language: "zh-CN" translation: true translated_from: "en" timestamp_precision: "block" topics: ["数学与科学","产业科技","人生方法"] series: ["Leslie Lamport"] --- # 图灵奖得主 Leslie Lamport：清晰思考、Paxos 与 Raft，以及与 Dijkstra 共事 > 中文译文，由英文原音字幕翻译整理，不是官方逐字稿；引用原话请核对英文原视频。说话人标签由整理者依上下文标注，带「未确认 / 未标注 / 不确定」等字样的标签不可靠。时间戳一般为块级（所在时间块的起点），不是逐句时间；正文自带 [hh:mm:ss] 的段落除外。 **内容提要：** 这场对谈沿着 Leslie Lamport 五十余年的工作脉络，串起面包店算法、与 Dijkstra 的交往、happens-before、状态机与不变量、拜占庭将军问题、Paxos、Raft、LaTeX，以及他对写作、证明和抽象的长期看法。Lamport 反复强调：并发系统真正困难的不是把代码写出来，而是找到合适的抽象、明确系统状态，并写下能够经受检查的证明。他也解释了为何自己更看重“能证明”的理解，而不是一种直觉上舒服的感觉；以及为什么数学、状态机和写作会迫使人暴露尚未说清楚的部分。 ## [0:02] 开场：写下来，才算真的知道 · YouTube **Leslie Lamport：** 如果你以为自己知道一件事，却不把它写下来，那你只是以为自己知道。 **Ryan Peterman：** 这位是 Leslie Lamport。他是图灵奖得主，以对分布式系统的贡献闻名。我采访他，想听听那些论文背后的故事。 **Leslie Lamport：** 他们的反应让我很震惊。他们生气了。我真的觉得他们可能会对我动手。 **Ryan Peterman：** Dijkstra 原来的解法到底有什么地方让你不满意？ **Leslie Lamport：** 那个想法对大多数人来说并不显而易见，而这件事其实给 Dijkstra 留下了印象。 **Ryan Peterman：** 作为 Paxos 算法的发明者，我也问了他怎么看与之竞争的 Raft 算法。 **Leslie Lamport：** Raft 后来发现了一个 bug，也修掉了；但我相信，当时大家觉得“更容易理解”的那个算法版本，恰恰是带着这个 bug 的版本。 **Ryan Peterman：** 我也很喜欢回望他五十年的职业生涯。你会说自己从来没觉得自己聪明——这怎么可能？ **Leslie Lamport：** 笨的人觉得自己聪明，因为他们笨到意识不到自己其实并不聪明。 **Ryan Peterman：** 你还写过，自己有段时间觉得像个失败者，因为你想找到一个宏大的并发理论，却一直没有找到。你现在还这么想吗？下面是完整访谈。我们从面包店算法开始：它到底解决什么问题？你又是怎么发现这个问题的？ ## [1:25] 面包店算法：并发、临界区与一次失败的投稿 · YouTube **Leslie Lamport：** 这个问题是 Edsger Dijkstra 在一篇 1965 年——我想是 1965 年——的论文里提出或发现的。我把那篇论文看成并发理论、并发程序设计真正的开端。他是第一个真正把“并发”当成组织程序的方法来使用的人：程序由一组半独立的任务组成，而这些进程必须彼此同步。 **Leslie Lamport：** 那是分时系统刚刚起步的年代，多个用户开始共用同一台计算机。大家意识到计算机比人快得多，而且当时计算机非常昂贵，所以很自然地希望同一台机器可以同时服务很多人。每个用户运行的程序可以彼此独立，但有些资源必须共享。最直观的例子就是打印机：两个人同时往同一台打印机打印，结果显然不会令人满意。 **Leslie Lamport：** Dijkstra 因此提出了“临界区（critical section）”这个概念：每个进程都有一段代码，在任何时刻最多只能有一个进程执行它。比如，那段代码可能就是实际操作打印机的代码。于是问题变成：怎样让多个进程自己协调，使任何时候最多只有一个进程进入它的临界区？ **Leslie Lamport：** 我是在 1972 年知道这个问题的。当时《Communications of the ACM》上有一篇文章给出了一个解法。我以前写程序，也喜欢这种小型的编程题；这个问题看起来就像一道很漂亮的小题。我看了那个相当复杂的解法，心想：“哦，天哪，这应该没那么难吧。”于是很快写了一个适用于两个进程的简单算法，投给了 CACM。 **Leslie Lamport：** 几周后，编辑给我回信，指出了程序里的 bug。这件事产生了两个后果。第一，我意识到并发程序非常难写对，你必须证明它是正确的；第二，它让我产生了一个很直接的念头：我非得把这个该死的问题解决掉不可。 **Leslie Lamport：** 后来我想出了面包店算法。灵感来自现在常说的 deli counter 场景：柜台边有一卷号码票，每位顾客进来取一个号，接下来服务尚未被叫到的号码中最小的那个。原话里我先说成“最高号”，马上又自我修正成“最低号”；关键就是大家按取号形成先后次序。 ## [5:26] 面包店算法：无需原子读写的惊人性质 · YouTube **Leslie Lamport：** 我借用了“取号”的想法，但 Dijkstra 定义的问题没有中央控制器，所以不能有一个中央机器统一发号。每个进程都必须自己选自己的号码。这就是核心想法，算法本身其实相当简单。 **Leslie Lamport：** 然后我写了正确性证明。正是证明让我发现，这个算法有一个非常有趣、甚至出乎当时直觉的性质。当时普遍有人认为——甚至有人在书或论文里写过——如果没有某种更底层的互斥机制，就不可能实现这种互斥。通常假定的底层机制是共享寄存器，也就是不同进程都可以读写的共享内存位置。 **Leslie Lamport：** 大家的直觉是，你不能允许两个进程同时写同一个寄存器，也不能允许一个进程读的时候另一个正在写；这些动作必须是原子的，表现得好像总能排成某个明确的先后顺序。但面包店算法令人惊讶的地方就在这里：它不需要这种假设。 **Leslie Lamport：** 算法让每一块共享内存只由一个进程负责写，所以不会出现两个写者彼此冲突。唯一麻烦的是：某个进程可能恰好在另一个进程写这个值的时候去读它，于是读到一个未知值。可算法照样成立。甚至可以说，读者在与写入并发时读到任何值，算法仍然有效。 **Ryan Peterman：** 我看到你写过，你把这个结果给一位字幕转写成 “Anatol Hol” 的同事看。证明太不可思议了，以至于他一开始根本不相信？ **Leslie Lamport：** 对，真正不可思议的是这个结果本身。 **Ryan Peterman：** 对，他不相信。 **Leslie Lamport：** 我就在白板上把证明写给他看。他当场找不到问题，但回家时还坚持说：“这里肯定有什么地方错了。”显然，他后来也一直没有找到那个错误。 ## [8:28] Dijkstra 的旧解、饥饿问题与 EWD · YouTube **Ryan Peterman：** 你的论文题目是《A New Solution of Dijkstra's Concurrent Programming Problem》。Dijkstra 原来的方案具体哪里让你不满意，以至于你还想再解一次这个问题？ **Leslie Lamport：** 他原来的方案有一个不太理想的性质：如果不断有进程试图进入临界区，其中某个进程可能一直被“饿死（starved）”，永远得不到进入临界区的机会。后续有一个解法——我想是 Don Knuth 的——处理了这个问题。那时大家衡量方案好坏的一个条件，就是一个进程可能需要等待多久。 **Leslie Lamport：** 我相信面包店算法是第一个真正做到“先到先服务”的方案。这里的意思是：如果一个进程先选好了号码，之后另一个进程才开始尝试进入，那么前一个进程会先进入临界区。我相信面包店算法是第一个具有这个性质的算法，而且我也觉得它比其他一些解法更简单。 **Ryan Peterman：** 你的很多文字里都会提到 Dijkstra。我还看到，1976 年你去荷兰待了一个月，也和他们一起工作。能讲讲那段经历吗？ **Leslie Lamport：** Dijkstra 有一类以自己姓名首字母命名的小文稿，叫 EWD。他想到什么，就会写下来，然后发给一些人。其中一篇 EWD 讲的是他和几位合作者——或者说更像他的学生、受他指导的人——写出的一个算法，那是最早的并发垃圾回收算法之一。 **Leslie Lamport：** 当时程序设计已经出现这种模式：有一个内存池，程序需要一块内存时向某个服务请求，然后得到一块；可到了某个时刻它不再使用这块内存，而最初创建它的进程未必知道有没有别的进程还在用它。所以系统需要另一个叫垃圾回收器的进程，去检查哪些内存已经没人使用，再把它们放回所谓的 free list，让分配内存的进程以后重新拿来用。 **Leslie Lamport：** 我看了他们的算法，发现可以简化。原方案把 free list 当成一个需要特殊处理的对象，由一个特殊进程管理，因此还得考虑它和使用内存的其他进程如何协调。我意识到 free list 完全可以只是普通数据结构的一部分，不需要特殊待遇。对我来说这只是一个很简单、很显然的想法，于是我把它发给了 Dijkstra。后来收到下一版论文时，我发现他把我列成了作者。 ## [12:31] 抽象能力、荷兰一个月与每周的啤酒 · YouTube **Leslie Lamport：** 我当时觉得他这么做非常慷慨，因为在我看来那只是一个非常简单、非常明显的点。很久以后我才明白，它对大多数人其实并不明显，而恰恰是这个想法给 Dijkstra 留下了印象。那基本上也是我真正和 Dijkstra 共同完成的唯一一件工作。 **Leslie Lamport：** 很多年以后，Dijkstra 说我有一种“非凡的抽象能力”。直到很近这些年——也许是拿到图灵奖以后——我才意识到，我之所以能取得那些成果、最后得到图灵奖，并不是因为我有多么高的“原始智力”，而是因为我有抽象这项天赋。Dijkstra 很早就看出来了。 **Leslie Lamport：** 那次我受邀去荷兰待一个月，不过并不是直接和 Dijkstra 共事，而是和一位字幕转写成 “Carl Carl Holton” 的同事一起。那一个月最终真正发表出来的东西只有一项。我们每周会和 Dijkstra 见一次，在讨论中不知怎么冒出了一个想法，后来变成面包店算法的一个变体，我把它写成论文发表了。这就是那一个月最具体的产出。 **Ryan Peterman：** 我也看到你写过：每周有一个下午是在 Dijkstra 家里一起工作、聊天、喝啤酒，而且你后来都不太确定那篇工作里到底谁负责了哪部分。 **Leslie Lamport：** 是啊。不过我觉得自己应该没喝到那么醉，因为我大概还得自己开车去、再自己开车回来。 **Ryan Peterman：** 对，对。 **Leslie Lamport：** 而且我当时喝的荷兰啤酒，酒精度也没那么高。 ## [14:44] 《Time, Clocks...》：从相对论到 happens-before · YouTube **Ryan Peterman：** 我想谈谈你被引用最多的论文，《Time, Clocks, and the Ordering of Events in a Distributed System》。这篇论文背后的故事是什么？你当时想解决什么问题？ **Leslie Lamport：** 起点很简单。有人给我发了一篇关于分布式数据库的论文：同一份数据在不同地方有多个副本，你必须想办法让它们保持同步。我读后发现，他们的方案会让一些操作“看起来像”按照某个序列执行，但那个序列可能和事件真正发生的先后不同。 **Leslie Lamport：** “一个事件发生在另一个事件之前”到底是什么意思，其实并不显然——至少对多数人不显然。但我碰巧学过狭义相对论，尤其是把空间和时间放在一起看成四维整体的时空观。爱因斯坦在 1905 年写了他的论文；然后我想大概在 1909 年，还有一个人提出了这种四维视角——他的名字我这会儿想不起来了。 **Leslie Lamport：** 在那个四维视角里，一个事件“先于”另一个事件有一个具体含义：如果第一个事件发出一个信号，而这个信号能够在第二个事件发生之前被第二处接收到，那么第一个事件可以在因果上先于第二个；当然通信不能比光速更快，因为没有东西能超越光速。 **Leslie Lamport：** 我意识到这里有一个非常直接的类比。在分布式系统里，happens-before 的含义和相对论里几乎一样，只不过不再问“以光速传播的影响能否从第一个事件到达第二个事件”，而是问：系统里真实发送的消息，是否可能让第一个事件的信息影响第二个事件。 **Leslie Lamport：** 真正让很多人震动的是这个 happens-before 定义。我甚至会把它称为分布式系统里最早具有“科学结果”意味的论文之一。不过我可能犯了一个别人后来提醒过我的错误：在一篇论文里塞了两个想法。 **Leslie Lamport：** 另一个想法是：可以构造一种排序，使它满足——如果事件 A happens-before 事件 B，那么 A 在这个排序里也一定排在 B 前面。只要能做到这一点，就可以提供构建任意分布式系统所需要的同步，因为你可以把系统描述成一台状态机。 ## [18:47] 状态机、不变量与为什么顺序推理会失控 · YouTube **Leslie Lamport：** 我当时说的状态机，就是一个有“状态”的东西，进程按顺序执行命令；一条命令改变状态，并产生一个值。所以你只需要描述：每条命令怎样把原状态变成新状态，以及它根据原状态会产生什么值。 **Leslie Lamport：** 这件事对我来说实在太明显了，但从实践角度看，它其实是那篇论文里非常重要的思想：你可以用状态机来思考如何构建分布式系统，也可以用状态机来理解并发系统。可这一部分当时几乎完全被忽略了。 **Leslie Lamport：** 我甚至有过两次这样的对话：别人跟我说，那篇论文里根本没有谈状态机。我只好回去一遍又一遍重读自己的论文，确认自己是不是疯了。结果它真的谈了状态机。 **Leslie Lamport：** 状态机还有另一个重要性。通常我们写并发程序时——面包店算法反而算一个例外——会假设动作是原子的，因此一次执行可以看成一串事件。对普通程序，我们很容易说：“给它正确输入，它就会产生正确答案。”可程序执行到一半时，一开始输入了什么已经是古代史；真正决定下一步做什么的，是当前状态。 **Leslie Lamport：** 所以理解一个程序的方法，是找出每一个时刻“状态所满足的什么性质”能够保证最终答案正确。这个性质在数学上就是一个取布尔值的状态函数，我们称它为不变量（invariant）。理解不变量，就是理解系统。我后来意识到，这对并发系统和并发程序同样成立。 **Leslie Lamport：** 很多人喜欢写那种沿着行为序列推演的证明。但问题是，可发生的序列数量随着长度迅速爆炸，推理就会越来越复杂，也非常容易漏掉情况。说到这里我自己还修正了一下表述：可能执行的数量随进程数呈指数增长，而不变量证明需要检查的结构，粗略说却只以进程数的二次量级增长。这就是为什么不变量证明更可控。 ## [22:47] 偏序并非总是实用默认 · YouTube **Leslie Lamport：** 很长时间里，做分布式系统理论的人一直试图发展基于偏序的各种方法和形式体系，也发表了很多论文。但如果你的目标是实际把东西做出来，我认为那通常不是最好的默认方法——不过我不该说得那么绝对。 **Leslie Lamport：** 像面包店算法这样的例外确实存在：对它来说，用偏序思考反而非常合适。但一般而言，如果你想要一种你可以有把握地反复使用的方法，我认为还是不变量。 ## [23:26] 拜占庭故障：从数字签名开始 · YouTube **Ryan Peterman：** 我想谈下一篇论文，也就是拜占庭将军问题。计算机专业的学生几乎都会听过它，而且这个名字本身就很好。这个问题背后的故事是什么？ **Leslie Lamport：** 我写完那篇 Time, Clocks 论文以后，里面讲的是怎样构造分布式系统，但假设系统不会发生故障。可大家采用分布式系统的一个重要理由，恰恰是你有多台计算机：一台坏了，其他机器还能继续工作。后来我加入的 SRI 那边就在解决这类问题，但在去 SRI 之前我已经开始思考它了。 **Leslie Lamport：** 我当时没有一个现成的故障模型，不知道应该假设“坏掉的进程能做什么”，于是干脆取最坏情况：一个故障进程可以做任何事情。在这个假设下，我想出了一个基本上可以实现容错状态机的算法，而那个算法使用数字签名。也就是说，故障进程虽然可以胡作非为，却不能伪造另一个进程的签名。 **Ryan Peterman：** 也就是说，这让你可以相信一条消息确实来自拥有相应私密凭据的那一方？ **Leslie Lamport：** 对。这样一条消息可以被转发，其他人仍然能检查：这条被转发的消息是不是原发送者真正签过的那条消息。 **Leslie Lamport：** 到 SRI 以后，我发现他们在解决同一个问题，但有两点不同。第一，当时大约是 1975 年，知道数字签名的人非常少。我记不清 Diffie-Hellman 那篇论文具体什么时候发表，不过差不多就在 1975 年。我之所以知道数字签名，是因为 Whit Diffie 是我的朋友，他也是那篇论文的两位作者之一。 **Leslie Lamport：** 有一次我们在咖啡馆里，他跟我说起这些东西，说他们有一个问题：需要构造数字签名，还没解决。我说：“哦，这看起来挺容易。”然后真的就在一张餐巾纸上写出了一个数字签名算法。我会说那是最早的数字签名算法之一，但当时完全不实用：大概要用 128 bit 左右去给 1 bit 的内容签名。 **Leslie Lamport：** 不过也没有听起来那么糟，因为你不一定要对整份文档签名，可以对文档的 hash 签名，前提是你认为别人无法伪造那个 hash。 **Ryan Peterman：** 也就是没法把 hash 反过来？ **Leslie Lamport：** 对，不能反过来——不能拿着一个 hash，再轻易找出另一个文档让它满足同一个 hash。总之，这就是为什么数字签名已经在我的工具箱里。SRI 的人当时没有这个工具，不过他们对问题的抽象其实比我的更漂亮：不是让各个进程一次对整串命令达成一致，而是先有一个算法，只对一条命令达成一致。 ## [27:30] 四台还是三台：无签名与有签名的差别 · YouTube **Leslie Lamport：** 然后把这个“对单条命令达成一致”的算法重复执行，就能处理一连串命令。这比我的描述方式更干净。最初发表的论文同时给出了两类算法：他们没有数字签名时用一种不同的算法，而有数字签名时可以用另一种。 **Leslie Lamport：** 对一个故障进程来说，无数字签名时需要四个进程；如果使用数字签名，只需要三个。因此原论文把两种算法都放进去，我也就成了作者之一。没有数字签名的那个算法更复杂。 **Leslie Lamport：** 一般情形的算法真的像天才之作，几乎到了难以理解的程度。源字幕在这里把一般公式转写成了“为了容忍 n 个故障，需要 four n 个进程；使用数字签名时需要 three n 个进程”。我先保留这段字幕的字面信息，不在正文里偷偷把它改成另一个公式。单故障版本不算难，多故障版本则是字幕转写为 Marshall “Peas” 的那位合作者做出来的，我觉得极其精彩。 **Leslie Lamport：** 后来在另一篇论文里，我找到了一个更简单的归纳证明：大意是从 n-1 的情形推出 n 的情形。不过这一段源字幕中的式子也明显转写损坏，出现了类似 “3 n * n minus one” 的片段。我能确定的是，我当时在对比后来更简单的归纳证明和原论文里那个极其聪明、但非常难读的证明；原来的工作依然让我觉得“到底是谁能想得出来啊”。 **Leslie Lamport：** 论文发表以后，我也更明确地意识到“拜占庭故障”这个概念：这里的故障不是进程停机，而是我们必须假定一个进程可以做任何事情。我一开始这么假定，只是因为我不知道还能假定什么；而 SRI 的人是因为有非常实际的理由——他们拿着一份合同，要给飞机做多处理器、多计算机系统，所以他们真正需要考虑那种你无法预测其行为的故障。 **Leslie Lamport：** 你会不断遇到这样的诱惑：比如想用三个进程容忍一个故障，写出一个看起来似乎能工作的算法，然后觉得“那个反例现实里不可能发生”。可再往下推，总能构造出一串完全说得过去的故障，让那个算法在存在一个故障进程时失败。所以最后你还是需要四个。 **Leslie Lamport：** 我当时还觉得，数字签名在这个算法里也许有点像一种隐喻：我们关心的不是恶意攻击，而是随机发生的硬件故障，那么也许存在某种“类似签名”的机制，把失败概率做得足够低。但我没有继续研究，后来似乎也没人真的沿这个方向做。所以那套使用数字签名的算法在当年很大程度上被忽略了，因为数字签名的计算成本太高。 ## [31:30] 为什么要给问题讲一个“好故事” · YouTube **Leslie Lamport：** 至于现在怎样，我并不清楚。今天数字签名归根到底就是计算，而计算已经很便宜了。曾经有一次，我和一位 Boeing 的工程师通信，我问他们知不知道这些结果。他说知道，而且当初在 Boeing 读那篇论文的人就是他。他看完后的反应非常直接：“哦，那我们需要四台计算机。” **Leslie Lamport：** 无论如何，我意识到这是一个重要结果，应该让更多人知道。我从 Dijkstra 那里学到过一件事。他写过著名的“哲学家就餐问题”。我不展开那个问题本身；坦率说，我觉得它的基础问题未必特别有趣，但它有一个很可爱的故事。 **Leslie Lamport：** 一群哲学家围着桌子坐，吃一种奇怪的意大利面，必须同时拿两把叉子；而每把叉子夹在两个人之间，由相邻两个人共享。我觉得，正是这个故事让那个问题流行了起来。于是我决定，我们的工作也需要一个好故事。 **Leslie Lamport：** 我就发明了“拜占庭将军”的叙事。以容忍一个故障为例，有四位将军，他们必须就“进攻还是撤退”达成一致。如果足够多的人一起进攻就能获胜；字幕里我的例子说，三个人进攻也能赢，但只有两个人进攻会输。问题是，其中一位将军可能是叛徒。那其他人怎样通过通信，仍然做出同一个进攻或撤退的决定？这就是“拜占庭将军问题”。 **Ryan Peterman：** 我在你的笔记里看到，好像还有一个更早或不同的问题，叫“中国将军问题”之类？ **Leslie Lamport：** 对，但那是另一个问题。Jim Gray 把一个不可能性结果描述成“中国将军问题”，我不打算在这里展开。它给了我“将军”这个故事的灵感。 **Leslie Lamport：** 我最初其实想叫“阿尔巴尼亚将军”。那时阿尔巴尼亚对外部世界几乎像个黑洞，是共产主义政权，属于苏联阵营，而且在我印象里比苏联本身还要封闭、限制更多。我的老板提醒我：“世界上真的有阿尔巴尼亚人，你是不是应该换个名字？”我这才想到，今天已经没有“拜占庭人”这个现实族群了，于是 Byzantine 成了一个完美的名字。 ## [35:33] 飞机、任意故障与“值得解决的问题” · YouTube **Ryan Peterman：** 这个故事很有意思：问题并不是第一次被提出，但你给了它一个抓人的名字，又增加了一些结果。你当时为什么会觉得它值得投入时间？更一般地说，你怎么判断一个问题值得做？ **Leslie Lamport：** 对这个问题，当时的现实价值非常明显：计算机迟早要控制飞机。那正值 20 世纪 70 年代的石油危机，人们知道可以通过减小飞机控制面的尺寸来提升能源效率，但这样会让飞机在空气动力学上变得不稳定。飞行员没法手动完成保持飞行所需的所有快速微调，而计算机可以。所以未来的飞机会由计算机控制，这一点很清楚——今天也确实如此。 **Leslie Lamport：** 当时不少人想当然地认为：如果要容忍一个故障，用三台计算机就够了。他们没有意识到，对任意故障来说你需要四台。这是一个真正重要、而且会影响实际系统设计的结果，所以我认为必须让大家知道。 **Ryan Peterman：** 如果把这个问题放到你整个职业生涯里看呢？在公司里可以用赚钱、节省成本之类的指标判断。但像面包店算法以及你后来的工作，问题空间很开放。你怎么知道什么值得解决？ **Leslie Lamport：** 我的整个职业生涯都在私人公司，而不是大学或政府。有些问题就是工程师带到我面前的：他们真的遇到了一个问题，需要一个答案。Paxos 就是这种情况——确实有人想要一个能完成那件事的算法。 **Ryan Peterman：** 那我们就谈 Paxos。它是你最著名的工作之一。那篇论文以及它试图解决的问题，故事是怎样的？ ## [38:05] Paxos 的起点：代码不等于算法 · YouTube **Leslie Lamport：** Paxos 要解决的，本质上和拜占庭将军工作中的问题相同：构造一个容错状态机。只是到了那个阶段，工业界真正关心的故障类型通常不再是“机器会任意作恶”，而是“机器停掉了”。Paxos 针对的就是这类故障。 **Leslie Lamport：** 我 1985 年加入了字幕转写为 “DEC SRC / deck circ” 的研究机构。那里的人里有不少来自 Xerox PARC，他们参与发明了个人计算，也有“分布式个人计算”的观念；Ethernet 也是为了这类环境发展出来的。大楼里的计算机连在同一个以太网上，共享一套公共存储。 **Leslie Lamport：** 他们已经有一套办法维持共享存储的一致性。准确地说，他们并没有一个“算法”的抽象描述，而是有一个操作系统，里面有一堆代码在做这件事。我当时甚至不相信他们做到的事情是可能的。至于当时为什么觉得不可能，我现在已经记不太清。 **Leslie Lamport：** 总之，我开始尝试写一个“不可能性证明”：如果有一个算法能解决问题，那它必须先做这个；为了做这个，又必须做那个……写着写着，我突然停下来意识到：“哦，这不是一个不可能性证明。等等——这就是一个能做成这件事的算法。” **Ryan Peterman：** 你刚才说，他们有代码，但没有算法。你是什么意思？ **Leslie Lamport：** 对。 **Ryan Peterman：** 大多数人坐下来写程序时，第一反应不就是直接想代码吗？ **Leslie Lamport：** 我职业生涯比较早的时候就逐渐意识到，“程序”和“算法”不是一回事。当年大家会把这些东西都叫 program，我自己可能也这么叫。后来我发现，我真正感兴趣的是算法。 **Leslie Lamport：** 程序是用某一种具体语言、具体代码写出来的；算法更抽象，同一个算法可以由很多不同语言的程序实现。它处在更高的抽象层。当然我喜欢这种东西，因为后来我才意识到，抽象正是我擅长的事。 ## [42:05] 抽象层、八年发表间隔与 Paxos 的古代故事 · YouTube **Leslie Lamport：** 大概从 2000 年前后开始，我职业生涯里很大一部分工作，就是劝做并发系统的人：不要只写代码，你得先有一个算法。一个完整系统当然会做很多事情，但其中应该存在一个核心，专门负责不同进程、不同计算机之间的同步。 **Leslie Lamport：** 这部分代码极难写对。你不应该一开始就陷在具体代码里，因为编码会把许多与并发本质无关的问题混在一起。应该先得到一个负责同步的算法，弄清楚它为什么正确，然后再实现它。 **Ryan Peterman：** 我看 Paxos 论文和你的笔记时注意到，从你想出算法到《The Part-Time Parliament》真正发表，中间隔了八年。为什么会隔这么久？ **Leslie Lamport：** 最初审稿人的意见大致是：论文还行，但好像也没那么重要。幸运的是 Butler Lampson 看出了算法的重要性，也看出“状态机可以实现很多东西”这个思路的价值。他到处推动大家用 Paxos、用状态机来构造系统。所以核心思想已经在传播，我自己就不着急发表，把论文在那里放了很久。 **Leslie Lamport：** 后来换了一位新编辑。他发现论文当时大概已经处在“原则上接受，但需要修改”的状态，于是决定把它推进发表。真正出版前又补了一些东西，主要是提到这几年间已经发生的相关工作。我请 Keith Marzullo 帮我处理了那一部分。 **Leslie Lamport：** Paxos 那篇论文采用了一个故意的叙事框架：把它写成发生在几百年前、后来发现的一份古代手稿。凡是我觉得太显然、不值得详细写的部分，就会用类似“现在已经不清楚 Paxos 人当时究竟是怎么做的”来带过。Keith 也延续了这个玩笑，给它写了点像前言之类的东西，我想还补了些引用。 **Ryan Peterman：** 我还看到你最初讲这篇论文时，甚至打扮成印第安纳·琼斯风格的考古学家。 ## [46:06] 印第安纳·琼斯式演讲与 Butler Lampson · YouTube **Ryan Peterman：** 那场关于 Paxos 论文和算法的演讲效果怎么样？ **Leslie Lamport：** 演讲本身也许还不错，但我觉得没人真正理解算法，也没人理解这个算法为什么重要。 **Ryan Peterman：** 听起来唯一理解它的人好像是 Butler Lampson。为什么他不一样？他看到了什么？ **Leslie Lamport：** 他非常懂怎样构建系统。他完全配得上自己的图灵奖。他是 Xerox PARC 最早那批做分布式个人计算的人之一。我想，他和 Chuck Thacker 大概是实验室里资历最深、最核心的两个人。 **Ryan Peterman：** 后来又有一篇论文提出了一个看起来解决同样问题的新算法，也就是 Raft。我想知道你有没有读过，以及你怎么看 Raft 和 Paxos 的关系。 ## [46:59] Paxos vs Raft：两阶段、领导者与“更好理解” · YouTube **Leslie Lamport：** Raft 的作者其实给我发过最初论文的草稿。我看完以后回了一句话，但现在我已经记不清原话到底是“等你们有一个算法了再发给我”，还是“等你们有一个证明了再发给我”。两句话中的一个——我真的忘了是哪句。你明白我的意思就好。至于他们后来有没有在论文里加入证明，我现在也记不清，而且我没有继续读后续版本。 **Leslie Lamport：** 有一位我很信任其判断的人读过后续版本。他的评价大意是：它基本上还是 Paxos，只是把 Paxos 论文里没有完全展开的一些细节补上了，不过描述方式非常不同。 **Leslie Lamport：** Paxos 的基本结构可以看成两个阶段，你想实现的是一串决定。算法涉及一个 leader，而且 leader 必须先被选出来。只要 leader 不变，第一阶段可以做一次之后就不再重复；接下来反复做的是第二阶段。如果 leader 失效，就需要选新的 leader，再重新做第一阶段。 **Leslie Lamport：** 所以我喜欢按“第一阶段—第二阶段”来理解它。工程师通常更喜欢反过来叙述：平时一直做第二阶段，直到 leader 失败，再回头做选举和第一阶段。甚至系统从一个全新的初始状态启动时，第一阶段需要建立的一些东西可以直接编码在初始状态里。但我还是觉得，把这两个阶段按逻辑顺序讲清楚，更有助于理解算法为什么成立。 **Leslie Lamport：** Raft 的一个宣传点是“它更简单”。很多人说 Paxos 很难理解，我一直不太明白为什么。我给一些人解释过，五分钟他们就懂了。Raft 的作者还做过教学比较：一组学生学 Paxos，另一组学 Raft，然后学生确实普遍说 Raft 更容易理解。 **Leslie Lamport：** 有趣的是，Raft 后来发现了一个 bug，也修复了。但我相信，那次比较里学生觉得更容易理解的版本，就是还带着那个 bug 的版本。这让我开始重新想“理解”到底是什么意思。 **Leslie Lamport：** 对我来说，理解意味着你能够把证明写出来；对大多数人来说，理解是一种温暖、模糊的感觉。 ## [51:00] “理解”是证明，还是一种温暖模糊的感觉 · YouTube **Leslie Lamport：** Raft 的叙述给程序员更多这种“温暖、模糊的感觉”，因为它按照程序员更习惯的顺序讲：先一直做日常的第二阶段，等出现故障再处理 leader 和第一阶段。 **Leslie Lamport：** 而我描述 Paxos 的方式，是为了让你更清楚地看到它为什么真的能够工作。这是我所说的“理解”的区别。 ## [51:26] LaTeX：从写一本书开始 · YouTube **Ryan Peterman：** 我们已经谈了你很多论文。你的另一个贡献——你当时也许没有意识到它会变成这么大的贡献——就是 LaTeX。它几乎影响了整个学术界。你当初为什么会想做 LaTeX？ **Leslie Lamport：** 这个故事很简单。我当时正准备开始写一本书，而 TeX 显然是必须使用的基础排版系统。但我觉得，要让 TeX 按我的需要工作，我得写一些宏。于是我想，只要多花一点点工夫，也许就能让这些宏不只我自己能用，其他人也能用。 **Leslie Lamport：** 在 TeX 之前，我用过一个叫 Scribe 的系统。Scribe 的核心想法很好：你描述的是文档的逻辑结构，而不是每个地方具体怎样排版，然后让系统负责格式化。Scribe 的排版效果本身并没有那么好，但我显然很喜欢这种抽象：重要的是思想、是写作本身，而不是排版细节。 **Leslie Lamport：** 后来我遇到 Addison-Wesley 的 Peter Gordon。我不太确定该怎么称呼他的职位，总之他负责寻找值得出版的书。他说服我应该为这套东西写一本书。那时候我从来没想过，居然真的会有人花钱买一本讲软件的书。不过，管他的，就写吧。 **Leslie Lamport：** 他还把我介绍给 Addison-Wesley 的一位字体/版式设计师。标准 LaTeX 样式后来呈现出来的排版设计，很大程度上是那位设计师负责的。 **Leslie Lamport：** LaTeX 基本上是我在所谓的“业余时间”里做出来的，大概花了六到九个月。我想现在追责时效应该早就过了，所以可以承认：当时我确实有些时间是在名义上给另一个毫不相关的项目记工时的时候，拿来做了这件事。 ## [54:28] 写作如何迫使思考变得诚实 · YouTube **Ryan Peterman：** 说到写作，你有一句话我很喜欢：如果你不写下来就只是在脑子里想，你其实只是“以为自己在思考”。你这句话真正想表达什么？ **Leslie Lamport：** 这句话最初主要是对构建计算机系统的人说的。你有一个想法，觉得它能工作；或者你做了一个东西，觉得别人会想用。那就先把它描述清楚。有一句老话——我也不记得从哪里听来的——是：“在写程序之前，先写使用说明书。”这是非常好的建议。 **Leslie Lamport：** 我做 LaTeX 时并没有真的一开始就先写说明书。但后来写书的过程中，只要我发现某个东西很难描述、很难解释，我就意识到那个东西本身需要改。结果因为写书，我确实改了 LaTeX 的不少地方。只是我没有从第一天就按照“先写说明书”的办法来。 **Ryan Peterman：** 为什么写作会有助于更好的思考？ **Leslie Lamport：** 因为人太容易骗过自己了。这也是我整个“写证明”观念背后的原因。我很早就学到：并发算法必须写正确性证明。后来算法越来越复杂时，我一开始还是按照自己数学博士训练中习惯的方式写证明，但很快发现那不行，细节太多，我根本无法持续追踪自己到底有没有把每件事都证明到。 **Leslie Lamport：** 计算机科学处理复杂性的一个基本办法是层级结构，所以我给证明也设计了层级结构。一个证明是一系列步骤，每一步都有自己的证明；而那一步的证明，要么就是一个段落，要么又是一组带证明的步骤。下一层还可以继续这样展开。你把整个问题不断拆成更小的部分。 **Leslie Lamport：** 这样就不会再出现“这一步到底从哪里来的？”这种模糊地带。你明确写出：这一结论来自这一步、这一步、这一步。如果它实际上不能从这些前提推出，那么你的证明就是错的。定理本身可能仍然是真的，但你的证明错了。 **Leslie Lamport：** 我先发现这种方法写程序正确性证明非常好用，后来又试着拿它写普通数学定理的证明，结果同样非常漂亮。于是我开始试着说服数学家也这样写证明。 **Leslie Lamport：** 有一次在一个小型研讨会上——具体主题我就不说了——我给大概二十位数学家展示这种证明。反应让我震惊：他们生气了。我真的觉得他们可能会对我动手。 ## [58:29] 数学家为什么会对层级化证明愤怒 · YouTube **Leslie Lamport：** 我认为那种反应完全不理性，而人不理性的时候往往是在害怕。我猜数学家害怕的是：将来他们是不是得把证明写到足以说服一个计算机程序的程度。 **Leslie Lamport：** 可我在这些演讲里已经说得非常清楚：你根本不需要比平时更“形式化”。你甚至可以写完全相同的数学内容，只是把它组织成简单的层级结构，并且在使用某个事实时明确说自己用了哪个事实。这里并没有要求你把一切变成机器形式化语言。 **Leslie Lamport：** 可那次演讲结束以后，还是有人站起来说：“我不想为了一个计算机程序去写我的证明。” **Leslie Lamport：** 而且这种方式确实更费工夫。为什么？因为它会揭露你没有说出来的东西。证明里会有一些步骤，你可能觉得“这不是显然的吗”，但你其实从没把它写下来。 **Leslie Lamport：** 如果你以为自己知道一件事，却不把它写下来，那你只是以为自己知道。错误就是从这些地方钻进来的。源字幕接下来还有一句转写成类似“你论文里三分之一的错误会从这里进来”，这句话的具体措辞不够可靠，但我想表达的核心很明确：写下来会逼你诚实面对自己真正说清了什么、又遗漏了什么。 ## [1:00:02] 为什么没有走学术路线 · YouTube **Ryan Peterman：** 回头看你的职业生涯，你做了很多人可能会以为来自大学的工作——论文、理论结果等等——但实际上你的整个职业生涯都在工业界。为什么你没有把自己看成一个学者，而是一直选择在产业里工作？ **Leslie Lamport：** 我最开始就是写程序，后来得到了一些工作，逐渐把我带进今天所谓的计算机科学。起初我甚至没有意识到，计算这件事本身还能有一门“科学”。 **Leslie Lamport：** 大概要到字幕转写成“mid to late '7s”的那个时期，我才真正意识到：对，确实存在计算机科学，我也可以被叫作计算机科学家。这段年份字幕有缺字，我的意思显然是在说一个更早的职业阶段，但我不在这里擅自补成精确年份。 **Leslie Lamport：** 可即便如此，我当时也从没觉得计算机科学天然就是一门大学里的学科。有一段时间我得在两条路之间选：一条是继续做当时还未必叫“计算机科学”的计算工作，另一条是去大学教数学。因为一些相当随机的原因，我选了前者。 **Leslie Lamport：** 一直到大概 80 年代中期，我仍不太觉得计算机科学是那种“必须去大学才能学”的东西。后来再回头想，也许更简单的原因只是：我觉得教计算机科学不会那么有趣。 ## [1:01:49] 并发的“图灵机”、状态机与无限 · YouTube **Ryan Peterman：** 我在你的文字里看到过一个脚注：你有一段时间把自己看成某种失败者，因为你曾经想发展出一个宏大的并发理论，却始终没有发现它。你现在还这么觉得吗？ **Leslie Lamport：** 当年做和我类似事情的人本来就不多，但其中很大一部分人都有一种愿望：找到“并发的图灵机”。图灵机是一种抽象，它非常深刻地抓住了“计算是什么”，所以大家希望为并发计算找到同样基础、同样统一的抽象。 **Leslie Lamport：** 没有人真正成功。当然，也有人认为自己成功了。源字幕把一个当时很流行、70 年代很大的方向转写成 “patronets / patriets”；这里应是一个专门的并发模型名称，我把具体拼写留到待核对。我后来甚至有点惊讶，发现今天仍有一个很大的社群在做这类工作。 **Leslie Lamport：** 我现在意识到，这类工作以及很多类似方向，本质上都以“语言”为中心。而我从来对语言本身没有兴趣。我感兴趣的是语言究竟在表达什么。 **Leslie Lamport：** 从这个角度说，也许我最终还是找到了并发计算的“图灵机”：状态机。现在我描述状态机甚至比早年更简单——它不需要“命令”这个概念，只需要一个状态，以及一个 next-state relation，也就是“下一个状态可以是什么”的关系。这比谈命令、返回值之类还要抽象。 **Leslie Lamport：** 对我来说，这就是并发的基础抽象。不过它和图灵机还有一个重要差别：图灵机帮助刻画什么是“可能计算的”，而状态机能够描述任何东西，甚至包括现实中无法实现的东西。这个差别其实是有意而且有用的。 **Leslie Lamport：** 举个例子，描述一个算法时，我可以说某个变量的值可以是任意整数。真实计算机显然不可能真的存下任意大的整数，但如果一开始就把讨论限制成机器整数，描述反而会无谓地复杂很多。 **Leslie Lamport：** 人们有一个很奇怪的想法，好像东西一旦是无限的就更复杂。完全反了。无限是为了让事情变简单才被引入的。你最早学的算术，就是在无限多个整数上做算术；如果硬把整数限制成一个有限集合，算术反而会复杂得多。 **Leslie Lamport：** 数学里的这些抽象，有些人因为数学训练不足而觉得困难，但它们实际上是在简化问题。对我来说，状态机就应该用数学来描述；那是最合适、也是最强大的描述方式。 ## [1:05:50] 程序语言与数学：理解问题时你打不过数学 · YouTube **Leslie Lamport：** 但计算机从业者、计算机科学家和程序员往往非常迷恋“语言”。他们不断发明各种语言。可所有这些语言最终都可以被描述；如果你要给它们一个语义，也完全可以用状态机来定义。 **Leslie Lamport：** 人们有时觉得换一种语言就会改善自己的思考。我不这么认为。当然，我们有充分理由使用计算机语言，而不是直接用数学来写可执行代码，那些理由主要和实现效率有关。 **Leslie Lamport：** 可如果目标是理解，你赢不了数学。你不能靠一个看起来更像编程语言的东西取代数学，然后期待它自动让并发问题更容易理解。对并发来说，我认为那是走错了方向。 ## [1:07:05] 他为什么从不觉得自己“聪明” · YouTube **Ryan Peterman：** 看你的文章和这些故事，会不断看到一些小片段：你说自己从来没有觉得自己很聪明，但你又会注意到别的孩子理解某些事情非常困难；或者别人卡在一个问题上，你解决了，却不把自己的贡献看成什么“天才之举”。这和我看到的你很难拼在一起，因为你又拿了图灵奖，做了这么多重要工作。怎么会一边只是觉得自己“发现了点东西”，一边又取得这些成就？ **Leslie Lamport：** 心理学里常说的一种现象是：一个人如果很擅长某件事，反而不一定意识到自己有多擅长，因为那件事对他来说就是很简单。反过来也一样：不擅长某件事的人，可能反而高估自己，因为他正是因为不擅长，才看不出自己的不足。 **Leslie Lamport：** 更简洁地说：笨的人觉得自己聪明，因为他们笨到意识不到自己其实并不聪明。 **Leslie Lamport：** 我的天赋从某种意义上说不是原始智力，而是抽象。直到最近——大概过去十年左右——我才真正意识到，自己在抽象这件事上比大多数人强多少。 ## [1:08:51] 给年轻自己的建议：别回答不必回答的问题 · YouTube **Ryan Peterman：** 你已经经历了这么多。如果现在回看职业生涯，可以回到刚大学毕业的自己面前，用今天知道的事情给他一个建议，你会说什么？ **Leslie Lamport：** 我很早就学到一件事：不要浪费时间去回答那些我根本不必回答的问题。我不会一直想“当年我本来应该怎么做”，因为那就是一个我没有必要回答的问题。 ## [1:09:25] 片尾：播客、人体工学键盘与听众反馈 · YouTube **Ryan Peterman：** 谢谢你收听这个播客。它是我的一个热情项目，我很享受把它一点点做出来。最近我还在有点秘密地做另一个热情项目：一把我一直希望市面上存在的人体工学键盘，现在终于已经有原型了。 **Ryan Peterman：** 我很想让你看看我们做出来的东西。它非常薄，是超低矮设计，也强调人体工学。我在市场上找不到类似的产品，所以我们干脆自己做了。我会把键盘链接放在简介里，你可以去看看，了解更多项目情况。我们也确实很需要大家的支持。 **Ryan Peterman：** 如果你对节目有任何反馈，我也很想听。YouTube 评论曾经直接促成一些嘉宾上节目，比如字幕转写成 “Ilia Gregoric” 的嘉宾以及 David Fowler；在有人留言之前，我甚至不知道他们。 **Ryan Peterman：** 评论里的反馈还让我学会减少开场里字幕转写成 “cliffhers” 的那些东西——从上下文看，是指过多的悬念式、吊胃口式开场。总之，你们的评论真的会改变节目。请继续告诉我你希望节目多做什么，我们下一期见。