27 ms·

The Paxos Algorithm, or How to Win a Turing Award

328 points by pron 7y ago

moomin 7y ago
Probably my favourite Lamport story is that his original Paxos paper was written in such a basic style (literally, Byzantine generals) that readers failed to realise exactly how revolutionary the content was.
- SilasX 7y ago
  Academic papers are almost encouraged to be hard to follow to make them sound more impressive.
  - std_throwaway 7y ago
    From experience I can tell you that the solution often is very very complex in the beginning. So complex even the researcher doesn't understand it. Publication comes when the solution can be expressed in a way that at least a handful of researchers can understand it. But this is not the end. Going back and looking at it one, three, ten, twenty years later people often find better, easier ways to express it.
  - lanstin 7y ago
    First third should be able to be understood by everyone even the students. Second third should only be comprehensible by professors. The last third should only be comprehended by the speaker. (Old joke about seminar talks).
  - CobrastanJorji 7y ago
    Yes, but the Paxos paper is the opposite. It read like a silly homily. It's like "why's poignant guide to algorithms" except that the algorithm being described was complex, novel, and incredibly useful. It was so not full of itself that it was ignored for years. It seems to be proof that trying to sound impressive is actually important.
    - perennate 7y ago
      > algorithm being described was complex I'd argue that the algorithm itself is simple, and that the difficult part is understanding why it works (i.e., why it satisfies the safety guarantees). > It seems to be proof that trying to sound impressive is actually important. I agree with this, and would add that making a paper sound impressive rarely conflicts with making it easy to understand. If anything, pointing out the contributions and applications of an approach help readers to understand that approach. At any rate, the same paper made easier to understand will generally be more likely to be accepted.
- cube2222 7y ago
  Actually, the original Paxos paper is about a "forgotten Greek island, Paxos, and its Parliament". And allegedly he presented it in an Indiana Jones outfit the first time. Byzantine generals were there in one of his earlier papers.
  - perennate 7y ago
    Link for anyone who wants to check it out: https://lamport.azurewebsites.net/pubs/lamport-paxos.pdf https://lamport.azurewebsites.net/pubs/lamport-paxos.pdf
  - truncate 7y ago
    Yep, the original Paxos paper wasn't easy to understand, and he says so in his follow up paper "Paxos made simple"[1] whose name justifies its existence as well. [1] https://lamport.azurewebsites.net/pubs/paxos-simple.pdf https://lamport.azurewebsites.net/pubs/paxos-simple.pdf
- scottlamb 7y ago
  That's interesting because I had the opposite impression: important but hard to understand. I think this has been common since at least 2001, given this text on his website: > At the PODC 2001 conference, I got tired of everyone saying how difficult it was to understand the Paxos algorithm, published in [122]. https://lamport.azurewebsites.net/pubs/pubs.html#paxos-simple https://lamport.azurewebsites.net/pubs/pubs.html#paxos-simpl... I didn't start working on distributed storage systems until 2007. Perhaps some people who read the paper in 1997 had a different impression. Edit: maybe we have different takes on this story from that same url: > My attempt at inserting some humor into the subject was a dismal failure. People who attended my lecture remembered Indiana Jones, but not the algorithm. People reading the paper apparently got so distracted by the Greek parable that they didn't understand the algorithm. You're saying they didn't understand the importance; I took that to mean they didn't understand the details. ... and reading onward from the section I quoted, it sounds like your take was correct!
  - dunkelheit 7y ago
    The terminology surrounding Paxos is very unfortunate in my opinion. First there is this general air of mystery which is entirely unnecessary. Next, the paper talks about "ballots" and "voting" but the actual protocol is very different from what is usually understood by voting - in the protocol everybody just votes what the leader told them! Maybe call it soviet-style voting or something.
    - furyofantares 7y ago
      I understand your complaint about the terminology and in the linked video that same confusion came up. But the terminology does make sense to me in the context of trying to reach consensus. When I’ve been a part of a group looking to reach consensus there’s an occasional ballot/vote taken to check for consensus and there isn’t a functional difference between abstaining and voting for some non-leading option. If you just say up front that there are additional logical constraints on when to abstain vs vote for the leader that make it work in a distributed system, then I think the metaphor serves to help think about it rather than confuse.
  - 7y ago
- ahelwer 7y ago
  I think you're thinking of his paper ordering of events in a distributed system, not the Paxos paper.
eternalban 7y ago
I have always been puzzled as to why Brian Oki & Barbara Liskov's earlier (1988) "Viewstamped Replication" has been shadowed by Lamport's work. Isn't the RAFT that rocked Paxos's boat not a variant of their work? I would appreciate knowledgeable insights about this.
- heavenlyblue 7y ago
  Lamport’s work is much more general in nature. I have to admit it’s harder to follow for the same reason.
