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

[Cheng Huang]

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)

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

[Simon Cross]

Greetings

I'd love to attend these, but there don't appear to be any dates or
times given and Skype no longer supports the Linux desktop (unless
they've update the web client to support video and voice on Linux
since I last checked).

Schiavo
Simon

[Stephan Merz]

The dates appear in the subject of the post. :-)

> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[Luke Dunstan]

While I am not in a reasonable time zone to watch the live broadcast anyway, I had the same concern as Simon. Although the normal Skype works on Linux, Skype for Business is not supported on Linux (not even the so-called web app), so I hope that the recording will be available later in a more portable format.

Best regards,

Luke

[Cheng Huang]

Yes, the lectures will be recorded and available for on-demand watching, accessible from any platform. :-)

Thanks,

-- Cheng

[Simon Cross]

Thanks!

[Weichung Shaw]

Hello Cheng Huang,

Where may I find the recording for the lecture?

Thanks.

Weichung Shaw

[Cheng Huang]

Andrew gave a fantastic presentation, so much so that he is now receiving compliments like the below:

“Thanks for the presentation – this was the best explanation of Paxos I’ve seen to date.”

The turnout was great too. We had 200+ attending the live session (online and a full lecture room). The recording of the lecture is now available at https://youtu.be/zCaJSrTmUFA. Enjoy!

Sorry for taking quite a while to make the recording available ...

[Weichung Shaw]

Thanks a lot! Looking forward to the (recording of) the next one. (Can't attend live, unfortunately..)

-Weichung Shaw

[fl]

While I am not in a reasonable time zone to watch the live broadcast anyway, I had the same concern as Simon. Although the normal Skype works on Linux, Skype for Business is not supported on Linux (not even the so-called web app), so I hope that the recording will be available later in a more portable format.

I take the opportunity of this remark to say my opinion about those lectures that are more and more frequent.

One of them was posted recently by Leslie. I've watched it. It was remarkable. It presented the philosophy

behind TLAPLUS together with some points I was not aware. A really good synthetic lecture. Unfortunately

the site that presented this lecture seems to consider it is its property. Impossible to have a copy

on one's laptop. Not very kind for the lecturer nor for the auditor.

On some other sites lectures can be downloaded. For instance (for those who can speak French):

https://www.college-de-france.fr/site/gerard-berry/_course.htm

But there is still a problem Berry's lectures are very rich and if you want to listen back a part of them

you can't because they are not divided into sections and have no table of contents

and no index and you can't even index by yourself the parts you would like to listen again.

Better than the usual ununderstandable powerpoints but not yet perfect.

--

FL

[Leslie Lamport]

Hi Frederic,

I didn't know that a talk of mine on PlusCal was on the web.  Could you send
me its URL?  Here are the talks of mine that on the Web that I know about.

   Who Builds a Skyscraper without Drawing Blueprints?
     SLIDES NOT SHOWN
     https://www.youtube.com/watch?v=iCRqE59VXT0
  
   How to Write a 21st Century Proof
   Heidelberg
      http://www.heidelberg-laureate-forum.org/blog/video/lecture-tuesday-september-23-2014-leslie-lamport/
      (The video is in a format my browser can't read.)
     
   A Mathematical View of Computation
   Heidelberg
      http://www.heidelberg-laureate-forum.org/blog/video/lecture-monday-august-24-2015-leslie-lamport/
   Max Plank Institute, 25 September 2015
     http://people.mpi-inf.mpg.de/~weidenb/SympTalks/
  
   What is Computation
   Technion  
     https://www.youtube.com/watch?v=BDPHfRuAFnU

If anyone knows of others, please tell me where they are.

Leslie
   

[Chris Newcombe]

   >>If anyone knows of others, please tell me where they are.

A few more:

1. Thinking for Programmers   (includes the non-recursive QuickSort example)
     https://www.youtube.com/watch?v=4nhFqf_46ZQ

2. Thinking Above the Code    (somewhat similar to #1, different Q&A)
     https://www.youtube.com/watch?v=-4Yp3j_jk8Q

3. Turing Award Lecture      (This link is broken for me now. It used to work.)
     http://amturing.acm.org/vp/lamport_1205376.cfm

4. A Mathematical view of Computer Systems   (21st Century Computing Conference in Beijing)
     https://www.youtube.com/watch?v=oIwdN-irLqs

5. What is Computation?        (Silicon Valley Leaders Symposium)
     https://www.youtube.com/watch?v=FRLFrZdTkuI

[fl]

   How to Write a 21st Century Proof
   Heidelberg
      http://www.heidelberg-laureate-forum.org/blog/video/lecture-tuesday-september-23-2014-leslie-lamport/
      (The video is in a format my browser can't read.)

I have written a proof using this method.

http://us2.metamath.org:88/downloads/inpreima2.pdf

The references are to metamath. (Not sure they are still up to date.)

http://www.metamath.org/

In my opinion, you need a specific editor to write this kind of proof. Writing it
as a latex text in a normal editor is very demanding even with the system of abbreviation
proposed by pf2.


When I was in high school, my main problem (one of my main problems to be honest) was
to deal with  all those hypotheses that pop in an out during the proof. Sometimes you could

use them, sometimes you couldn't. With  the model of proof proposed here and its hierarchy,

I would have understood.
 

     
   A Mathematical View of Computation
   Heidelberg
      http://www.heidelberg-laureate-forum.org/blog/video/lecture-monday-august-24-2015-leslie-lamport/

This is this one that I had seen. Very beautiful talk. A link to it deserves to be kept somewhere in an official
html page so that we can access it easily.

In fact they nearly have the kind of index I was asking for since it is possible to choose the slide and the
part of the talk referring to it begins.

--
FL

[fl]

In my opinion, you need a specific editor to write it. Writing it

as a latex text in a normal editor is very demanding even with the system of abbreviation
proposed by pf2.

The main problem with this kind of proof is that the hierarchy of sublevels can be very deep and
it's hard to write it on a sheet of paper. But you can make a reference to another sheet of paper obviously.
 

--
FL
 

[fl]

http://us2.metamath.org:88/downloads/inpreima2.pdf

Looking at it again several years later (I had written it in february 2012) I think it looks great.
I should read it again to know if it is true :)

What is poor is the trail of QEDs at the end. And it is also a bit too much detailed at one place:

it doesn't make sense for a human being.

Here is the source.

http://us2.metamath.org:88/downloads/inpreima2.tex
 
--
FL

[fl]

I've posted a new version of inpreima2 (that looks better) as an example of how to write
a 21st century proof.

http://us2.metamath.org:88/downloads/inpreima2.pdf

http://us2.metamath.org:88/downloads/inpreima2.tex

 
--
FL