Welcome to the inaugural lecture in the Dr. TLA+ Series!
June 22, 2016 - 10-11:30am PDT
This lecture will familiarize you with the Paxos Protocol - what it is, what problems it solves, how it works, and why it works that way. The Paxos Protocol was developed in 1998 by Leslie Lamport and is a foundational component in the field of distributed systems, solving the difficult and critical problem of consensus in a network of unreliable processes. All of you have, at one time or another, interacted with a system depending on this protocol. This lecture is also an excellent demonstration of TLA+ as a specification language & teaching tool - many of the concepts are tricky to articulate in English but dead simple and unambiguous when read in TLA+! We will also examine the Paxos TLA+ spec as a showcase of how to write a simple, concise, and powerful specification.
Andrew Helwer is a software engineer in Microsoft Azure, living in Seattle WA. He has a BSc in computer science from the University of Calgary, and was a TA in a recent Microsoft TLA+ course delivered by Leslie Lamport. He is enthusiastic about distributed systems & formal methods, and enjoys writing Wikipedia articles in those fields.
(not required, but helpful to take a look before the lecture)