- silasdavis 7y ago
  I also don't understand this
- bt848 7y ago
  I don't know if raft "rocked" paxos's boat or not. It's a social phenomenon where Stanford people and their associates evangelize raft not because it is superior but just because it came from Stanford. People think raft is easier to implement but from my studies of available implementations the truth is it's actually just more likely that someone will Dunning-Krueger their way into believing they can implement it. There are a large number of defective raft implementations in the wild. There are almost no paxos implementations, correct or otherwise, making it harder to reason about its popularity and ergonomics. One thing is for sure: if you think you do not quite understand paxos then it is quite likely that you also do not understand raft, even though raft makes you feel like you might.
  - kerkeslager 7y ago
    Raft also has a frequently-linked, simple visual explanation[1]. If that's at all accurate to what Raft is, that would certainly make Raft easier to understand than Paxos, although that's a function of the learning materials available, not anything inherently more understandable about the algorithm itself. I feel that I understand Raft and not Paxos, although currently that's simply because I haven't yet tried to understand Paxos. But the reason I am still interested in Paxos is that looking at Raft, it still seems like Raft has a bottleneck at the leader. Essentially, it looks like what makes this distributed consensus look simple is that only leader elections are actually distributed: the rest of the algorithm isn't distributed at all. When I get around to reading about Paxos I'm hoping it will be different. [1] https://raft.github.io/ https://raft.github.io/
sova 7y ago
Are all Turing Award winners Turing Award Complete?
codepie 7y ago
The rest of the material from the summer school is available here: https://sptdc.ru/schedule/ https://sptdc.ru/schedule/
dunkelheit 7y ago
I had the privilege of attending this lecture in person. One eerie thing about it was that Dr. Lamport didn't improvise at all - he just read from the slides and that was all he had to say! Overall it was a good introduction to TLA+ which I think has a big advantage of being very simple to understand and use - no complicated math needed apart from set theory. What I didn't quite understand is how to make sure that your models are implementable in code (if you start with a model) and faithfully describe your actual code and the reality itself. Seems like all bugs will end up lurking in this gap between the model and what is actually executed and there is no reliable way to close this gap.
- pron 7y ago
  This is a common question among TLA+ beginners. There can be bugs in the implementation. Those would either be bugs due to a mistranslation of the spec -- i.e., an error in the implementation -- or, because the spec also implicitly or explicitly describes the assumptions about the environment, a mismatch between the actual environment (hardware, software stack, user behavior) and the spec -- i.e. an error in the spec. In both cases, having the spec makes finding those bugs easier, and in the first case, the bugs are usually cheap to find and fix. The costliest bugs are in the design, and that's where TLC, a model checker for TLA+, can automatically spot them. Now, what if you want a formal -- i.e. mechanical -- relationship between the code and the spec? In principle, this is possible, and has been done; e.g. see [1] for C, and there have been other, similar projects for Java. In practice, we don't do it. Why? Well, we can't. There is no known technique that can verify anything but small programs/specs for arbitrary correctness properties. The reason is that the scalability of all formal methods has limitations. Currently, we can formally verify a few thousand lines of formal specification. That specification can be either code or a high-level spec. That means that we can either verify very small programs, or a high-level spec that represents a large program. The latter is the only thing available to us to help with large program, and how TLA+ is normally used. Small programs are verified end-to-end (i.e., that the actual code, or even machine code, conforms to a high-level spec) only in very special, niche, cases, and/or at a great cost. What else can we do? We can verify code not against a high-level spec, but against some specification of small, local properties. This way, every code unit is verified separately [2]. This could help catch errors in translation, but, while useful, the benefit is not as great as verifying a high-level spec. This approach, a high-level spec verified formally, translated informally to code, and the code is then verified formally against local properties only, is how Altran UK builds their software; they use the older Z, instead of TLA+ for the high-level spec, and SPARK for code-level verification. Local properties can be verified with languages/tools like SPARK, JML and its various tools for Java, ACSL and various tools for C, and others, including dependent type languages used in research. There is also an affordable way to mechanically check a program's conformance to a TLA+ spec, but only approximately -- it isn't sound. It's called "model-based trace-checking," and the idea is to grab logs from the program, or an entire distributed system, and let TLC check that they conform to a possible execution of the spec. I've written about this technique here [3]. It is important to realize that all kinds of software assurance techniques, from proof assistants to unit tests, come with significant tradeoffs to confidence, effort and scale, and that none can guarantee that a system will not fail. We must choose an appropriate balance for our specific system, usually by employing more than one approach (usually more than two). Personally, I think that high-level TLA+ specifications, checked with the TLC model checker (not with the TLAPS proof assistant) are at a pretty good sweet-spot for a relatively large number of mainstream software projects in terms of cost/benefit compared to other tools and approaches (but should still be combined with testing and code review). [1]: https://cedric.cnam.fr/fichiers/art_3439.pdf https://cedric.cnam.fr/fichiers/art_3439.pdf [2]: You may think that it's possible to verify local properties of local units, and then compose them to ensure conformance to a high-level spec. Unfortunately, this way doesn't beat the scalability limitation, and also works only on very small programs. [3]: https://pron.github.io/files/Trace.pdf https://pron.github.io/files/Trace.pdf
