莱斯利·兰波特是一位美国计算机科学家，以对分布式系统理论和实践的基础性贡献而闻名。他获得了2013年图灵奖，其工作包括发明LaTeX文档准备系统和提出动作时序逻辑（TLA）。他的思想支撑着现代云计算、并发编程和形式化验证。
兰波特出生于纽约布鲁克林，在麻省理工学院学习数学，于1960年获得学士学位。他分别于1963年和1972年在布兰迪斯大学获得硕士学位和数学博士学位。他在1970年代于马萨诸塞计算机联合公司工作时，早期研究转向计算机科学，并开始研究仅通过共享消息传递进行通信的进程协调问题。
分布式系统与面包店算法
兰波特最早的主要贡献是1974年发表的面包店算法，这是一种多进程互斥协议。它为每个进程分配一个票据编号，并确保进程按票据顺序进入临界区，即使没有原子读-修改-写操作也能实现互斥。这项工作解决了并发编程中的基本挑战，当时竞态条件和数据损坏问题十分普遍。该算法至今仍是操作系统课程中的教学重点。
他后来在1978年的论文《时间、时钟和分布式系统中事件排序》中形式化了逻辑时钟的概念，引入了基于因果关系（发生于之前）的事件偏序。这使得分布式系统无需依赖物理时钟即可同步，从而实现一致的状态复制。这篇论文成为计算机科学中被引用最多的论文之一，影响了数据库、文件系统和云基础设施的设计。
Paxos与共识协议
兰波特、罗伯特·肖斯塔克和马歇尔·皮斯于1982年提出的拜占庭将军问题，定义了系统组件如何在部分节点故障或发送冲突信息的情况下达成一致。兰波特的解决方案，即拜占庭容错算法，为可靠性设定了基准。他随后在1989年开发了Paxos共识协议，该协议允许分布式网络在故障情况下就单一值达成一致，是复制状态机的基石。
Paxos支撑着许多现代分布式数据库和服务，包括谷歌云和微软Azure的服务。兰波特以用一个虚构的希腊岛屿立法机构的寓言来介绍Paxos而闻名，他后来承认这种教学风格使其采纳变得复杂。该协议的实际实现已经演变，但其理论框架仍是标准。
LaTeX文档系统
1970年代末，在SRI国际工作期间，兰波特创建了LaTeX，作为唐纳德·克努斯TeX排版引擎之上的一组宏。他设计LaTeX旨在将内容与呈现分离，让作者专注于结构，而系统处理格式。其首个主要版本于1985年发布，并迅速成为数学、物理学和工程学学术出版的事实标准。
LaTeX支持自动编号、交叉引用和参考文献管理，并提供大量用于专业任务的包。自1986年以来，由一个开发团队维护，其在预印本库和期刊中的广泛使用使其成为学术交流的固定组成部分。兰波特本人撰写了最初的使用指南，该指南至今仍是参考。
动作时序逻辑（TLA+）
从1990年代起，兰波特专注于形式化验证。他开发了动作时序逻辑（1999年称为TLA+），这是一种用于描述和推理并发及反应系统的规范语言。TLA+使用数学逻辑来建模系统状态及状态之间转换的动作，使工程师能够在实现前证明不变量和安全属性。
TLA+已应用于实际分布式协议，包括施乐帕洛阿尔托研究中心和NEC的协议，并影响了亚马逊内部分布式系统的设计。兰波特还创建了PlusCal算法语言，该语言可编译为TLA+，使形式化方法对从业者更易用。他2013年的图灵奖引文赞扬了他在实践和理论两方面的贡献。
奖项与遗产
除图灵奖外，兰波特还获得了2004年IEEE Emanuel R. Piore奖、2005年Dijkstra奖（因Paxos协议共同获得）和2014年ACM SIGOPS Mark Weiser奖。他于1991年入选美国国家工程院，并于1992年成为计算机协会会士。他关于并发和分布式系统的论文塑造了课程和工业实践。
兰波特曾在马萨诸塞计算机联合公司、SRI国际、数字设备公司和康柏工作，于2001年加入微软研究院，至今仍担任首席研究员。他继续倡导严格的软件规范，其影响遍及操作系统、数据库理论和编程语言。
个人生活与影响
兰波特出生于1941年，在布鲁克林长大。他提到数学家和逻辑学家艾伦·图灵是自己的思想灵感来源。他以机智著称，发表了关于数学和计算机科学的幽默文章，包括《并发计算机科学：早期岁月》和一篇抨击“分布式系统”一词误用的文章。他的格言“分布式系统是一种你不知道其存在的计算机故障就能使你的计算机无法使用的系统”被广泛引用。
兰波特继续在全球讲学，并为验证工具的设计做出贡献。他的工作连接了理论抽象与工程实践，形式化方法社区和整个软件行业都将他视为奠基性人物。
category:computer-science category:distributed-systems category:formal-methods category:typesetting