[Dr. TLA+ Series] Raft - Jin Li (Thursday, July 21st, 10-11:30am PDT)

[Cheng Huang]

Welcome to the 2nd lecture in the Series. This one has been highly anticipated … :-)

Schedule:

Thursday, July 21st, 10-11:30am PDT

Live streaming:

Join Skype Meeting

Abstract 

In this talk, we will discuss Raft and its TLA+ spec. Raft is a consensus algorithm for managing a replicated log. It produces a result equivalent to (multi-)Paxos. The design of Raft separates key elements of consensus algorithm, such as leader election, log replication, etc.., which results in the Raft more understandable and implementable. Raft has been widely taught and implemented, with a partial list of implementation available at https://raft.github.io/. 

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

- In Search of an Understandable Consensus Algorithm (Best Paper at USENIX ATC 2014) (https://raft.github.io/raft.pdf)

- TLA+ specification for the Raft consensus algorithm (https://github.com/ongardie/raft.tla)

Bio:

Dr. Jin Li manages the Cloud Computing and Storage group at MSR Technologies/MSR-NExT. His team has made great contributions to Microsoft with monetary value in the order of hundreds of million dollars per annum, with works such as the local reconstruction code (LRC) in Azure and Windows Server, the erasure code used in Lync, Xbox and RemoteFX, the Data Deduplication feature in Windows Server 2012, the high performance SSD based key-value store in Bing, and the RemoteFX for WAN feature in Windows 8 and Windows Server 2012. He is an IEEE Fellow.

[Cheng Huang]

Just a reminder that the Raft lecture is on Thursday morning ...

[Cheng Huang]

The recording of the Raft lecture is now available (https://github.com/tlaplus/DrTLAPlus/blob/master/raft_lecture.md). Raft is a rather subtle algorithm, but Jin did a fantastic job explaining it and making the algorithm crystal clear.

 

The TLA+ part starts at 1 hour 5 minutes (01:05). The highlight of this part occurs at 01:15. When the audience asked whether certain information needs to be persisted, Jin modified the Raft TLA+ spec on the spot and demonstrated that TLC very quickly found an execution trace that causes invariant violation. This is a perfect example showcasing the power of specification and model checking.

 

Enjoy! J