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!
he is limited to his own knowledge. he keeps reciting his own paper "how to write a proof in 21 century" he obviously left behing all the dependent type systems we have now like irdis ,agda, Coq , and all the developments in proof assitants . He doesnt have the foundational knowledge of a Robert Harper for example.
Actually these 2 SMR algorithms use different techniques. RCU is based on quiescence state, but on the other hand Hazard Pointers is “pointer-based”. I.e. it explicitly marks live object which cannot be deallocated rn
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).
yeah the magic question is asked without understanding that this is a declarative specification. It's layer after layer, for all the thing that's not specified in the specification, it doesn't care.
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.
It does require a mental effort, and that is in general not that different from, say, physical effort. Most people wouldn’t be bothered to climb a mountain just to be able to follow along with a video, and for anyone who is not current on such formal methods it’ll take concentration and hard (but productive!) work to understand, follow, and then learn how to apply these methods in one’s own domain. I’m amazed that there are even 7k views! This is fairly specialist material, and is a “corner” of the general field of formal methods in software engineering. There are other and more popular (not necessarily better, just complementary) ways of teaching or approaching this subject - so videos like this one may well attract just a tenth as many views as this one, and still be very good. Ultimately, all those methods achieve overlapping subsets of the “holy grail” of formal capture and reasoning of software system behavior. E.g. formal semantics of programming languages are a different line of attack toward the same goal, and I see this TLA+-centric approach as a convenient fusion of “low hanging fruit” from both operational and denotational software semantics. This multiparadigm aspect certainly makes it a flexible approach, and may well make it more appealing as well. In some ways it has helped me to clear up various dusty corners in the understanding of both kinds of semantics as usually taught (typically in isolation from each other unless it’s some intro course).
because the video is boring. I am majored in pure math. I used to be crazy about formulas. Now I am an engineer. I love using graphs to explain my intuitions.
