图灵奖牛人LeslieB. Lamport介绍
英文原文链接https://en.wikipedia.org/wiki/Leslie_Lamport
Leslie B. Lamport，生于1941年，美国著名的计算机科学家，以发明分布式关键技术（特别是PAXOS）、LATEX、TLA+知名，于2013年获得图灵奖。他1960年在MIT获得数学学士学位，1972年从Brandeis大学获得数学Ph.D，1970~1977在Massachusetts Computer Associates从事计算机科学研究，1977~1985就职于SRI International，1985~2001就职于DEC和Compaq，2001~2014就职于Microsoft Research in Mountain View（加州，2014年微软关闭该分支机构），之后在Microsoft Research in Redmond（华盛顿州）。在整个职业生涯，发表了许多经典论文，特别是如下被广泛引用的分布式领域奠基性文章：
n 1978年发表“Time, Clocks, and the Ordering ofEvents in a Distributed System”,该文章在2000年获得了PODC Influential Paper Award（重大影响论文奖）。稳重提出了分布式领域的关键技术：happen-before（事件的先后）、partial order（偏序，关联事件的顺序）、total order（全序，所有事件保证顺序）、logical clocks（类似全局系列号）、physical clocks（比如基于GPS的全局时钟，GOOGLE SPANNER利用GPS思想就可从此论文找到依据）、state machine（首次提出基于状态机的算法）。
n 1979年发表“How to Make a MultiprocessorComputer That Correctly Executes Multi-process Programs”,提出了Sequential consistency技术,为后续定义不同的Consistency model提供了基础。
n 1982年发表“The Byzantine Generals‘ Problem”,提出了在分布式不可信环境下（也即是分布式节点有Byzantine错误），保证2/3的将军可信才能保证系统的可用性，这是PAXOS的基础。
n 1984年发布“Time Instead of Timeout forFault-Tolerant Distributed Systems”，基于时间驱动的状态机算法（GOOGLESPANNER中的时间和误差可从此论文找到依据）。
n 1985年发表“Distributed Snapshots: DeterminingGlobal States of a Distributed System”，提出了State MachineReplication复制状态机的早期概念。
n 1998年发表“The Part-Time Parliament”，综合前期的研究成果，提出了PAXOS算法早期版本，搭建了分布式系统最为坚实的理论基础。
自此之后，基于PAXOS发表了一系列的论文（参考http://paxos.systems/variants.html介绍）：
n 2002年发表Disk Paxos
n 2003年发表Cheap Paxos
n 2004年Fast Paxos
n 2005年Generalized Paxos
n 2008年Stoppable Paxos
n 2009年发表Vertical Paxos
从理论上证明了PAXOS的正确性，并且Google的Chubby论文从产品层面给出了验证，从而让分布式技术在各领域得以广泛应用。
除了在分布式领域进行了大量的研究工作外，Lamport还发明了TLA+（TemporalLogic of Actions），它是在图灵奖获得者Amir Pnueli发明的Temporal Logic基础上进行的改进；它能根据分布式算法的状态机，检查该算法的正确性，该工具被Amazon、Microsoft、Raft等广泛适用。
Lamport先生是醉心研究的人，尽管取得了如此众多的丰硕成果，他在微软仍然坚持做研究，目前还是Principal Researcher。
为牛人致敬！
Lamport研究成果重要链接：
http://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html
https://www.microsoft.com/en-us/research/people/lamport/