Paper 48: Paxos and TLA+ Workshop

Armen Baghumian will be taking us through The Part-time Parliament, Lamport ’90/’98 paper, [1].

While we work through the paper, we'll specify it formally in TLA+. The paper is rather long so the goal would be to specify the preliminary protocol.

Although the preliminary is not practical to implement in practice, it is a great way to learn the algorithm by not being distracted by optimization details.

Please bring a laptop
It would be a good idea to install TLA+ toolbox [2].

Here [3] you can find the TLA+ cheat sheet.

If you're interested in familiarizing yourself with TLA+, you can go through Lamport's The TLA+ Video Course [4].

[1] http://lamport.azurewebsites.net/pubs/lamport-paxos.pdf
[2] https://lamport.azurewebsites.net/video/installing-toolbox.html
[3] https://lamport.azurewebsites.net/tla/summary.pdf
[4] https://lamport.azurewebsites.net/video/videos.html