SoylentOrange 7y ago
My advisor’s advisor worked with Lamport, and my advisor’s thesis was in distributed consensus in file systems. My advisor worked heavily on a lot of the Paxos follow up work. He told me that Paxos is actually so complicated that only Lamport really understands it. He said that after the original paper came out, everyone was trying to simplify it, but no one was successful. He said almost any implementation he saw (in those early years) contained serious errors. It’s a truly remarkable thing.
- fulafel 7y ago
  It almost seems like TLA paradoxically made systems harder to understand, since presumably it was the enabler for pushing the limit of complexity.
  - contingencies 7y ago
    Isn't this a truism with all technology? One could say the same about, for example, human language itself or any domain-specific professional vocabulary. As programmers we are relatively unique in that we are encouraged to analyze, create and maintain the behavior of complex systems across disparate domains, which demands developing a certain comfort with new vocabularies and an independent capacity for identifying behavioral and structural similarities across systems and domains. Some ~relevant quotes: Tesler's Law of Conservation of Complexity: Every application has an inherent amount of irreducible complexity. The only question is who will have to deal with it - the user, the application developer, or the platform developer? - Larry Tesler (ca. 1984) With a good programming language and interface, one - even children - can create from scratch important simulations of complex non-linear systems that can help one's thinking about them. - Alan Kay (2016) An evolving system increases its complexity unless work is done to reduce it. - Meir Lehman Any sufficiently complex system acts as a black box when it becomes easier to experiment with than to understand. Hence, black-box optimization has become increasingly important as systems become more complex. - Google Vizier: a service for black-box optimization Golovin et al., KDD'17 We're more aware of simple processes that don't work well than of complex ones that work flawlessly. - Marvin Minsky, MIT AI lab co-founder Tainter's Law of Problem Solving: As easier solutions are exhausted, problem solving moves inexorably to greater complexity, higher costs, and diminishing returns. The endogenous nature of [the] buildup of complexity eventually makes the system fundamentally illegible to the human operator - a phenomenon that is ironic given that the fundamental aim of the control revolution is to increase legibility. - Ashwin Parameswaran (2012) It is time to unmask the computing community as a Secret Society for the Creation and Preservation of Artificial Complexity. - Edsger Dijkstra You're not going to find the best algorithm in terms of computational complexity by coding. - Leslie Lamport I have struggled with complexity my entire career. One of our key approaches for managing complexity is to 'walk away' and start fresh. Often new tools or languages force us to start from scratch which means that developers end up conflating the benefits of the tool with the benefits of the clean start. The clean start is what is fundamental. The simplest way of controlling complexity growth is to build a smaller system with fewer developers. - Terry Crowley Successful programming is all about managing complexity. Managing complexity has many aspects. You can eliminate, avoid, simplify, hide or automate complexity, and so on. - Keith Bentley The most robust programs isolate complexity in a way that lets significant parts of the system appear simple and straightforward and interact in simple ways with other components in the system. - Terry Crowley ... from https://github.com/globalcitizen/taoup https://github.com/globalcitizen/taoup
