记2013年图灵奖得主、微软科学家莱斯利...
【题】记2013年图灵奖得主、微软科学家莱斯利·兰伯特
【出处】《中国计算机学会通讯》第10卷第5期 2014年5月刊
【说明】本文由微软亚洲研究院公关部实习生王雅编译
莱斯利·兰伯特 (Leslie Lamport)在读高中时就已经涉足计算机科学领域，这乍一听没有什么了不起 —— 但你要知道，那是 20 世纪 50 年代中期。当时兰伯特就读于纽约的布朗士科学高中，他和一个朋友四处“捡破烂”——通过搜寻废弃的真空管来搭建数字电路。
在随后的几十年间，他逐渐成为计算机领域名副其实的传奇人物。他在 1978年发表的论文《分布式系统内的时间、时钟和事件顺序》(Time, Clocks, and the Ordering of Events in a Distributed System)成为计算机科学史上被引用次数最多的文献。兰伯特为“并发系统的规范与验证”研究贡献了核心原理，他的分布式计算理论奠定了这门学科的基础。
3 月 18 日，为表彰兰伯特对这些宝贵的进步所作出的杰出贡献，美国计算机学会 (ACM) 将 2013年度图灵奖颁发给他，这一殊荣被看作计算机领域的诺贝尔奖。73 岁的兰伯特是微软研究院第 5 位荣获图灵奖的科学家。
尽管兰伯特的学术生涯充满了众多令人称道的成就，兰伯特对自己的评价却十分谦逊，“我并不太善于寻找解决方案，但我确实很善于提出问题。”不过在了解他的人当中，很少有人会同意这个说法。
比尔·盖茨这样评价兰伯特 ：“作为一名带头人，他界定了分布式计算的许多关键概念，并让今天执行关键任务的计算机系统成为可能，兰伯特的伟大不仅仅局限于计算机科学领域，而且还体现在努力让世界变得更加安全。”同样来自微软研究院的 1992年图灵奖得主巴特勒·兰普森 (Butler Lampson) 对他的评价也很高 ：“兰伯特对并发系统理论和实践在质量、范围和重要性上的贡献都是难以超越的。它们完全可以和迪克斯特拉(Dijkstra)、霍尔(Hoare)、米尔纳 (Milner)和伯努利 (Pnueli)等所有图灵奖得主前辈的成就相提并论，但他最大的优点是作为一名应用数学家，擅长利用数学工具来解决具有非凡现实意义的问题。”
时间、时钟和相对论
这项重要成果源于 1978 年他广有影响力的论文《分布式系统中的时间、时钟和事件顺序》的发表。文章介绍了有关分布式计算、同步和异步实体之间通讯的原则性思维新途径。它在当时令人耳目一新，后来成为各种并发系统行为推理的基础，是一篇开山之作。
当时，兰伯特正在 Compass公司任职，他为罗伯特·托马斯 (Robert Thomas)和保罗·约翰逊(Paul Johnson)共同撰写的论文《复制数据库的维护》(The Maintenance of Duplicate Databases)作序。这篇论文认为，对于两个完全相同的数据库，如果其中之一发生改变，那么对它们更新时就需要用到时间戳(timestamp)。而在看完论文后，兰伯特发现，“它没有保留因果关系。尽管事件按照完成时间的顺序出现在系统中，但其在逻辑上并不与命令发出的顺序相一致。我意识到，如果改变时间戳的产生方法，这个问题可能很容易得到解决。”
兰伯特对问题的洞察力源自他对物理学和狭义相对论的兴趣。他意识到，确定两个事件在时间顺序上存在问题，除非两者之间有因果联系 —— 也就是说，除非它们之间传递过信息。他由此认识到，如果这种信息的时间戳可以用来确定事件的顺序，则该系统中发生的所有事件都可以按单一顺序排列。推而广之，一个计算系统内的任何事物都可以用状态机来描述（状态机保持着特定状态，接收输入后产生一个输出，同时改变其自身的状态）。兰伯特推论，这个概念可以适用于更加复杂的系统，如银行或航空票务预订。
面包店算法
兰伯特在 Compass工作期间的另一个成果是在《迪克斯特拉(Dijkstra)并行编程问题新解》一文中提出的面包店算法。该算法旨在解决互斥问题 ：排除多个线程试图对相同存储位置写入时发生数据损坏的现象，以及在一个线程完成对特定位置写入之前另一个线程无法读取该位置的现象。其名称暗指面包店常用的排序系统 ：客户在进入店面时需要选择一张有编号的票。
兰伯特回忆道：“我还在 Compass工作时，在《美国计算机学会通讯》(CACM) 上读到一篇关于互斥算法的论文，这是我第一次接触互斥问题。我读完文章后，觉得这似乎并不十分困难。”于是，他编写了一个快速算法，并将其撰写成简短论文寄给刊物编辑，后者立即回复并解释了兰伯特的算法行不通的原因。
这件事给了他一个提醒，他意识到他不应该只编写并行算法，而不去验证其正确性。这促使他回过头来彻底解决了这个问题。时至今日，他仍然对自己在面包店算法上的成就感到自豪，“我感觉自己发现了一个算法，而不是发明了它。”
拜占庭将军
离开 Compass后，兰伯特加入了美国斯坦福国际研究院 (SRI)。在此期间，他和同事马歇尔·皮斯 (Marshall Pease) 及罗伯特·肖斯塔克 (Robert Shostak) 合作完成了两篇旨在解决“拜占庭故障”(Byzantine failures)的论文。
当时斯坦福国际研究院有一个项目，目标是为美国航空航天局建立容错型航电计算机系统 (fault - tolerant avionics computer system)。这种系统要求不允许发生故障。一般说来，“普通”故障可能会导致信息丢失或过程停止，但它们不会遭到损坏—— 即便遭到损坏，也能通过利用冗余来丢弃损坏的信息。即便过程停止，也不会给出错误答案。然而，“拜占庭故障”却可能犯错误，或给出错误信息。
当时常用的技术是“三重模块冗余 (triple modular redundancy)”，使用三个独立的计算机按照某种少数服从多数的原则“投票”，即使其中一台机器提供了错误答案，其他两台仍然会提供正确答案。但是为了证明其有效，必须拿出证据。在编写证据过程中，研究人员遇到了一个问题：“错误”计算机可能给其他两台机器分别发送不同的错误值，而后者却不知道。这就需要使用第四台计算机来应对这个故障。
兰伯特说：“如果你使用数字签名就可以用三台机器达成目的，因为如果‘错误’计算机向一台计算机发送了带签名的错误值，并向另一台发送了不同的带签名错误值，后两台计算机就能够交换消息，以检查究竟发生了什么情况，因为两个不同的值都是签名发送的。”
在一个朋友的启发下，兰伯特联想起拜占庭帝国军队中“司令将军和叛徒将军”的问题，于是他将这个问题及其解决方案命名为“拜占庭将军问题”。
希腊喜剧
微软硅谷研究院院长莱文 (Levin) 介绍道 ： “兰伯特的应对故障计划所涉及的是分布式计算研究的一个重要领域，他的工作是基础性的。后来又延伸至 Paxos 算法。现在，Paxos 算法已经成为现代分布式系统中的一项重要技术。如果没有以 Paxos 或非常类似的技术为核心，就不会有人想去建立一个具有鲁棒性的、可靠的大型分布式系统。”
兰伯特的论文《兼职议会》(The Part-Time Paliament) 通过希腊神话中一个岛屿及其立法机构的类比解释了Paxos算法。他说 ：“我尝试添加一些幽默气氛。还是老问题 ：借助状态机来处理存在的故障。在这种情况下，状态机像是需要通过一系列法律的议会。所不同的是，我们的目的不是处理‘拜占庭故障’，而是处理普通、简单的故障，只不过在异步环境下进行。我们并非处理恶意失败，有些是单纯的工程问题，所以我懒得去探究，于是就简单地说：‘考古记录并未说明他们究竟是如何做到这一点的。’在另一个案例中，为了说明如何进行特定优化，我引用了一个奶酪商人的故事，说明如何使之更有效率。在所有的故事中，我都给人物取了希腊人的名字，以伪希腊语写作，并借用计算机科学家的音译姓名。案例中的奶酪商人名为高达(Gouda)，实际上借用的是一位计算机科学家穆罕默德·高达 (Mohamed Gouda)。”
“论文的结论是，可能会发生一些导致系统崩溃的事件。你可以利用系统来自我重新配置，但是如果你稍有疏忽，就可能会遇到一种情况 ：议会无法再通过更多的法律。在故事中恰恰发生了这种情况，而一个名叫兰普森 (Lampson) 的将军便接管政权，成为独裁者。”
然而，兰伯特没想到他的好友巴特勒·兰普森是最初唯一读懂了故事的人，并意识到这是一篇讨论如何构建分布式系统的论文。或许在一定程度上由于他所选择的这个比喻，这篇论文的实际内容在相当长一段时间没有得到重视。
论文的最终发表已经是 10年后的事情，而且经过增补，纳入了对干预方法的思考。兰伯特后来写了一篇题为《Paxos化繁为简》(Paxos Made Simple) 的文章来解释算法的简洁性——而且没有借用希腊文字游戏。随着时间的推移，人们逐渐认识到这项工作是一个真正的进步。
抽象的正确性
兰伯特引入了安全和活跃度两种概念，以概括并发系统的部分正确性和终止的特征。安全是指一个系统中没有发生任何不好的事情，而活跃度则指有好事发生。
兰伯特说 ：“我引入安全和活跃度概念后不久，埃米尔·伯努利(Amir Pnueli)（1996年图灵奖获得者）展示了如何使用时序逻辑对程序进行推理。你可以用相同的逻辑来表述程序及其属性。对正确性的检验就简化成观察一个程序是否在逻辑上暗合其规范。埃米尔·伯努利原先的逻辑只使用了一个时间运算符：始终 (always)，有些事情‘始终’是真的。人们加入了不同的复杂时序运算符，例如‘直到某些事情为真’或‘直到其他一些事情为真’。”这使得事情变得尾大不掉，且难以理解。
而兰伯特却另辟蹊径，他说：“我有一个很好的方法，可以坚持使用单一的运算符，但是要对运用于该运算符的基本非时序方程式加以变革。我没有使用只关注单一状态的基本方程，而是加入了关注一对状态 —— 当前状态和未来状态的方程。通过加入关注两种状态的方程，我就能够描述一台在这个逻辑下工作的状态机。如果我能够描述这个逻辑下的状态机，就可以把活动度属性描述成为时序方程式，进而就可以把整个程序或整个规范描述成为一个单一方程式 —— 一个真正能够工作的方程式。这就是行为时序逻辑(temporal logic of action, TLA)。”
行为时序逻辑是 TLA+ 规范语言、PlusCal 算法以及与之相关工具的基础。兰伯特在 2002 年出版的专著《规范系统：硬件和软件工程师的TLA+语言及工具》(Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers) 中对行为时序逻辑和 TLA+ 做出了解释。其基本原则是，正式描述事物的最好办法就是用简单的数学。其推论是 ：除了精确编写简单数学算式所需的工具外，一个规范语言应尽可能少地包含其他内容。
兰伯特现任职于微软硅谷研究院，在他看来，在企业研究院做学术研究有着独特魅力。他说：“我喜欢在一个企业研究院里工作，因为我能跟不同的人在一起，充分地接触到各类现实的问题。如果单靠自己提出问题，我只能拿出很少的东西，但如果我去外面的世界，那里的人们正在努力打造真正的计算机系统，会有 100 万个问题等着我。我回顾自己的大部分工作，比如拜占庭将军问题、Paxos 等，都是来自现实世界。”
在兰伯特看来，微软研究院带给他的最大财富是一群与他朝夕相处的研究员和来自产品部门的工程师们。他说 ：“微软整个企业对研究的态度与我曾任职的其他任何地方都不一样。微软能够意识到是研究人员贡献了研究理念。公司能做的就是在研究人员和工程师之间架设沟通渠道，让工程师知道研究人员正在做什么，而研究人员也能知道工程师面临的问题是什么。微软建立了项目经理系统，并且将其作为一种常设机制来实现这一点。”
微软的产品组曾多次获益于兰伯特的专业知识。他的 Paxos 研究成果已经在多个产品中使用，其中包括 Windows Azure存储、Azure的 REST可用性代理 (rest availability proxy)和 Cosmos数据存储及查询系统。他还对 Windows 服务器事务协议(transaction protocol)的正确性作出了贡献，而且针对模型驱动应用的奥斯陆平台(Oslo platform)的构筑灵感也来自他在行为时序逻辑的研究。此外，微软公司的许多工作人员都曾从兰伯特一手创建的LaTeX系统中获益。
尽管被授予素有计算机领域诺贝尔奖之称的图灵奖，兰伯特却并不认为他攀上了学术生涯的顶峰。他觉得能够持续地为计算机研究工作，才是他事业的巅峰状态。作为一位拥有辉煌履历和至高荣誉的研究者，兰伯特分享了他关于研究的点滴体会：“选择合适的问题，并为此努力找到好的解决方案。”
（完）
留下你的评论