Leslie Lamport - The Paxos algorithm or how to win a Turing Award. Part 1. 

this guy gives the best talks, besides being such a genius as well obviously

I find it hard to believe that there is only 11475 views so far in 2 years! Great work! Mr.V :)

A little bit of confusion in the audience about the “magic” could be probably dispelled by reminding about the process: 1. Our goal is to have an algorithm whose behavior leads to a quorum in a distributed system. 2. We then come up with a specification of such a behavior: if Spec is true for a behavior, then we hope there would be a quorum. 3. We then must check that indeed in all cases the Spec does what we want: specify behaviors that always lead to quorum. This is done by setting up a model that uses the Spec, and proving in some way that in no case will the model’s behavior not lead to a quorum. That’s model testing or model proving. Only then we trust the Spec. 4. We must then come up not with a model, but with an actual algorithm, and we test that algorithm to fulfill the Spec. If we can show that it fulfills the Spec, then by implication all its behaviors end up in a quorum. Spec is “magic” in the sense that it only constrains behaviors to those that we consider “valid” for our purposes, but doesn’t tell us how to build a system that would behave that way. It only shows how to check if a behavior fulfills the criteria we want (eg. achieving quorum), and together with the model shows that such behaviors exist and that none of the accepted behaviors would be “broken” (not end up in a quorum). At that point the Spec is a “litmus test”, a substitute for model testing/proving. We need the substitute because it can be very general and doesn’t prescribe an implementation, and thus doesn’t corner us with an implementation that would be unduly constrained. All we want is a spec that ensures quorum and no more, ie. a spec that is false only if the behavior doesn’t lead to a quorum, and doesn’t exclude any behavior (ie. any concrete path) of getting to the quorum, as long as the necessary invariants are maintained throughout (those should be minimal invariants). We need the spec to be general, otherwise an algorithm we devise may well lead to a quorum but not fulfill the spec. And conversely, because the spec is so general, it’s prescriptive rather than constructive: it captures valid behaviors, but doesn’t in general give away how to construct them (build them up).

This guy is such a genius. I'd say it's remarkable the video has attracted only 7,318 views, but of course it isn't remarkable, RU-vid audiences favour low hanging fruit.

More details at lamport.azurewebsites.net/tla/paxos-algorithm.html

I really wish he used minbal instead of maxbal. he keeps saying that acceptors cannot vote in any ballot smaller than maxbal, that should mean it's the minimum ballot number!