Leslie Lamport on the Science of Distributed Systems

Leslie Lamport defines the core problem of distributed systems as getting multiple processes to all be doing the same thing, and argues there is no fundamental difference in how one reasons about distributed versus non-distributed concurrent algorithms. His interest in concurrency traces to 1972, when he read a mutual exclusion algorithm in CACM that struck him as unnecessarily complicated. The mutual exclusion problem had been originally posed by Edsger Dijkstra, whom Lamport credits with starting the modern study of concurrency.

Lamport's first attempt at a simpler two-process mutual exclusion solution contained a bug identified by a CACM editor, and that experience convinced him concurrency is tricky and requires formal correctness proofs. The bakery algorithm emerged from his effort to fix that problem, and he says that for two or three years afterward, everything he worked on followed directly from it. Work on proving correctness of multiprocess programs began around 1975, and he published a correctness proof of a distributed algorithm approximately in 1978, though he says it took him until about 1990 to fully understand what correctness of a protocol truly means.

Lamport considers the most important contribution of his time clocks paper to be the introduction of state machine replication rather than the logical clocks themselves. A state machine takes a state, receives commands, produces outputs, and changes state, and implementing one correctly in a distributed setting allows you to implement anything. He also realized the time clocks paper algorithm fixed a causality violation in a prior distributed database consistency algorithm where commands could execute out of order relative to submission order. Tim Roughgarden notes that state machine replication is central to modern blockchain protocol design, and that systems like Ethereum and Solana can be viewed as aspiring to solve the general version of that problem.

After the time clocks paper, Lamport says adding fault tolerance was an obvious next step because computers in a distributed system will fail. For Byzantine fault tolerance he initially assumed digital signatures, which he learned about from Whitfield Diffie, whom he describes as a friend and co-founder of civilian cryptography. Lamport wrote a simple digital signature algorithm on a napkin at a coffee house in Berkeley around 1976. With digital signatures, Byzantine fault tolerance requires 2N plus 1 computers to tolerate N faults; without digital signatures, 3N plus 1 are required. Airplane builders chose the 3N plus 1 approach because they considered digital signatures impractical, a decision Lamport disagreed with for non-malicious random failure scenarios. Marshall Pease discovered the general N-process Byzantine fault tolerance algorithm, which Lamport described as amazingly brilliant and very difficult to understand, and Lamport later found a recursive description that made it comprehensible, one Pease himself had not used.

Paxos originated when Lamport tried to write an impossibility proof at Digital's System Research Center and ended up with an algorithm instead. The impossibility problem it relates to is the Fisher Lynch Patterson result, which shows a certain problem cannot be solved without the use of clocks. Paxos gives up liveness in principle but maintains safety, making it highly unlikely in practice that computers will fail to reach a decision indefinitely. Butler Lampson was one of the few who initially understood the significance of the Paxos paper and went around popularizing it. Lamport withheld the paper from publication after referees told him to remove the Paxos narrative, then published it with that content once its importance became clear. The abstraction at the core of Paxos, where a majority of legislators inside a chamber with synchronous communication enables liveness, is now used by almost all distributed systems.

Lamport viewed concurrency as more of a physics problem than a language or mathematical problem, citing mutual exclusion and the concept of same time as inherently physical. He argues that solving mutual exclusion by inventing a language construct was not actually solving mutual exclusion. He credits working at an industrial research lab with exposing him to problems from engineers and programmers he would not have encountered in academia, using a Jean Renoir analogy about painting outdoors versus in a studio to explain why proximity to real systems produces richer problems. He developed TLA plus to help system designers think more abstractly about concurrent programs, and says very good engineers who use it improve their ability to abstract and become better designers. His upcoming book, A Science of Concurrent Programs, targeted for publication in March by Cambridge University Press, consolidates the theory behind stating correctness properties precisely and showing mathematically that algorithms satisfy those properties.

Byzantine fault tolerance research was pushed by DARPA out of concern for survivability of large-scale systems against attacks and failures, and that technology is now being applied for economic purposes in blockchain. Paxos from Lamport and viewstamped replication from Liskov converged on similar ideas around the same period, illustrating how the right moment enables ideas to emerge independently. There is a prediction that survivability of systems may become very important again, potentially drawing blockchain technology back toward those original government-focused concerns.