5 ms·

Is it though? The hard part about distributed systems is performance in our crappy real world environment with unreliable poorly performing and faulty public in

by tyu2 6y ago

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)

ahelwer 6y ago
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!
smiths1999 6y ago
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.
mjb 6y ago
> 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.
- tyu2 6y ago
  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.
  - Tomis02 6y ago
    Correctness dictates algorithms. That's what TLA+ helps you with.
  - pron 6y ago
    But TLA+ is used to shorten development and help with algorithm performance.
  - 6y ago
pron 6y ago
> 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. 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.

by tyu2 6y ago

ahelwer 6y ago

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!

smiths1999 6y ago

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.

mjb 6y ago

> 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.

tyu2 6y ago
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.
- Tomis02 6y ago
  Correctness dictates algorithms. That's what TLA+ helps you with.
- pron 6y ago
  But TLA+ is used to shorten development and help with algorithm performance.
- 6y ago

pron 6y ago

> 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. 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.