justicezyx 7y ago
I got rumors that Lamport is not a well sociable figure, therefore get less recognition from his peers, which delayed his Turing award. Any anecdotes?
antirez 7y ago
I wonder if DS would have a different tone now if the leading figure would be somebody else more focused in making things intuitive and understandable. I've the feeling that many DS concepts, after you understand them, you say like: wow that was really not very well explained in the books I read.
- noahl 7y ago
  Making a concept intuitive and easy to understand is extremely difficult to do. A person who could do this would probably have to understand Paxos better than Lamport does. I wouldn't assume that Leslie Lamport doesn't want his algorithm to be understood. It's just that explaining things is really, really, really hard. (This is also why teaching is an incredibly difficult profession.)
  - perennate 7y ago
    Making an explanation intuitive takes time and effort, but I don't think it requires the explainer to have a better understanding of the concept than another person. They probably must have a good understanding of the concept, but once there is a good enough understanding, I think it's more a matter of finding the right way to explain it. Lamport's original Paxos paper (https://lamport.azurewebsites.net/pubs/lamport-paxos.pdf https://lamport.azurewebsites.net/pubs/lamport-paxos.pdf) is notoriously difficult to understand because he decided to write the whole paper as an archeological survey report. Writing an explanation more intuitive than that isn't difficult even with only a basic understanding of Paxos -- just avoid the whole island and Parliament thing. His later paper (https://lamport.azurewebsites.net/pubs/paxos-simple.pdf https://lamport.azurewebsites.net/pubs/paxos-simple.pdf) is much more clear.
    - sabujp 7y ago
      reading the paxos-simple.pdf it seems it's very much like blockchain
  - stingraycharles 7y ago
    Not necessarily. Sometimes it takes a person who’s involved with “laymen” to explain a solution in simple terms that resonates well with them. This is why being a good teacher is not at all the same trait as being a good researcher: they’re two very distinct skills.
6thaccount2 7y ago
I've tried googling paxos algorithm a bit, but don't understand what it does and why it is useful. Could someone please explain it to me like I'm five?
- antirez 7y ago
  It's goal in the end is very simple: you have N different state machines and you want every state machine to process the same operations in the same order. To do that you need they agree every time a new operation must be processed. (Multi) Paxos is an agreement algorithm that does that.
  - antpls 7y ago
    Does Paxos work in adversarial environment (where some nodes are compromised and try to trick the system by sending forged messages) ?
    - yodsanklai 7y ago
      No, but there are other versions who do. Look up byzantine consensus.
- deleted 7y ago
  [deleted]
- truncate 7y ago
  Start with understanding "Consensus problem". Paxos is one of the famous solution. There is blog called "The Paper Trail" which has lots of articles on this topic[1]. You should start with the oldest post IMO (from Three General Proble,, FLP impossibility, 2/3 phase locking, to Paxos). Once you have an idea, you can readup the "Paxos made simple"[2]. In distributed systems, each node needs to agree on facts (which could be value of a key, ordering of operations on an object etc...), and Paxos helps you with that. [1] https://www.the-paper-trail.org/tags/consensus/ https://www.the-paper-trail.org/tags/consensus/ [2] https://lamport.azurewebsites.net/pubs/paxos-simple.pdf https://lamport.azurewebsites.net/pubs/paxos-simple.pdf
- 7y ago
vyodaiken 7y ago
Paxos is wrong, as Lamport explains on page 7 of "Paxos made simple", but apparently nobody reads that far.
- grogers 7y ago
  Page 7 talks about the conditions under which a liveness condition can be satisfied. What about that is wrong? If you mean paxos is wrong because it can't guarantee progress, then sure it's wrong (and because of FLP, all consensus algorithms are)
  - vyodaiken 7y ago
    Paxos livelocks (doesn’t work). So Lamport suggests electing a coordinator via timeouts(since flp is a joke). But if you can elect via timeouts you don’t need paxos at all. QED The really annoying thing is that "Paxos Made Simple" begins by outlining the algorithm as a solution for a completely async network (unlike real networks) but then towards the end, just blows that off and falls back on timeouts. But if you have timeouts there are far simpler and more efficient solutions. FWIW: FLP is a silly "theorem" that says "if you can't tell the difference between a system that has crashed and one that is slow - why then you can't tell the difference."
    - ahelwer 7y ago
      Paxos livelocks in a very unstable state which requires multiple independent nodes to sent specific messages at specific times. If you add random intervals between retries, the probability of staying in a livelocked state quickly grows astonishingly low.
      - vyodaiken 7y ago
        I wrote a little simulation. Paxos rarely gets stuck with a small number of proposers/acceptors, but jams up solid once you get to, I forget, 10 or 20. Here it is: https://www.yodaiken.com/wp-content/uploads/2016/10/paxos.ptpx_.ppxt_.png https://www.yodaiken.com/wp-content/uploads/2016/10/paxos.pt... Embarrassingly badly written Lua code for the simulator https://github.com/yodaikenv/consensus https://github.com/yodaikenv/consensus The key to me is that once you accept the need for leader election, you have much simpler alternatives and can toss away the rest of paxos.
sabujp 7y ago
paxos is used heavily in cloud spanner, also tldr; https://youtu.be/8-Bc5Lqgx_c?t=4494 https://youtu.be/8-Bc5Lqgx_c?t=4494 , it's also interesting to watch two mathematicians go at it : https://youtu.be/8-Bc5Lqgx_c?t=4902 https://youtu.be/8-Bc5Lqgx_c?t=4902
sabujp 7y ago
there's a tla video course by lamport : https://www.youtube.com/watch?v=p54W-XOIEF8&list=PLWAv2Etpa7AOAwkreYImYt0gIpOdWQevD https://www.youtube.com/watch?v=p54W-XOIEF8&list=PLWAv2Etpa7...

328 points by pron 7y ago

Probably my favourite Lamport story is that his original Paxos paper was written in such a basic style (literally, Byzantine generals) that readers failed to realise exactly how revolutionary the content was.

SilasX 7y ago
Academic papers are almost encouraged to be hard to follow to make them sound more impressive.
- std_throwaway 7y ago
  From experience I can tell you that the solution often is very very complex in the beginning. So complex even the researcher doesn't understand it. Publication comes when the solution can be expressed in a way that at least a handful of researchers can understand it. But this is not the end. Going back and looking at it one, three, ten, twenty years later people often find better, easier ways to express it.
- lanstin 7y ago
  First third should be able to be understood by everyone even the students. Second third should only be comprehensible by professors. The last third should only be comprehended by the speaker. (Old joke about seminar talks).
- CobrastanJorji 7y ago
  Yes, but the Paxos paper is the opposite. It read like a silly homily. It's like "why's poignant guide to algorithms" except that the algorithm being described was complex, novel, and incredibly useful. It was so not full of itself that it was ignored for years. It seems to be proof that trying to sound impressive is actually important.
  - perennate 7y ago
    > algorithm being described was complex I'd argue that the algorithm itself is simple, and that the difficult part is understanding why it works (i.e., why it satisfies the safety guarantees). > It seems to be proof that trying to sound impressive is actually important. I agree with this, and would add that making a paper sound impressive rarely conflicts with making it easy to understand. If anything, pointing out the contributions and applications of an approach help readers to understand that approach. At any rate, the same paper made easier to understand will generally be more likely to be accepted.
cube2222 7y ago
Actually, the original Paxos paper is about a "forgotten Greek island, Paxos, and its Parliament". And allegedly he presented it in an Indiana Jones outfit the first time. Byzantine generals were there in one of his earlier papers.
- perennate 7y ago
  Link for anyone who wants to check it out: https://lamport.azurewebsites.net/pubs/lamport-paxos.pdf https://lamport.azurewebsites.net/pubs/lamport-paxos.pdf
- truncate 7y ago
  Yep, the original Paxos paper wasn't easy to understand, and he says so in his follow up paper "Paxos made simple"[1] whose name justifies its existence as well. [1] https://lamport.azurewebsites.net/pubs/paxos-simple.pdf https://lamport.azurewebsites.net/pubs/paxos-simple.pdf
scottlamb 7y ago
That's interesting because I had the opposite impression: important but hard to understand. I think this has been common since at least 2001, given this text on his website: > At the PODC 2001 conference, I got tired of everyone saying how difficult it was to understand the Paxos algorithm, published in [122]. https://lamport.azurewebsites.net/pubs/pubs.html#paxos-simple https://lamport.azurewebsites.net/pubs/pubs.html#paxos-simpl... I didn't start working on distributed storage systems until 2007. Perhaps some people who read the paper in 1997 had a different impression. Edit: maybe we have different takes on this story from that same url: > My attempt at inserting some humor into the subject was a dismal failure. People who attended my lecture remembered Indiana Jones, but not the algorithm. People reading the paper apparently got so distracted by the Greek parable that they didn't understand the algorithm. You're saying they didn't understand the importance; I took that to mean they didn't understand the details. ... and reading onward from the section I quoted, it sounds like your take was correct!
- dunkelheit 7y ago
  The terminology surrounding Paxos is very unfortunate in my opinion. First there is this general air of mystery which is entirely unnecessary. Next, the paper talks about "ballots" and "voting" but the actual protocol is very different from what is usually understood by voting - in the protocol everybody just votes what the leader told them! Maybe call it soviet-style voting or something.
  - furyofantares 7y ago
    I understand your complaint about the terminology and in the linked video that same confusion came up. But the terminology does make sense to me in the context of trying to reach consensus. When I’ve been a part of a group looking to reach consensus there’s an occasional ballot/vote taken to check for consensus and there isn’t a functional difference between abstaining and voting for some non-leading option. If you just say up front that there are additional logical constraints on when to abstain vs vote for the leader that make it work in a distributed system, then I think the metaphor serves to help think about it rather than confuse.
- 7y ago
ahelwer 7y ago
I think you're thinking of his paper ordering of events in a distributed system, not the Paxos paper.

eternalban 7y ago

I have always been puzzled as to why Brian Oki & Barbara Liskov's earlier (1988) "Viewstamped Replication" has been shadowed by Lamport's work. Isn't the RAFT that rocked Paxos's boat not a variant of their work? I would appreciate knowledgeable insights about this.

heavenlyblue 7y ago
Lamport’s work is much more general in nature. I have to admit it’s harder to follow for the same reason.
silasdavis 7y ago
I also don't understand this
bt848 7y ago
I don't know if raft "rocked" paxos's boat or not. It's a social phenomenon where Stanford people and their associates evangelize raft not because it is superior but just because it came from Stanford. People think raft is easier to implement but from my studies of available implementations the truth is it's actually just more likely that someone will Dunning-Krueger their way into believing they can implement it. There are a large number of defective raft implementations in the wild. There are almost no paxos implementations, correct or otherwise, making it harder to reason about its popularity and ergonomics. One thing is for sure: if you think you do not quite understand paxos then it is quite likely that you also do not understand raft, even though raft makes you feel like you might.
- kerkeslager 7y ago
  Raft also has a frequently-linked, simple visual explanation[1]. If that's at all accurate to what Raft is, that would certainly make Raft easier to understand than Paxos, although that's a function of the learning materials available, not anything inherently more understandable about the algorithm itself. I feel that I understand Raft and not Paxos, although currently that's simply because I haven't yet tried to understand Paxos. But the reason I am still interested in Paxos is that looking at Raft, it still seems like Raft has a bottleneck at the leader. Essentially, it looks like what makes this distributed consensus look simple is that only leader elections are actually distributed: the rest of the algorithm isn't distributed at all. When I get around to reading about Paxos I'm hoping it will be different. [1] https://raft.github.io/ https://raft.github.io/

sova 7y ago

Are all Turing Award winners Turing Award Complete?

codepie 7y ago

The rest of the material from the summer school is available here: https://sptdc.ru/schedule/ https://sptdc.ru/schedule/

dunkelheit 7y ago

I had the privilege of attending this lecture in person. One eerie thing about it was that Dr. Lamport didn't improvise at all - he just read from the slides and that was all he had to say! Overall it was a good introduction to TLA+ which I think has a big advantage of being very simple to understand and use - no complicated math needed apart from set theory. What I didn't quite understand is how to make sure that your models are implementable in code (if you start with a model) and faithfully describe your actual code and the reality itself. Seems like all bugs will end up lurking in this gap between the model and what is actually executed and there is no reliable way to close this gap.

pron 7y ago
This is a common question among TLA+ beginners. There can be bugs in the implementation. Those would either be bugs due to a mistranslation of the spec -- i.e., an error in the implementation -- or, because the spec also implicitly or explicitly describes the assumptions about the environment, a mismatch between the actual environment (hardware, software stack, user behavior) and the spec -- i.e. an error in the spec. In both cases, having the spec makes finding those bugs easier, and in the first case, the bugs are usually cheap to find and fix. The costliest bugs are in the design, and that's where TLC, a model checker for TLA+, can automatically spot them. Now, what if you want a formal -- i.e. mechanical -- relationship between the code and the spec? In principle, this is possible, and has been done; e.g. see [1] for C, and there have been other, similar projects for Java. In practice, we don't do it. Why? Well, we can't. There is no known technique that can verify anything but small programs/specs for arbitrary correctness properties. The reason is that the scalability of all formal methods has limitations. Currently, we can formally verify a few thousand lines of formal specification. That specification can be either code or a high-level spec. That means that we can either verify very small programs, or a high-level spec that represents a large program. The latter is the only thing available to us to help with large program, and how TLA+ is normally used. Small programs are verified end-to-end (i.e., that the actual code, or even machine code, conforms to a high-level spec) only in very special, niche, cases, and/or at a great cost. What else can we do? We can verify code not against a high-level spec, but against some specification of small, local properties. This way, every code unit is verified separately [2]. This could help catch errors in translation, but, while useful, the benefit is not as great as verifying a high-level spec. This approach, a high-level spec verified formally, translated informally to code, and the code is then verified formally against local properties only, is how Altran UK builds their software; they use the older Z, instead of TLA+ for the high-level spec, and SPARK for code-level verification. Local properties can be verified with languages/tools like SPARK, JML and its various tools for Java, ACSL and various tools for C, and others, including dependent type languages used in research. There is also an affordable way to mechanically check a program's conformance to a TLA+ spec, but only approximately -- it isn't sound. It's called "model-based trace-checking," and the idea is to grab logs from the program, or an entire distributed system, and let TLC check that they conform to a possible execution of the spec. I've written about this technique here [3]. It is important to realize that all kinds of software assurance techniques, from proof assistants to unit tests, come with significant tradeoffs to confidence, effort and scale, and that none can guarantee that a system will not fail. We must choose an appropriate balance for our specific system, usually by employing more than one approach (usually more than two). Personally, I think that high-level TLA+ specifications, checked with the TLC model checker (not with the TLAPS proof assistant) are at a pretty good sweet-spot for a relatively large number of mainstream software projects in terms of cost/benefit compared to other tools and approaches (but should still be combined with testing and code review). [1]: https://cedric.cnam.fr/fichiers/art_3439.pdf https://cedric.cnam.fr/fichiers/art_3439.pdf [2]: You may think that it's possible to verify local properties of local units, and then compose them to ensure conformance to a high-level spec. Unfortunately, this way doesn't beat the scalability limitation, and also works only on very small programs. [3]: https://pron.github.io/files/Trace.pdf https://pron.github.io/files/Trace.pdf

SoylentOrange 7y ago

My advisor’s advisor worked with Lamport, and my advisor’s thesis was in distributed consensus in file systems. My advisor worked heavily on a lot of the Paxos follow up work. He told me that Paxos is actually so complicated that only Lamport really understands it. He said that after the original paper came out, everyone was trying to simplify it, but no one was successful. He said almost any implementation he saw (in those early years) contained serious errors. It’s a truly remarkable thing.

fulafel 7y ago
It almost seems like TLA paradoxically made systems harder to understand, since presumably it was the enabler for pushing the limit of complexity.
- contingencies 7y ago
  Isn't this a truism with all technology? One could say the same about, for example, human language itself or any domain-specific professional vocabulary. As programmers we are relatively unique in that we are encouraged to analyze, create and maintain the behavior of complex systems across disparate domains, which demands developing a certain comfort with new vocabularies and an independent capacity for identifying behavioral and structural similarities across systems and domains. Some ~relevant quotes: Tesler's Law of Conservation of Complexity: Every application has an inherent amount of irreducible complexity. The only question is who will have to deal with it - the user, the application developer, or the platform developer? - Larry Tesler (ca. 1984) With a good programming language and interface, one - even children - can create from scratch important simulations of complex non-linear systems that can help one's thinking about them. - Alan Kay (2016) An evolving system increases its complexity unless work is done to reduce it. - Meir Lehman Any sufficiently complex system acts as a black box when it becomes easier to experiment with than to understand. Hence, black-box optimization has become increasingly important as systems become more complex. - Google Vizier: a service for black-box optimization Golovin et al., KDD'17 We're more aware of simple processes that don't work well than of complex ones that work flawlessly. - Marvin Minsky, MIT AI lab co-founder Tainter's Law of Problem Solving: As easier solutions are exhausted, problem solving moves inexorably to greater complexity, higher costs, and diminishing returns. The endogenous nature of [the] buildup of complexity eventually makes the system fundamentally illegible to the human operator - a phenomenon that is ironic given that the fundamental aim of the control revolution is to increase legibility. - Ashwin Parameswaran (2012) It is time to unmask the computing community as a Secret Society for the Creation and Preservation of Artificial Complexity. - Edsger Dijkstra You're not going to find the best algorithm in terms of computational complexity by coding. - Leslie Lamport I have struggled with complexity my entire career. One of our key approaches for managing complexity is to 'walk away' and start fresh. Often new tools or languages force us to start from scratch which means that developers end up conflating the benefits of the tool with the benefits of the clean start. The clean start is what is fundamental. The simplest way of controlling complexity growth is to build a smaller system with fewer developers. - Terry Crowley Successful programming is all about managing complexity. Managing complexity has many aspects. You can eliminate, avoid, simplify, hide or automate complexity, and so on. - Keith Bentley The most robust programs isolate complexity in a way that lets significant parts of the system appear simple and straightforward and interact in simple ways with other components in the system. - Terry Crowley ... from https://github.com/globalcitizen/taoup https://github.com/globalcitizen/taoup

justicezyx 7y ago

I got rumors that Lamport is not a well sociable figure, therefore get less recognition from his peers, which delayed his Turing award. Any anecdotes?

antirez 7y ago

I wonder if DS would have a different tone now if the leading figure would be somebody else more focused in making things intuitive and understandable. I've the feeling that many DS concepts, after you understand them, you say like: wow that was really not very well explained in the books I read.

noahl 7y ago
Making a concept intuitive and easy to understand is extremely difficult to do. A person who could do this would probably have to understand Paxos better than Lamport does. I wouldn't assume that Leslie Lamport doesn't want his algorithm to be understood. It's just that explaining things is really, really, really hard. (This is also why teaching is an incredibly difficult profession.)
- perennate 7y ago
  Making an explanation intuitive takes time and effort, but I don't think it requires the explainer to have a better understanding of the concept than another person. They probably must have a good understanding of the concept, but once there is a good enough understanding, I think it's more a matter of finding the right way to explain it. Lamport's original Paxos paper (https://lamport.azurewebsites.net/pubs/lamport-paxos.pdf https://lamport.azurewebsites.net/pubs/lamport-paxos.pdf) is notoriously difficult to understand because he decided to write the whole paper as an archeological survey report. Writing an explanation more intuitive than that isn't difficult even with only a basic understanding of Paxos -- just avoid the whole island and Parliament thing. His later paper (https://lamport.azurewebsites.net/pubs/paxos-simple.pdf https://lamport.azurewebsites.net/pubs/paxos-simple.pdf) is much more clear.
  - sabujp 7y ago
    reading the paxos-simple.pdf it seems it's very much like blockchain
- stingraycharles 7y ago
  Not necessarily. Sometimes it takes a person who’s involved with “laymen” to explain a solution in simple terms that resonates well with them. This is why being a good teacher is not at all the same trait as being a good researcher: they’re two very distinct skills.

6thaccount2 7y ago

I've tried googling paxos algorithm a bit, but don't understand what it does and why it is useful. Could someone please explain it to me like I'm five?

antirez 7y ago
It's goal in the end is very simple: you have N different state machines and you want every state machine to process the same operations in the same order. To do that you need they agree every time a new operation must be processed. (Multi) Paxos is an agreement algorithm that does that.
- antpls 7y ago
  Does Paxos work in adversarial environment (where some nodes are compromised and try to trick the system by sending forged messages) ?
  - yodsanklai 7y ago
    No, but there are other versions who do. Look up byzantine consensus.
deleted 7y ago
[deleted]
truncate 7y ago
Start with understanding "Consensus problem". Paxos is one of the famous solution. There is blog called "The Paper Trail" which has lots of articles on this topic[1]. You should start with the oldest post IMO (from Three General Proble,, FLP impossibility, 2/3 phase locking, to Paxos). Once you have an idea, you can readup the "Paxos made simple"[2]. In distributed systems, each node needs to agree on facts (which could be value of a key, ordering of operations on an object etc...), and Paxos helps you with that. [1] https://www.the-paper-trail.org/tags/consensus/ https://www.the-paper-trail.org/tags/consensus/ [2] https://lamport.azurewebsites.net/pubs/paxos-simple.pdf https://lamport.azurewebsites.net/pubs/paxos-simple.pdf
7y ago

vyodaiken 7y ago

Paxos is wrong, as Lamport explains on page 7 of "Paxos made simple", but apparently nobody reads that far.

grogers 7y ago
Page 7 talks about the conditions under which a liveness condition can be satisfied. What about that is wrong? If you mean paxos is wrong because it can't guarantee progress, then sure it's wrong (and because of FLP, all consensus algorithms are)
- vyodaiken 7y ago
  Paxos livelocks (doesn’t work). So Lamport suggests electing a coordinator via timeouts(since flp is a joke). But if you can elect via timeouts you don’t need paxos at all. QED The really annoying thing is that "Paxos Made Simple" begins by outlining the algorithm as a solution for a completely async network (unlike real networks) but then towards the end, just blows that off and falls back on timeouts. But if you have timeouts there are far simpler and more efficient solutions. FWIW: FLP is a silly "theorem" that says "if you can't tell the difference between a system that has crashed and one that is slow - why then you can't tell the difference."
  - ahelwer 7y ago
    Paxos livelocks in a very unstable state which requires multiple independent nodes to sent specific messages at specific times. If you add random intervals between retries, the probability of staying in a livelocked state quickly grows astonishingly low.
    - vyodaiken 7y ago
      I wrote a little simulation. Paxos rarely gets stuck with a small number of proposers/acceptors, but jams up solid once you get to, I forget, 10 or 20. Here it is: https://www.yodaiken.com/wp-content/uploads/2016/10/paxos.ptpx_.ppxt_.png https://www.yodaiken.com/wp-content/uploads/2016/10/paxos.pt... Embarrassingly badly written Lua code for the simulator https://github.com/yodaikenv/consensus https://github.com/yodaikenv/consensus The key to me is that once you accept the need for leader election, you have much simpler alternatives and can toss away the rest of paxos.

sabujp 7y ago

paxos is used heavily in cloud spanner, also tldr; https://youtu.be/8-Bc5Lqgx_c?t=4494 https://youtu.be/8-Bc5Lqgx_c?t=4494 , it's also interesting to watch two mathematicians go at it : https://youtu.be/8-Bc5Lqgx_c?t=4902 https://youtu.be/8-Bc5Lqgx_c?t=4902

sabujp 7y ago

there's a tla video course by lamport : https://www.youtube.com/watch?v=p54W-XOIEF8&list=PLWAv2Etpa7AOAwkreYImYt0gIpOdWQevD https://www.youtube.com/watch?v=p54W-XOIEF8&list=PLWAv2Etpa7...