[Dr. TLA+ Series] Paxos - Andrew Helwer (June 22nd, 10-11:30am PDT)

Welcome to the inaugural lecture in the Dr. TLA+ Series!

Time

June 22nd, 10-11:30am PDT

Abstract

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.

Bio

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.

Paper and Spec (not required, but helpful to take a look before the lecture)

Paxos Made Simple

Paxos.tla

Dr. TLA+ Series: learn an algorithm and protocol, study a specification

Each session will focus on a single algorithm and protocol, presented by a single speaker. The speaker will:

-- dive deep into how the algorithm and protocol works

-- illustrate in detail how the TLA+ specification is written

-- share the learnings from writing/studying the TLA+ specification

Audience: the series are for people who already know how to write at least simple TLA+ specs. Rather than how to get started, the series focus on learning new algorithms/protocols and techniques to write better specifications.

Time	Topic	Speaker
June	Paxos	Andrew Helwer (Microsoft)
July	Raft	Jin Li (Microsoft)
July	Logical Physical Clocks	Prof. Murat Demirbas (U. of Buffalo, SUNY)
August	Fast Paxos	Cheng Huang (Microsoft)
TBD	Serializable Snapshot Isolation	Chris Newcombe (Oracle)

.........................................................................................................................................

à Join Skype Meeting

works with web browsers (direction here)

.........................................................................................................................................