6 ms·

Using TLA+ to Model Cascading Failures

98 points by mbellotti 8y ago

tluyben2 8y ago
I have been modelling parts of our systems in TLA+ for years now and it really helps a lot working out complex scenarios.
- Leace 8y ago
  I'd love to read about that in detail. Are there any publicly available documents you could share?
  - tluyben2 8y ago
    I am hoping to find the time to write something, preferably a (free) book; I think I might find the time this summer for that.
    - Tomte 8y ago
      When you decide to start, collect mail adresses of interested readers. Don't just assume people will stumble upon your book, seek out readers long before the book is finished. I recently told this on Twitter to an Academic who had just finished writing a book on Cryptography in middle-age Venice (how cool is that?), but with publication still many months off. She had never thought about collecting people's mail addresses, even though dozens (if not hundreds) of people replied on Twitter that they'd be interested in reading the book.
      - detaro 8y ago
        > a book on Cryptography in middle-age Venice (how cool is that?), but with publication still many months off. Sounds interesting, link?
        Tomte 8y ago
        Erm, not Middle Ages, Rennaissance, of course! https://www.amazon.de/Venices-Secret-Service-Intelligence-Renaissance/dp/0198791313 https://www.amazon.de/Venices-Secret-Service-Intelligence-Re...
  - Ixiaus 8y ago
    Hillel Wayne[1] has written a bunch about TLA+ for lay programmers like me. I've found his blog posts pretty good, I also bought his book Practical TLA+ which I like. He also wrote the free web book Learn TLA+[2]. [1]: https://www.hillelwayne.com/post/using-formal-methods/ https://www.hillelwayne.com/post/using-formal-methods/ [2]: https://learntla.com/introduction/ https://learntla.com/introduction/
    - lintuxvi 8y ago
      He also runs workshops for teams wanting to incorporate this into their toolset.
  - Twirrim 8y ago
    Anecdotally, the team I was in in AWS needed to build a complicated component, one that, should it get it wrong, would be disastrous for the service. They'd estimated about 4-6 months for a two person team, made from some of the best engineers in the service, focused entirely on it to get it written, tested and out to production. They decided to use TLA+ to model, despite neither engineer having used it before. They lost about a week to getting up and running with it (one engineer's only complaint was how tied in to Eclipse it was), and then spent the res of the month working on and modelling the whole task. It found problems. A whole bunch of them. The fixed the model until finally TLA+ gave them an all clear. Then came the coding. Well... that didn't take very long at all. The TLA+ model effectively outlined all the code and methods for them. The actual programming ended up being almost a cookie cutter simple code. In total, the new and complicated component went from drawing board to tested and ready for production in about 2 months. Despite having had to learn TLA+, it ended up taking less time than if they'd not written the TLA+ models in the first place.
    - baq 8y ago
      Lamport claims on his website that Amazon uses TLA+ and has used it for quite a while now. Saying that to confirm plausibility of this story.
      - Tomte 8y ago
        https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon....
      - Twirrim 8y ago
        Amazon/AWS has published a few white papers about their use of TLA+ and other Formal Methods:http://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf http://lamport.azurewebsites.net/tla/formal-methods-amazon.p.... James Hamilton is a fan of TLA+, and talks about its use in Amazon: https://perspectives.mvdirona.com/2014/07/challenges-in-designing-at-scale-formal-methods-in-building-robust-distributed-systems/ https://perspectives.mvdirona.com/2014/07/challenges-in-desi...
    - 8y ago
