{"id":253700,"date":"2016-06-22T00:00:00","date_gmt":"2016-06-22T07:00:07","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-research-item&p=253700"},"modified":"2016-09-02T12:15:06","modified_gmt":"2016-09-02T19:15:06","slug":"dr-tla-series-paxos","status":"publish","type":"msr-video","link":"https:\/\/www.microsoft.com\/en-us\/research\/video\/dr-tla-series-paxos\/","title":{"rendered":"Dr. TLA+ Series- Paxos"},"content":{"rendered":"

Welcome to the inaugural lecture in the Dr. TLA+ Series! \u00a0 \u00a0The presentation slide and the complete schedule of Dr. TLA+ Series are available at https:\/\/github.com\/tlaplus\/DrTLAPlus (opens in new tab)<\/span><\/a> \u00a0 \u00a0This 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. \u00a0 \u00a0Paper and Spec (not required, but helpful to take a look before the lecture) \u00a0Paxos Made Simple \u00a0Paxos.tla \u00a0 \u00a0Dr. TLA+ Series: learn an algorithm and protocol, study a specification \u00a0Each session will focus on a single algorithm and protocol, presented by a single speaker. The speaker will: \u00a0— dive deep into how the algorithm and protocol works \u00a0— illustrate in detail how the TLA+ specification is written \u00a0— share the learnings from writing\/studying the TLA+ specification \u00a0Audience: 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. \u00a0Time Topic Speaker \u00a0June Paxos Andrew Helwer (Microsoft) \u00a0July Raft Jin Li (Microsoft) \u00a0July Logical Physical Clocks Prof. Murat Demirbas (U. of Buffalo, SUNY) \u00a0August Fast Paxos Cheng Huang (Microsoft) \u00a0TBD Serializable Snapshot Isolation Chris Newcombe (Oracle)<\/p>\n","protected":false},"excerpt":{"rendered":"

Welcome to the inaugural lecture in the Dr. TLA+ Series! \u00a0 \u00a0The presentation slide and the complete schedule of Dr. TLA+ Series are available at https:\/\/github.com\/tlaplus\/DrTLAPlus \u00a0 \u00a0This 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 […]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr_hide_image_in_river":0,"footnotes":""},"research-area":[13560],"msr-video-type":[],"msr-locale":[268875],"msr-post-option":[],"msr-session-type":[],"msr-impact-theme":[],"msr-pillar":[],"msr-episode":[],"msr-research-theme":[],"class_list":["post-253700","msr-video","type-msr-video","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us"],"msr_download_urls":"","msr_external_url":"https:\/\/youtu.be\/tqU92TI3WJs","msr_secondary_video_url":"","msr_video_file":"","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/253700","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-video"}],"version-history":[{"count":1,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/253700\/revisions"}],"predecessor-version":[{"id":286841,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/253700\/revisions\/286841"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=253700"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=253700"},{"taxonomy":"msr-video-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video-type?post=253700"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=253700"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=253700"},{"taxonomy":"msr-session-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-session-type?post=253700"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=253700"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=253700"},{"taxonomy":"msr-episode","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-episode?post=253700"},{"taxonomy":"msr-research-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-theme?post=253700"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}