The Writings of Leslie Lamport (abridged)
If you’ve ever done even half-serious work on consensus algorithms, then you will know that Leslie Lamport is a central figure. Paxos, Byzantine Generals, TLA — if any of these are familiar to you, well, Lamport is behind them. (And LaTeX too!)
What follows is papers and nuggets from his homepage, biased to blockchain relevance. I preserve the numbers from his page. It’s as much for my own reference as anything:)
30. SIFT: Design and Analysis of a Fault-Tolerant Computer for Aircraft Control, 1978. PDF
The origin of the Byzantine generals problem and its solutions, reported in [41].
27. Time, Clocks and the Ordering of Events in a Distributed System, 1978. PDF
If you can order input requests, then you can implement an arbitrary distributed state machine. This paper describes how.
41. Reaching Agreement in the Presence of Faults, 1980. PDF
The first time the consensus problem was stated, and Byzantine consensus problem too. With a solution algorithm, albeit exponentially expensive. You need 3n+1 processors to tolerate n faults, but with digital signatures, just 2n+1. The digital signatures can be simpler than the fancy crypto ones we think of today.
46. The Byzantine Generals Problem, 1982. PDF
A better description of the solution to the Byzantine consensus problem. Also the origin of “Byzantine” (for better or for worse!).
50. Specifying Concurrent Program Modules, 1983. PDF
The beginnings of TLA.
How do you write temporal logic specifications? (Where a “specification” is what it means for a system to be correct in a formal way.) The initial ideas were to write a specification as a set of temporal properties, but that didn’t work so well. What did work was to describe a state transition as a boolean-valued function. Maybe obvious in retrospect, but not at the time. BTW that’s a sign of a great invention if you ask me! Paper [102], years later, follows up.
55. Using Time Instead of Timeout for Fault-Tolerant Distributed Systems, 1984. PDF
The state machine approach [27] means we can convert any consensus algorithm into a general method for implementing distributed systems. Therefore the BFT algorithms of [46] are fault-tolerant implementations of arbitrary distributed systems!
69. LaTeX: A Document Preparation System, Addison-Wesley, 1986.
Leslie wrote TeX’s first macro, and LaTeX was born. Leslie kept making it better. Wow.
82. A Simple Approach to Specifying Concurrent Systems, 1989. PDF
A more accessible description of TLA [50].
101. How to Write a Proof. PDF
To write a proof, use TLA. Nuff said.
102. The Temporal Logic of Actions. PDF
Introduction of TLA. Use a programming language to program, but not to specify an algorithm. For that, use TLA.
107. Specifying and Verifying Fault-Tolerant Systems, 1994. PDF
The BFT proof [51], in TLA.
122. The Part-Time Parliament, submitted 1990, published 1998 (!). PDF
Paxos: fault tolerant consensus. (Not BFT, just FT.)
Described in hard-to-understand way, to say the least. Much confusion ensues.
139. Paxos Made Simple, 2001. PDF
Paxos [122] described in an easier-to-understand way.
158. Fast Paxos, 2006, LINK
Default Paxos [122] has three message delays. Here, it goes with two unless three are needed.
173. Byzantizing Paxos by Refinement, 2011. PDF
Castro and Liskov’s PBFT was the first practical way to do BFT. Lamport sees it as a modification to Paxos [122]: 2n+1 non-faulty processes are trying to implement non-BFT Paxos in the presence of n malicious processes.
174. Leaderless Byzantine Paxos, 2011. PDF
Better BFT by eliminating the leader.
[Added May 2022]
Here’s a great article about Leslie Lamport: “How to Write Software With Mathematical Perfection”, Quanta Magazine, May 2022. Link.
Leslie Lamport revolutionized how computers talk to each other. Now he’s working on how engineers talk to their machines.
