Dr. TLA+ Series- Paxos

Опубликовано 12 июля 2016, 22:50

Welcome to the inaugural lecture in the Dr. TLA+ Series! The presentation slide and the complete schedule of Dr. TLA+ Series are available at github.com/tlaplus/DrTLAPlus 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 and 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. 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)