usgroup 8y ago
Can anyone advise on whether it’s worth modelling general critical systems in TLA+ where they are not distributed? In broad strokes, how does one make sure that your real system indeed behaves like your model?
- pron 8y ago
  > Can anyone advise on whether it’s worth modelling general critical systems in TLA+ where they are not distributed? Absolutely, and not just critical systems. Any system that is either complex or may have some non-obvious subtleties can benefit from a specification. > In broad strokes, how does one make sure that your real system indeed behaves like your model? In general, TLA+ can be used to specify very large and very complex systems. It is currently infeasible to mechanically verify with absolute certainty that systems of such size conform to a specification, regardless of tools used. The only systems that can be verified to such an extreme extent (called end-to-end verification, namely interesting global properties are verified all the way down to the code, and even to the machine-code level) are very, very small (no more than about 10KLOC), and even then require a tremendous amount of effort by experts. Specifications should be relatively short and clear. They are therefore useful for stating your assumptions about the system, and then checking the consequences of those assumptions. Whether the assumptions are accurate, approximate or wrong can then be verified by inspection -- this is certainly feasible and commonly done in practice. There are also relatively cheap mechanical ways to check that the system conforms to the spec, but not with absolute certainty. One is called trace checking, and its possible use with TLA+ is described here: https://pron.github.io/files/Trace.pdf https://pron.github.io/files/Trace.pdf
  - apta 8y ago
    How common is it to use TLA+ on existing/pre-built systems, to retrospectively try to find issues or bugs in them?
    - pron 8y ago
      It's hard to answer because using TLA+ in general is far from common. But among users, I would say that most cases are where they have an existing system. That was certainly how I first used TLA+ (when I realized there could be deep design issues with a system I worked on; TLA+ showed me that there indeed were two serious problems, and it also verified that my fix was correct).
victor106 8y ago
Anyone here can shed some light on how to incorporate tla+ into an agile process?
- pron 8y ago
  Augmenting Agile with Formal Methods: https://www.hillelwayne.com/post/augmenting-agile/ https://www.hillelwayne.com/post/augmenting-agile/
tunesmith 8y ago
It seems TLA+ would be a really great fit for modeling actor systems, has anyone found good examples of this, for instance for Akka or Erlang?
- polskibus 8y ago
  Akka has testkit and multi node testkit which you can use to test such systems. If you need to explore state space, you can use data driven and or combinatorial testing attributes from *unit libraries.
  - pron 8y ago
    TLA+ and any kind of testing serve different purposes. I don't know how good of an analogy this is, but tests are more like strength tests on a structure, while a TLA+ is like a blueprint.
- pron 8y ago
  It's very easy to specify such systems in TLA+. I think this becomes apparent as you learn it.

98 points by mbellotti 8y ago

I have been modelling parts of our systems in TLA+ for years now and it really helps a lot working out complex scenarios.

Leace 8y ago
I'd love to read about that in detail. Are there any publicly available documents you could share?
- tluyben2 8y ago
  I am hoping to find the time to write something, preferably a (free) book; I think I might find the time this summer for that.
  - Tomte 8y ago
    When you decide to start, collect mail adresses of interested readers. Don't just assume people will stumble upon your book, seek out readers long before the book is finished. I recently told this on Twitter to an Academic who had just finished writing a book on Cryptography in middle-age Venice (how cool is that?), but with publication still many months off. She had never thought about collecting people's mail addresses, even though dozens (if not hundreds) of people replied on Twitter that they'd be interested in reading the book.
    - detaro 8y ago
      > a book on Cryptography in middle-age Venice (how cool is that?), but with publication still many months off. Sounds interesting, link?
      - Tomte 8y ago
        Erm, not Middle Ages, Rennaissance, of course! https://www.amazon.de/Venices-Secret-Service-Intelligence-Renaissance/dp/0198791313 https://www.amazon.de/Venices-Secret-Service-Intelligence-Re...
- Ixiaus 8y ago
  Hillel Wayne[1] has written a bunch about TLA+ for lay programmers like me. I've found his blog posts pretty good, I also bought his book Practical TLA+ which I like. He also wrote the free web book Learn TLA+[2]. [1]: https://www.hillelwayne.com/post/using-formal-methods/ https://www.hillelwayne.com/post/using-formal-methods/ [2]: https://learntla.com/introduction/ https://learntla.com/introduction/
  - lintuxvi 8y ago
    He also runs workshops for teams wanting to incorporate this into their toolset.
