Hacker News Reader

Comment by ahelwer | Hacker News Reader

I guess I'm pretty opinionated about this, but it was odd the author talked about the necessity of changing the way you think without also including anything about TLA+. IMO the "way you think" about distributed systems - if you want to be effective - will basically end up looking exactly like you think when writing a TLA+ spec, and learning TLA+ is a fast-track method of thinking like a distributed systems engineer. This is much, much more important in day-to-day work on distributed systems than knowing how a bunch of distributed systems algorithms work.

View on HN

Is it though? The hard part about distributed systems is performance in our crappy real world environment with unreliable poorly performing and faulty public internet, unreliable hardware, OSes, etc. Which is directly at odds with needing TLA+, because if you do need it, it means the complexity of the algorithms is so great, that you won't be able to keep them in your head and understand every aspect of their performance to make something work well. It's similar how people think they can just peek a random consensus algorithm they've heard is correct and easy and make a decently working distributed storage, which is silly of course, it's only good for educational purposes.

EDIT: (Ah, I see you are a TLA+ promoter, that's why you made a comment like that)

I think the hard part about distributed systems is the combinatorial explosion of possible system states, which is also common to any concurrent program. Really distributed systems is just concurrency on hard mode, where failures are basically guaranteed instead of being very rare.

I wouldn't particularly say I'm a TLA+ promoter (it's a FOSS project), any more than anyone who has a great fascination with a language/framework/algorithm/viewpoint is a promoter. We're all promoters of the memes that live inside our heads!

I am not a "TLA+ promoter" but think it is a very valuable tool for anyone building distributed systems. The value of TLA+ is that it forces you to carefully consider your algorithm, which is certainly important if the algorithm is complex but equally important if the algorithm is simple. Most people will struggle to correctly specify even a simple algorithm in TLA+ because they will miss a lot of things they had assumed without ever thinking about.

Real world systems need to handle all the things you mention. TLA+ helps you consider all these issues with spelling them out individually. There is no point in building a complex system if you haven't taken the time to validate the correctness of the target system in the first place.

> Which is directly at odds with needing TLA+, because if you do need it, it means the complexity of the algorithms is so great, that you won't be able to keep them in your head and understand every aspect of their performance to make something work well.

I don't think this is correct.

What TLA+ allows us to do is be more creative in our design and choice of algorithms, while allowing the computer to help us reason about whether the choices we're making still result in a system that is correct. "Correct" in in this context means two things: "safe" as in it doesn't lose or corrupt data, and "live" as in it eventually makes progress without deadlock or other blockers. That doesn't capture "meets the SLA" or "fast enough for real use" or even "tolerates gray failures". All of those are critical properties indeed - but unless you have fundamental safety and liveness you're never going to get those properties anyway. You might think you have them, but then you'll have a bad time eventually.

So TLA+ (and similar tools) aren't a complete solution to the problem, but they are an exceptionally useful one. Fundamentally, they're useful because distributed and concurrent protocols, even very simple ones like 2PC, are wickedly difficult to reason about clearly. Computers can help us reason, and specification languages can help us communicate clearly about our reasoning.

That's the thing, performance should dictate the algorithms, not the other way around and TLA+ can't make this process any easier, only harder. I get it's not the case at AWS, where distributed services AWS thinks customers might want is what dictates the choices, but this is an exception, not the rule and unless someone wants to work there they have no reason to be doing it this way, especially not for educational purposes learning distributed systems.

Correctness dictates algorithms. That's what TLA+ helps you with.

But TLA+ is used to shorten development and help with algorithm performance.

> performance should dictate the algorithms, not the other way

You want correctness first, and performance second. But these two are very much intertwined. And knowing exactly where the boundary is will help you co-design them.

Some AWS engineers have said the following[1]:

"TLA+ [...] giving us enough understanding and confidence to make aggressive performance optimizations without sacrificing correctness."

[1] https://blog.acolyer.org/2014/11/24/use-of-formal-methods-at...

Having used TLA+ for years, I would say it's the exact opposite. All bugs happen due to someone believing something is simple enough to work out in their head while it actually isn't. So if your judgment about what you can keep in your head is good, you never have any bugs and you really don't need TLA+. But if you do happen to have bugs occasionally, then your belief about how much you can keep in your head is sometimes wrong. TLA+ is a very quick way to write down what's in your head so you can think about it more rigorously. Surely, if you can truly keep it in your head, it should be easy for you to write it down precisely. And just in case you're wrong, there are tools that can check if you're right, just to be extra sure. In short, TLA+ helps if you ever have bugs. It doesn't help if you never do.

Reply on news.ycombinator.com