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.
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).
[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.
There are lots of very large Coq code bases that work just fine with code extraction. Scalability of extraction isn't the problem.
Is it really true that TLA scales to large programs? Why isn't there a Compcert in TLA? Why isn't there a Flyspec in TLA? And how about stuff like CertiGrad, where just the spec is pretty involved?
My impression has always been that Coq/HOL scale and TLA-style systems break down once your spec gets big enough (let alone the impl).
> There are lots of very large Coq code bases that work just fine with code extraction. Scalability of extraction isn't the problem.
The largest programs ever verified end-to-end with Coq, Isabelle, or any other proof assistant correspond to about ~10KLOC of C, or less than 1/5 of jQuery (although such a small program could require up to 50K or even 100K lines of proofs). And even those certainly-non-trivial-yet-rather-tiny programs took years of efforts by experts. Moreover, concessions in the programs' design and choice of algorithms had to be made in order to make verification feasible at all.
And I agree that extraction doesn't suffer from a scalability problem. What does is the ability to verify the spec in the first place. If we could write proofs that correspond to programs with 100K, then extracting an executable would not be the isse, but we can't (or, at least, we don't know how).
> Is it really true that TLA scales to large programs?
Yes. Again, there's no magic: we can only verify so many lines of a formal spec (of which code is an example). So it's either a small program or a small high-level spec that corresponds to a large program. No known technique can affordably verify large (or even medium, or even non-small) programs, end-to-end, for arbitrary functional correctness properties.
> Why isn't there a Compcert in TLA?
There are programs fifty times the size of CompCert that used TLA+ (to be honest, most real-world programs are 50x the size of CompCert), but not for end-to-end verification; i.e. there is an informal translation of spec to code. Unlike Coq, which is usually used for research or by researchers, TLA+ is used in industry and by "ordinary" engineers without lengthy training in formal logic, so there aren't many papers written about its use, but here's one[1]. Ironically, another reason you don't see as many papers about verification in TLA+ as in Coq is that its use is much simpler. I once saw a paper about specifying and verifying a program's time-complexity in Coq. No one would ever write such a paper about TLA+, because it's just too easy; a TLA+ beginner could do it in their first week of learning (the main reason there's a paper about using TLA+ for PharOS is because they used TLAPS, the TLA+ proof assistant, rather than the TLC model checker, which made the work academically interesting).
In any event, if someone is interested in using any of those tools "in production," I recommend they give them all a try.
Thanks, that's clarifying. You can do this sort of "lightweight" verification in basically any theorem prover. The difference you observe sounds like a difference in community emphasis rather than capability?
There is one big difference in tooling: Coq doesn't have a good model checker. While you can verify several thousand lines of code/spec, writing proofs for those could take months or years, while model-checking is pretty much pushing a button (and then letting the computer or cluster work, possibly for hours or even days), and you probably need to do this a few times, but the difference between having a model checker and not is often the difference between practically reasonable and not. TLA+ has a proof assistant, but people who use TLA+ in industry hardly ever use it because the small added confidence is simply not worth so much more work.
TLA+ does have things that make it hard for you to modularize and reuse pieces of it in the large.
The first category of problems deal with tooling. TLA+ doesn't have a great story when it comes to automation. There is no package manager. Version control is trickier than it needs to be (it's not obvious what files you might want to commit to git and which you shouldn't when you first start working with TLA+). There isn't a lot of support for automatically running things at the commandline (the community mostly uses the TLA+ toolbox, which is a GUI-based IDE). You can and people do these things, but they feel like distinctly second-class citizens. Really TLA+ feels tied to the TLA+ toolbox, warts and all.
The second problem is language support. TLA+'s main way of breaking down problems into modules and then using one module as an interface for another (its notion of refinement) suffers from problems analogous to the ones faced when dealing with inheritance. In TLA+'s case, it is easy to add additional new states into a state machine defined in another module (this is TLA+'s celebrated idea of stuttering), but is rather more annoying to do the opposite, e.g. show that in your new module a single state is meant to correspond to a two states in another module (e.g. you have a transaction primitive that allows you to assume that two states can be done simultaneously).
This is complicated by the fact that the easiest verification technique in TLA+ is model-checking, which fares the worst when dealing with transitive chains of logical implication. TLA+'s model checker does not have a native notion of logical implication. Instead the way you e.g. prove the statement A => B is by effectively proving A and B but privileging A to be the search space that the model checker operates in. This means chains of the form A => B, B => C, C => D and therefore A => D (and all the intermediate stages) are somewhat annoying. You either prove each step with separate models along the chain and just let a human infer that this means A => D, or you prove the statement A => (B and C and D), without using any of the intermediate implications.
Without robust support for transitive implication, the option of using composition in the traditional composition vs. inheritance debate becomes much less palatable as an option when it comes to inheritance.
To some extent this is a limitation inherent in model checking and goes away with the proof based verifier for TLA+ TLAPS. But there isn't a collection, that I know of, of proved theorems for TLAPS like many other theorem provers.
I suspect again this is due to both the lack of a package manager in the TLA+ ecosystem as well as some not so ergonomic parts of TLAPS. TLAPS feels very magical. Its main way of proving things is what's often referred to as sledgehammer or auto in other theorem provers; write the next step in your proof and hope the computer is smart enough to infer it from the previous step. It feels magical when it works. When the computer can't figure something out, it can be a huge pain to figure out why. It doesn't feel like I'm mechanically building up a proof so much as it feels like I'm playing a guessing game with the computer to see which leaps of logic it'll accept. This gets better with time as you develop an intuition of which leaps work and which don't, but can still be painful. This is mainly because TLAPS itself isn't a prover, but rather delegates to the "magic" methods of other provers.
Finally set theory and first order logic, the theoretical basis of TLA+, sometimes makes showing equivalence between items (which is vitally necessary when dealing with code written by multiple individuals who might use different encodings for the same idea) very difficult. In particular, trying to use the fact that A is equivalent to B, therefore some predicate P has an exactly analogous P' on B is tricky. Another way of stating this is that TLA+ as a language makes it a bit difficult to leverage isomorphisms and homomorphisms to reduce the amount of work you have to do. This is somewhere where alternative logical systems can have a big leg up.
All that being said, among the technologies commonly referred to as "formal verification," I would say that TLA+ is the one I would most commonly recommend to people in business situations. This precisely because of what many people view as a flaw, that TLA+ is a formal specification language and not a way to actually write or verify actual running code.
Because TLA+ specs are divorced from your codebase, they require far less buy-in to see dividends. You don't have to rewrite your codebase in another language. You don't even have to change your coding practices.
Indeed TLA+'s closest competitor on most teams is also precisely what most teams lack, which is high-quality documentation.
This means you can integrate TLA+ into your work with extremely little risk. Try formalizing your mental model in TLA+. See if it reveals interesting conclusions. If it does, congratulations! TLA+ has been useful to you and you can keep it around as an artifact detailing your thoughts in the future. If not, delete your specs and no harm no foul. No code depends on its existence. You don't need some lengthy transition period to migrate systems away from "using" TLA+. You lose no more time than the amount you put into writing your spec.
> The first category of problems deal with tooling. TLA+ doesn't have a great story when it comes to automation. There is no package manager. Version control is trickier than it needs to be (it's not obvious what files you might want to commit to git and which you shouldn't when you first start working with TLA+). There isn't a lot of support for automatically running things at the commandline (the community mostly uses the TLA+ toolbox, which is a GUI-based IDE). You can and people do these things, but they feel like distinctly second-class citizens. Really TLA+ feels tied to the TLA+ toolbox, warts and all.
I currently see this as the biggest barrier to widespread adoption. Not the only barrier, but the biggest by far. A modernized CLI + exportable traces would make a huge difference.
> you to modularize and reuse pieces of it in the large.
There is no such thing as formal specifications "in the large." The largest software specification ever written in any language that could be fully verified is no more than a few thousand lines (although proofs can be very long). Having said that, I think TLA+ module system is fine; reminds me of ML.
> The second problem is language support. TLA+'s main way of breaking down problems into modules and then using one module as an interface for another (its notion of refinement) suffers from problems analogous to the ones faced when dealing with inheritance.
I don't think so, but if you're modularizing your specs you may be doing something wrong.
> but is rather more annoying to do the opposite, e.g. show that in your new module a single state is meant to correspond to a two states in another module
Right, but the problem here is fundamental. Verifying temporal quantifiers is co-NP-hard in the number of states.
> This means chains of the form A => B, B => C, C => D and therefore A => D (and all the intermediate stages) are somewhat annoying.
Yes, but still about 10x less annoying than writing proofs. :)
> Without robust support for transitive implication, the option of using composition in the traditional composition vs. inheritance debate becomes much less palatable as an option when it comes to inheritance.
Again, using composition is a hint that you may be doing it wrong.
> But there isn't a collection, that I know of, of proved theorems for TLAPS like many other theorem provers.
Deductive proofs are currently not a viable verification approach in industry (except in some small niches, and/or to tie together model-checking results), so libraries of that kind are mostly useful for researchers who research formal mathematics or deductive verification; that's not exactly TLA+'s target audience. Other proof assistants are used almost exclusively for research or by researchers so they're optimized for that.
> This is mainly because TLAPS itself isn't a prover, but rather delegates to the "magic" methods of other provers.
That's not why (you can choose specific Isabelle tactics in your BY clause). The reason is that the TLA+ proof language was designed to be declarative. I guess some people prefer a more imperative style.
> Another way of stating this is that TLA+ as a language makes it a bit difficult to leverage isomorphisms and homomorphisms to reduce the amount of work you have to do. This is somewhere where alternative logical systems can have a big leg up.
There are many things in TLA+'s design that make deductive verification harder, and many things in other language's designs that makes deductive verification harder. There is no one best way to do this.
I think the difference is that TLA+ was designed not for research but for industry use, and so its preferences take into account what's feasible. There is no point making something that few people would do easier at the expense of making something many would do harder.
> Because TLA+ specs are divorced from your codebase, they require far less buy-in to see dividends. You don't have to rewrite your codebase in another language. You don't even have to change your coding practices.
... And because there is no tool in existence that can verify those systems at the code-level anyway, so it's not like there's any other option. You get ~2000-5000 lines of formal spec. You can use them for code and get a tiny program or for a high-level spec formally "divorced" from your code.
There is formal specification in the large if you count formal mathematics. Mizar's library of formalized mathematics is easily millions of lines if not tens of millions of lines at this point. There are individual formalized mathematics repositories in other languages (Coq and Agda included I think? It's been a while since I looked into that) that run into the hundreds of thousands of lines of code.
So there are pointers as to how to organize formal specs for extremely large projects.
The reason as far as I can tell for why there aren't large software verification projects as opposed to pure formal math is that the cost benefit analysis is wildly out of whack. It makes essentially no business sense to try to formally verify things past several thousand lines. This doesn't seem like a bright line to me though, e.g. that there is a technological inflection point at several thousand lines that prevents further scaling. Again formal mathematics repositories are a counterexample. It's just that because of the high cost of formal verification, there is a business ceiling at the equivalent of man hours willing to be spent somewhere in the vicinity of hundreds of thousands of lines of unverified code to millions of lines of unverified code and you can rapidly exhaust that budget with full formal verification (which can easily account for orders of magnitude increases in time spent).
Ah thanks for the TLAPS repo. I forgot about the library, but even there I'm not seeing a lot of reuse in it. There's some of it, but not a lot. Maybe just because users of TLAPS are far fewer than users of TLC.
Indeed you can choose specific Isabelle tactics in your BY line. In practice I'm not sure I've ever seen it in any TLAPS proof. I've very very briefly played with that functionality and at first glance it seems much more difficult than using Isabelle directly because of the added layer of indirection. If you have one in the wild, I'd love to take a look to learn from.
I definitely agree there is no one way to do things. I've left out all the things that I think TLA+ is fantastic at. I think it's the closest thing to mathematics that can be practically used in industry. Far more so than the rhetoric you usually hear about FP languages, TLA+ is immediately familiar to anyone with a pure mathematics background, both syntactically and semantically. TLA+, unlike something like Agda, also has a fairly straightforward set of semantics and mathematical grounding in its theory. The benefit of writing each spec from scratch allows them to be independently understandable with no need to understand the idiosyncrasies of arcane libraries or frameworks.
But I do think it has problems with modularity. My state example wasn't to do with the difficulty of verification or the explosion of the state space (which honestly don't bother me, my TLA+ specs are often exponential or worse wrt model checking time in the size of my constants, but I still get a lot of mileage out of them), but rather the difficulty in even expressing that idea. When I'm confronted with wanting one state to stand in for two I often have to resort to using two separate specs, one with fewer states and then the other being the original spec and then showing my new spec fulfills both. I think the modularity problems mostly stemming from tooling and language choices, but a little bit from theory (although Mizar is also set theory based). For example I don't think I've ever used a 3rd party module in a TLA+ spec I've written. Even trying to express the equivalence between two specs that just use different strings for the same states can be tricky. Wouldn't it be cool if people could import Lamport's Paxos spec directly into their own specs of their own systems? Or any other specs someone has written specifying one part of their system? That would be pretty awesome if there was something akin to an NPM repository of all these specs for various algos that you could import into your own spec. The tools for this exist in Mizar. They do not for TLA+.
Turning my attention back to deductive verification rather than the expression part of the equation, more specifically for TLAPS, I'm actually not a fan of the imperative tactics that are found in Coq. But an error message better than what amounts to red highlighting and "no" would be nice in TLAPS. Something where you can mix YOLOing with more hands-on proof building, with tactics, functions, or even just a trace of the constraint search would be great.
I think the idea that you have some limited thousands of line to "spend" is a useful bit of intuition. One knob you're leaving out though is the richness of the properties you're trying to prove. As you decrease the richness of the properties you can prove you can drastically decrease your burden. This starts bleeding into static analyzers and then if you dial the knob even further down into mainstream type systems. But the knob can be fairly low and still be useful.
For example absence of crashing/abnormal exits is something that is feasible to prove on very large codebases. It's hard to do completely end-to-end (even CompCert's front-end isn't proven), mainly because of the difficulty of fully modeling stuff like filesystems, but can be done for modules spanning hundreds of thousands of lines of code. It is of course a weak property. That the program does something is nowhere near the same thing as doing the correct thing. But it is nonetheless a very useful one.
Absence of SQL injection attacks and CSRF attacks are other examples (can be done either by external analysis or by leveraging language level features), although those feel a bit more like cheating since you basically cleverly restrict the amount of code that "matters."
That would be the closest to an alternative to formal specifications I could suggest. I still think formal specs are lower risk because this still requires coding in certain styles amenable to this static check (or languages that enforce it).
> There is formal specification in the large if you count formal mathematics.
Sure, but TLA+ is not aimed at research. The biggest problem, by far, plaguing not just proof assistants but formal logic in general, pretty much since its inception, is complexity. Which is ironic because the entire purpose of formal logic -- from Leibniz's original dream to Frege's early success -- is to be simple, clear and easy tool for practitioners. Compared to the dismal failure of formal logic in achieving that (which was acknowledged and lamented by the likes of von Neumann and Turing, but has since been shrugged off even though the problem has gotten considerably worse), I think the fact that people who are not trained logicians use TLA+ to do real work makes it a crowning achievement not only in software verification but in the history of formal logic. To achieve that, TLA+ had to shed away everything that isn't absolutely necessary. Lamport once said after hearing a lecture about some proposed addition to TLA+: "it's taken you 6 months to add something to TLA+ that it had taken me 15 years to remove".
> It makes essentially no business sense to try to formally verify things past several thousand lines.
Well, we don't know how to do that in a way that would be feasible; I consider that a "limit" because the software we use and need is very commonly three orders of magnitude ahead of what deductive verification can handle. And the gap has been constant or even growing for the past 40 years or so.
> Again formal mathematics repositories are a counterexample.
I disagree. Formal mathematics is about taking years to prove a proposition that could be written in one or a couple of lines. I think that the resemblance between deductive mathematical proofs and deductive software verification is like that between painting the Sistine Chapel and painting a large hospital. The similarity is superficial.
> If you have one in the wild, I'd love to take a look to learn from.
> But I do think it has problems with modularity. My state example wasn't to do with the difficulty of verification or the explosion of the state space ... but rather the difficulty in even expressing that idea.
Can you DM me on Twitter (get there from the about page of my blog: https://pron.github.io) or send me an email (my name at Google's mail service)? I'm curious to see the problem you're referring to.
> Wouldn't it be cool if people could import Lamport's Paxos spec directly into their own specs of their own systems?
Well, I don't yet understand the exact issue you're having, but no, I don't think that would be particularly helpful at all, for the following reason: If people wanted to modify Paxos itself, they can get their hands on Lamport's spec and tinker with it. If they want to use it as a component, then they can write an abstraction of it in a few line. All of TLA+ is about the abstraction/refinement relation (that is, IMO, what makes its theory cooler than Coq et al. for software).
> But an error message better than what amounts to red highlighting and "no" would be nice in TLAPS.
Yep.
> One knob you're leaving out though is the richness of the properties you're trying to prove. As you decrease the richness of the properties you can prove you can drastically decrease your burden. This starts bleeding into static analyzers and then if you dial the knob even further down into mainstream type systems. But the knob can be fairly low and still be useful.
Right, but we know more than to say it's just richness. We know exactly what kind of properties scale (through abstract interpretation, of which both type systems and static analysis are examples): inductive (= compositional) ones. I.e. a property such that if it holds for any state (whether or not reachable by the program), then any step in the program preserves it, or, alternatively, a property P, such that P(x) and P(y), where x and y are terms, implies that P(x ∘ y). Problem is that most functional correctness properties are not inductive/compositional for the language (i.e. that the above two description hold for any term in the language).
> That would be the closest to an alternative to formal specifications I could suggest.
I think that's one additional tool. But a knob that's easier to turn is soundness. The difference between verifying a property to 100% certainty and to 99.999% certainty can be 10x in cost, and as -- unlike mathematics -- an engineer is not interested in the correctness of an abstract algorithm but in that of a physical system that can always fail with some nonzero probability -- absolute confidence is never strictly a requirement. Of course, this is not just my opinion but it also seems to be that of many formal methods researchers, which is why concolic testing is such a hot topic right now.
I think that specification and verification must be separate -- i.e. you specify at any "depth" and then choose a verification strategy based on cost/benefit (so, no to dependent types), and in most cases, it's possible that concolic testing would be enough.
1. The very large Coq/Agda texts are usually large because of the proofs, not the specification/propositions. There's a 5-10x ratio, if not more.
2. I don't think that TLA+'s theory is intrinsically more "straightforward" than Agda's, even though it's certainly more familiar (I know some people who would insist that type theory is more straightforward than set theory). I think that a lot of work has gone into making TLA+ relatively easy to grasp; I think it's more design than a specific choice of theory, although the choice of theory certainly affects the design. In addition, as I've already mentioned, I think that TLA itself (i.e. not the set theory in the "+") is a particularly beautiful theory for talking about computation and discrete systems, that has some obvious advantages over the lambda calculus; in particular the abstraction/refinement relation that's the core of TLA (the semantic domain of TLA is a Boolean lattice where the less-than relation is behavior refinement).
Thanks for the detailed answer. I can see immediate value of TLA+ in helping you clarify your high-level thinking about the system and finding bugs in it. Maybe the problem is the expectation that "verified by formal methods" is some magical stamp of approval that makes your program bug-free, when in reality it is just one of many tools to make your program better.
Exactly! (Except formal methods are not one but many methods and tools that are as different from one another as code review is from testing. Also, I wouldn't call TLA+ a "lightweight" formal method despite being relatively easy to learn and to apply; it's hard to get more heavyweight than TLA+.)
While we’re on the subject, I think it’s worthwhile to explain the name “formal methods”, and especially “formal” (methods just means techniques, in our case techniques for software verification), as I’ve seen people constantly misuse it.
Formal means mechanical, i.e. doable in principle by a computer (sometimes we say doable or checkable by a computer, but the two are equivalent from a computability perspective though not from a complexity perspective). So when you say you have a formal proof that does not mean you have a mathematical proof, but a proof that can be verified by a computer. Then why do we say "formal" instead of "mechanical"? Because the word formal was used for centuries before Alan Turing discovered that it is equivalent to "mechanical." The main idea of symbolic logic is that of the formula, or logical form; a sentence whose truth can be derived by the direct manipulation of its form (syntax) without any use of intuition or understanding. So, to this day, when we talk of things making use of symbolic (or formal) logic, we say formal rather than mechanical.
Now, if formal means mechanical and methods means techniques for software verification, are testing and type checking — both software verification techniques that are carried out by the computer — formal methods? Technically they are! But formal methods is also the name of an academic discipline, and so formal methods usually refers to whatever it is that people who research formal methods study, and type checking have not traditionally been a part of that discipline. What’s interesting that both of them — or, rather, certain forms of them — are now actually part of formal methods research. A few formal methods researchers study dependent type systems, type systems that can express a far richer set of program properties than simple type systems, and the study of concolic testing, a combination of symbolic and abstract interpretation/model-checking and concrete (i.e. “normal”) testing is a very hot topic in formal methods research at the moment. What's common to all topics in formal methods research is some use of formal logic.
I've not been involved with formal methods for 15 years (at what is now Altran UK) so I'm rather rusty.
Wasn't B an attempt at bridging the gap between specification and implementation by a process of gradual refinement, with each "layer" being record and verified? I only touched it while at uni, so I don't remember any of the details of how that was supposed to work. Did that ever go anywhere?
I don't know B, and I think you are correct, but it, too, doesn't break the "scalability barrier". It would allow you to generate small programs by a process of refinement, but not very large ones. I think it is aimed mostly at safety-critical realtime embedded systems (and I believe it's used mostly for railways), so it's extremely useful (like other model-checked languages for that domain, like SCADE), but not something that can significantly help mainstream software.
Absolutely, none of the current formal methods approach scale to the level of much commercial software. Much of the systems engineering work that we did at Altran was focused on minimising the extent of the system that would need the higher levels of verification. So flow analysis and absence of runtime error proofs were commonplace, but proof of correctness against the spec was something that was much more focused on specific very high integrity components.
I remember thinking that B was a heck of a lot of work for event the smallest projects. I'm kind of surprised that it's still being used.
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.
I earnestly believe that "Paxos is impossible to understand" is a baseless meme, a sort of learned helplessness in the CS community. I understand Paxos perfectly well. You can see it all laid out there in the TLA+ spec, and explained in many videos. It is absolutely untrue that only Lamport understands Paxos.
I'm sure many people understand it. I personally find it very hard to fully understand, and "Paxos Made Simple" didn't help. About one year ago, I went through all the steps of the proof, I implemented it. I really tried to understand it. Today, without external reference, I probably wouldn't be able to implement it again. For such a short piece of code, it's surprisingly difficult.
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
Great quotes and wow, is that a link worth following! If you’re reading this and haven’t gone to read more of the wisdom in taoup but you liked what’s above, I urge you to go do so now.
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.
Viewstamped replication came first, and defined the same core replication mechanism as paxos. but it was presented in the context of a replicated database system, together with a bunch of other stuff. Lampport's analysis of the core algorithm caught people's eyes -- with some amount of marketing on his part, and possibly because it was much more clearly focused on just the consensus problem, which made it somewhat more friendly as a theoretical building block.
rather, he pioneered many of the fundamental techniques that underlie both viewstamped replication and Paxos (and a boatload of other things; it was a very well-deserved award!) But Barbara invented the actual consistent replication algorithm first.
and yes, raft is in many ways a restatement of viewstamped replication. The thing that makes both of them a better pedagogical basis is that they present the common case of having a working master direct replication, and then handle the failure case explicitly. It ends up being exactly the same thing that multi paxos does, but for most people, it ends up being a much more intuitive way of thinking about the system and algorithm.
Or, at least that's been my experience in teaching it for 15 years.
> But Barbara invented the actual consistent replication algorithm
Do you know anything about Brian Oki's subsequent career? I was curious as to what he did after his VSR thesis and found a '93 paper of his (The Information Bus [1]). Interesting to see again he was a bit ahead of his time, this time anticipating 'Eventual Consistency'.
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.
The Raft paper has a full section on understandability, and comes with a TLA+ spec.
I am baffled that a serious effort at producing papers that are understandable and implementable is dismissed as a “social phenomenon”. Deliberately obscure papers are bad, sloppy science, not a clever signaling mechanism.
As pointed out elsewhere in the conversation and indeed in revised editions of the Paxos paper, it does not even break new ground and is equivalent to the earlier view management protocol.
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.
I find that the core of Paxos (the Synod protocol) is very easy to understand - it is literally just two exchanges of messages! The tricks that you need to add to go from the Synod protocol and get an actual production implementation of the replicated log are another matter, the original paper only hints about some of them. There is e.g. the Paxos Made Live paper (link: https://www.cs.utexas.edu/~lorenzo/corsi/cs380d/papers/paper...) that has more on this topic.
BTW Paxos also has a leader - this is what makes these protocols efficient. They need only the linear number of messages instead of the quadratic "everybody talks to everybody" design.
>BTW Paxos also has a leader - this is what makes these protocols efficient.
That's the funny part of Paxos. Paxos is specifically sold as a multi-proposer protocol. The most subtle and hard to understand part of the protocol is the clever 2 phase proposal election with value inheritance. But it's all pointless because in order to make the system work you need a single coordinator you elect using timeouts or reliable message protocols.
> BTW Paxos also has a leader - this is what makes these protocols efficient. They need only the linear number of messages instead of the quadratic "everybody talks to everybody" design.
Okay, but again, this means that the leader is the bottleneck. In that case, I'd want the leader to be on beefier hardware than the other machines, and to not serve up any read requests, so all of its resources are devoted to leading. In order to accommodate this, you'd want to elect leaders from a pool of leaders which have the beefier hardware. And at that point, since you're only talking to the leaders when you write, rather than talk through to the leaders through the extra latency of the followers, just write to the leaders directly. And then at that point this looks suspiciously like the leaders are a sharded database and the followers are caches. Am I missing something?
Word on the street is if you really really try to understand Paxos you will find that its much more nuanced and complex than raft. Many have tried, but failed.
I think the answer is that in the late 80s/90s, academic CS decided that the important topics in this area centered on completely asynchronous networks. The super famous, but trivial, FLP "theorem" gave a respectable foundation for work in the area (even though it pretty much says, you can't get anywhere with a completely asynchronous network). There was a lot of very interesting work prior to this period that was just discarded. For example Liskov's paper on using timeouts
Viewstamps depends, implicitly, on timeouts. You send a message a number of times and if you don't get a response, you abort. In the completely asynchronous world, there is no way to do that.
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.
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.)
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) 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) is much more clear.
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.
We could start making things more intuitive and understandable by realizing not everyone on this site is versed in the same technology, and thus we should spell out/explain our acronyms and technical lingo before using them.
Data Science? Distributed Storage? Distributed Systems?
I'm starting with a book designed to teach kids Apache Spark using garden gnomes ( http://www.distributedcomputing4kids.com/ ) and depending on how that goes I want to branch out and do some other topics.
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.
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.
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.
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].
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!
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.
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.
At the very beginning people actually would not understand the value of the algorithm.
This comes from Lamport himself, after having colleagues read the paper he asked them if they new a such and such distributed consensus algorithm and they could not think of one.
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.
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.
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.
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).
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?
It's super simple. You have a network where sometimes messages don't get delivered. One agent (process, site ... ) sends a message m to a collection of other agents distributed around the network. How can the sender be sure that at least some number of the intended recipients got the message. This is what databases do with commit protocols. Essentially the same problem is generalized for so-called distributed consensus protocols - of which Paxos is a very complicated example. The simple solution is that the sender keeps sending either until a timeout happens or it gets ack messages from whatever number of recipients it needs to be sure got the message. That's it. If the recipients are executing a deterministic state machine and the messages are the inputs to that state machine, you can be sure all the ones that have received the same messages in the same order are in the same state.
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.
To add context, Paxos allows you to have the the same state across multiple servers without any manual master/replica failover, with allowances for a minority of the servers to go down due to upgrades or failures and with clients getting the same results no matter which of the servers they connect to. (In distributed systems this is called Consensus.)
It's used in distributed datastores like Zookeeper and Exhibitor, which are used in situations where you need both consistently and as close to zero downtime as possible. It also influenced Raft, a similar but simpler algorithm to accomplish the same goals. Raft is used by etcd, which is the database that powers Kubernetes.
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.
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)
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."
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.
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:
This is authentically a very interesting simulation and I would be interesting to see a writeup if you have one. I will say that you only have multiple proposers if the proposers cannot talk to one another, as otherwise they would be silenced by any simple leader election protocol (heartbeats + node rank, etc.) It's true that the leader election protocol is not part of paxos per se but all implementations will have one, and the protocol livelocks in the unusual case where there's an enduring network partition and the multiple proposers are sending messages with specific timing.
Edit: I took a look at your post[0] and it is interesting. I'll take a look at CM.
stage 1: elect a single coordinator (which you have to do with paxos anyways)
stage 2: the coordinator sends each message over and over until it has accepts from 51% of acceptors or it times out and starts a reformulation of the acceptor set
If an acceptor does not receive a message from the coordinator over a sufficient period,it times out and tries to trigger a new coordinator election
Coordinator election: try for t time units to get a majority of acceptors to accept your proposal to be coordinator. give up on timeout or notification that there is a running coordinator.
This is the simplest method and not the most efficienct, but it is both live and safe.
Chang/Maxemchuk propose to make stage 2 more efficient that acceptors be arranged in a cycle and messages from the coordinator be numbered sequentially. Then each acceptor takes a turn to broadcast its accept but only does it if it has seen all prior (lower numbered) messages and their accept message responses. on each cycle completion, the coordinator can commit the first message in the cycle.
If the leader fails, the next leader needs to know the values the acceptors have already accepted in order to propagate the previously chosen value, if any. I assume this happens in your election phase. Since we only want to talk to a majority of acceptors during the election, we need a way to order the values proposed by different leaders (ballot number). Without that, we'd need to receive responses from possibly all acceptors, which would break liveness. Once the leader has proposed a value at a ballot number, acceptors need to not accept values from older ballots, otherwise the old leader, having woken up from a nap, could just overwrite the chosen value. So in filling in the not specified portions of your algorithm in the simplest way possible to make it work, we've just described paxos.
I will have to read the Chang-Maxemchuk paper, I have not heard of that before.
The key is to decide whether timeouts work in your network. If timeouts don't work and you don't have some reliable message protocol, then nothing works. If timeouts do work, then a completely simple obvious brute force algorithm works. In this algorithm, we have leader/coordinator election. The leader then polls the acceptors for the highest sequence number of a committed message and recovers all missing messages. Then the leader starts sending new messages - increasing the same sequence number. The old leader, if it recovers should know that its lease as leader has timed out, but if it does not it cannot get acks from a majority of acceptors for a new message because a majority have signed on to the new leader. There is no "value" competition - only a competition for the id of the new leader during leader election. We don't need Paxos at all.
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.