The Paxos Algorithm
or How to Win a Turing Award

Leslie Lamport

Last modified on 16 October 2024

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:
  • The Paxos consensus algorithm.
  • TLA+
  • How to win a Turing award.
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 lectures assume no prior knowledge of the Paxos consensus algorithm or of TLA+, the language in which the specifications are written.  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 in the .pdf files.  I hope that you will eventually appreciate the elegance and precision of the TLA+ specs.

Here are links to the two videos and to a zip file containing the slides for the talk in three pdf files: 

    Lecture 1       Lecture 2       Slides
There is also accompanying material consisting of the TLA+ specs described in the lectures and follow-up exercises you can do after watching the videos.  The file README.txt contains instructions for the exercises.  Here is a link to a zip file containing this material: 
    Accompanying Material