The Paxos Algorithm
or How to Win a Turing Award
Last modified on 23 August 2019
In July 2019 I gave a pair of 1-1/2 hour lectures at a summer
school on distributed computing in Saint Petersburg, Russia.
The lectures covered three topics:
If you are interested in any of those topics, you might want to watch
the videos of the lectures. In them, I present a rigorous
development of the Paxos consensus algorithm that formalizes the
thinking I believe led me to discover it. I explain the
algorithm with three specifications: a trivial one stating what the
algorithm is supposed to accomplish, a high-level algorithm in which
each process directly views the state of every other process, and the
actual algorithm in which processes communicate by sending messages.
- The Paxos consensus algorithm.
- How to win a Turing award.
The lectures assume no prior knowledge of the Paxos consensus
algorithm or of TLA+, the language in which the specifications are
In fact, the lectures constitute a crash course on TLA+.
If you're interested just in the algorithm, you will probably find the
specs annoying and will try to read only the plentiful comments,
ignoring the TLA+.
To understand the algorithm, you will have to stop the
video at certain points and read the specs—either the ASCII
sources in the
.tla files or the pretty-printed versions
.pdf files. I hope that you will eventually
appreciate the elegance and precision of the TLA+
Here are links to the two videos and to accompanying material,
which is contained in a
zip file that you should download:
Lecture 1 Lecture 2 Accompanying Material
The accompanying material consists of the specs described in the
lectures and follow-up exercises you can do after watching the videos.
README.txt contains instructions for the