- Twirrim 8y ago
  Anecdotally, the team I was in in AWS needed to build a complicated component, one that, should it get it wrong, would be disastrous for the service. They'd estimated about 4-6 months for a two person team, made from some of the best engineers in the service, focused entirely on it to get it written, tested and out to production. They decided to use TLA+ to model, despite neither engineer having used it before. They lost about a week to getting up and running with it (one engineer's only complaint was how tied in to Eclipse it was), and then spent the res of the month working on and modelling the whole task. It found problems. A whole bunch of them. The fixed the model until finally TLA+ gave them an all clear. Then came the coding. Well... that didn't take very long at all. The TLA+ model effectively outlined all the code and methods for them. The actual programming ended up being almost a cookie cutter simple code. In total, the new and complicated component went from drawing board to tested and ready for production in about 2 months. Despite having had to learn TLA+, it ended up taking less time than if they'd not written the TLA+ models in the first place.
  - baq 8y ago
    Lamport claims on his website that Amazon uses TLA+ and has used it for quite a while now. Saying that to confirm plausibility of this story.
    - Tomte 8y ago
      https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon....
    - Twirrim 8y ago
      Amazon/AWS has published a few white papers about their use of TLA+ and other Formal Methods:http://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf http://lamport.azurewebsites.net/tla/formal-methods-amazon.p.... James Hamilton is a fan of TLA+, and talks about its use in Amazon: https://perspectives.mvdirona.com/2014/07/challenges-in-designing-at-scale-formal-methods-in-building-robust-distributed-systems/ https://perspectives.mvdirona.com/2014/07/challenges-in-desi...
  - 8y ago

usgroup 8y ago

Can anyone advise on whether it’s worth modelling general critical systems in TLA+ where they are not distributed? In broad strokes, how does one make sure that your real system indeed behaves like your model?

pron 8y ago
> Can anyone advise on whether it’s worth modelling general critical systems in TLA+ where they are not distributed? Absolutely, and not just critical systems. Any system that is either complex or may have some non-obvious subtleties can benefit from a specification. > In broad strokes, how does one make sure that your real system indeed behaves like your model? In general, TLA+ can be used to specify very large and very complex systems. It is currently infeasible to mechanically verify with absolute certainty that systems of such size conform to a specification, regardless of tools used. The only systems that can be verified to such an extreme extent (called end-to-end verification, namely interesting global properties are verified all the way down to the code, and even to the machine-code level) are very, very small (no more than about 10KLOC), and even then require a tremendous amount of effort by experts. Specifications should be relatively short and clear. They are therefore useful for stating your assumptions about the system, and then checking the consequences of those assumptions. Whether the assumptions are accurate, approximate or wrong can then be verified by inspection -- this is certainly feasible and commonly done in practice. There are also relatively cheap mechanical ways to check that the system conforms to the spec, but not with absolute certainty. One is called trace checking, and its possible use with TLA+ is described here: https://pron.github.io/files/Trace.pdf https://pron.github.io/files/Trace.pdf
- apta 8y ago
  How common is it to use TLA+ on existing/pre-built systems, to retrospectively try to find issues or bugs in them?
  - pron 8y ago
    It's hard to answer because using TLA+ in general is far from common. But among users, I would say that most cases are where they have an existing system. That was certainly how I first used TLA+ (when I realized there could be deep design issues with a system I worked on; TLA+ showed me that there indeed were two serious problems, and it also verified that my fix was correct).

victor106 8y ago

Anyone here can shed some light on how to incorporate tla+ into an agile process?

pron 8y ago
Augmenting Agile with Formal Methods: https://www.hillelwayne.com/post/augmenting-agile/ https://www.hillelwayne.com/post/augmenting-agile/

tunesmith 8y ago

It seems TLA+ would be a really great fit for modeling actor systems, has anyone found good examples of this, for instance for Akka or Erlang?

polskibus 8y ago
Akka has testkit and multi node testkit which you can use to test such systems. If you need to explore state space, you can use data driven and or combinatorial testing attributes from *unit libraries.
- pron 8y ago
  TLA+ and any kind of testing serve different purposes. I don't know how good of an analogy this is, but tests are more like strength tests on a structure, while a TLA+ is like a blueprint.
pron 8y ago
It's very easy to specify such systems in TLA+. I think this becomes apparent as you learn it.