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 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
Here are links to the two videos and to accompanying material,
which is contained in a
Lecture 1 Lecture 2 Accompanying MaterialThe accompanying material consists of the specs described in the lectures and follow-up exercises you can do after watching the videos. The file