July 21, 2016 - 10-11:30am PDT
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/.
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.
(not required, but helpful to take a look before the lecture)
- In Search of an Understandable Consensus Algorithm (Best Paper at USENIX ATC 2014)
- Raft TLA+ specification