10 ms·

TLA+: design, model, document, and verify concurrent systems

148 points by lolptdr 7y ago

yingw787 7y ago
Raymond Hettinger just have a talk at PyCon an hour ago about formal reasoning and solvers. There’s a lot of polish in the talk, with a whole ReadTheDocs site with runnable Python code with solvers written from scratch. The slides aren’t out yet publicly or privately, but I would highly recommend going through the examples when the PyCon committee releases the information. The way he puts it makes it much less intimidating than I thought it would be. Also Raymond is a very nice guy :D
- camel_Snake 7y ago
  PyCon usually uploads talks within a day or two of their presentation. There should be a PyCon 2019 YouTube channel already.
  - manaskarekar 7y ago
    PyCon 2019 https://www.youtube.com/channel/UCxs2IIVXaEHHA4BtTiWZ2mQ https://www.youtube.com/channel/UCxs2IIVXaEHHA4BtTiWZ2mQ
gralx 7y ago
I've been learning TLA+ for the past two months, hoping I could use it as a formal language for software design generally and not just for concurrent systems. I'm enamored with the idea of using math formalisms to describe a state machine. But now that I've gone through Lamport's (very charming) video tutorials at OP's link and studied some of the specifications at https://github.com/tlaplus/Examples/tree/master/specifications https://github.com/tlaplus/Examples/tree/master/specificatio... I'm less sure now that I can. I'll keep plugging away, but if anyone here has any suggestions or offers any alternatives, I'm all ears.
- pron 7y ago
  I think TLA+ is a great fit for what you want to do. What problems are you facing? BTW, while state machines are certainly the recommended approach for TLA+ specifications (and for very good reasons), there are others, which may be useful in some cases. For example, here I have a rule-based specification of Tic-Tac-Toe: https://pron.github.io/files/TicTacToe.pdf https://pron.github.io/files/TicTacToe.pdf Instead of describing a state machine, the specification is a conjunction of state machines in a style known as "behavioral programming". Also, you may benefit from looking at the TLA+ subreddit (https://old.reddit.com/r/tlaplus/ https://old.reddit.com/r/tlaplus/) for various posts on TLA+ and formal methods in general, and maybe get some ideas.
  - gralx 7y ago
    > I think TLA+ is a great fit for what you want to do. I'm very happy to hear that. > What problems are you facing? Generally, the problem of formally specifying a program in set theory and first-order logic syntax before choosing implementation details, such as the language to program it in. I have to give more thought to how I would describing specific problems. I've started with a program I want to write that I've already modelled informally. I'll edit this post later to explain it.
    - pron 7y ago
      First, just to be precise, system dynamics are specified in TLA+ with TLA, which is a linear-time temporal logic (albeit one that seeks to minimize temporal reasoning); set theory is used "only" for the data part. Second, the whole point of a high-level specification is that it is not dependent on a programming language, and allows you to choose the level of detail that suits you. One of the things that set TLA+ apart is that it allows for very convenient refinements, i.e. you can specify the same system multiple times, at different levels of detail, and show that a more detailed specification indeed implements a more abstract one. Perhaps looking at examples (which you can find on the subreddit I linked and in the sidebar) will give you a better feel for how TLA+ is used for precisely the goal you have in mind. The Practical TLA+ book[1] (which uses PlusCal) also has good examples. [1]: https://www.apress.com/gp/book/9781484238288 https://www.apress.com/gp/book/9781484238288
hcnews 7y ago
This keeps getting re-shared periodically on HN. I wonder what's HN policy around re-sharing same/similar content.
- lolptdr 7y ago
  I searched and found several instances of a similar link, but HN doesn't stop me from posting it. I'm guessing there's some decay algorithm or it's not checking sub-domains or deep-links.
- Tomte 7y ago
  If it did not get "attention" (which I interpret as 10+ karma, but that's my interpretation), it may be resubmitted. If the last "attention" is older than a year, resubmitting is also okay. The first part is in the FAQ, the second part has been said by the mods multiple times.
bayareanative 7y ago
Interesting. I've worked concurrent systems in VHDL and Verilog (but not SystemVerilog) stacks, and those using C, C++, Haskell, OCaml, Ruby, Go, Erlang and Rust. I wonder if this approach could formally verify systems like seL4. Here's an approach to verifying concurrent systems using coq: https://www.sciencedirect.com/science/article/pii/S1571066108000765 https://www.sciencedirect.com/science/article/pii/S157106610...
- hwayne 7y ago
  You might be interested in TLAPS, the TLA+ proof system: https://tla.msr-inria.inria.fr/tlaps/content/Home.html https://tla.msr-inria.inria.fr/tlaps/content/Home.html There's also this essay on proving TLA+ specifications in Isabelle: https://davecturner.github.io/2018/02/12/tla-in-isabelle.html https://davecturner.github.io/2018/02/12/tla-in-isabelle.htm...
- pron 7y ago
  The main difference between Coq and TLA+ is that Coq is a research tool, intended and designed for use by researchers, while TLA+ is intended as an industry tool, and designed for use by engineers. They are essentially equivalent in their power when it comes to specifying and verifying software (although Coq is more suitable for proving general mathematics), but Coq is used almost exclusively by researchers. The learning curve is very different (one could get productive to the point they specify real nontrivial systems after learning TLA+ within a few days or a couple of weeks, while with Coq this takes many months), and TLA+ has much more automation.
billfruit 7y ago
One thing that bothered me while trying to learn the TLA+ is the two different but equivalent forms or syntax for writing it: a mathematical formula/expression form and code/program form. This topic is difficult as it, and having to deal with not one but two equivalent forms of saying one thing is perhaps a bit hard on a learner. I wish if there was a tutorial of TLA+ that ditched the whole mathematical formula notation, and taught only the code form.
- pron 7y ago
  They're equivalent in the sense that PlusCal, the pseudo-code-like language compiles to TLA+, the mathematical notation. The book Practical TLA+ teaches pretty much only PlusCal. Eventually, though, to get the full power, even those who start with PlusCal will need to learn at least some TLA+.

148 points by lolptdr 7y ago

Raymond Hettinger just have a talk at PyCon an hour ago about formal reasoning and solvers. There’s a lot of polish in the talk, with a whole ReadTheDocs site with runnable Python code with solvers written from scratch. The slides aren’t out yet publicly or privately, but I would highly recommend going through the examples when the PyCon committee releases the information. The way he puts it makes it much less intimidating than I thought it would be. Also Raymond is a very nice guy :D

camel_Snake 7y ago
PyCon usually uploads talks within a day or two of their presentation. There should be a PyCon 2019 YouTube channel already.
- manaskarekar 7y ago
  PyCon 2019 https://www.youtube.com/channel/UCxs2IIVXaEHHA4BtTiWZ2mQ https://www.youtube.com/channel/UCxs2IIVXaEHHA4BtTiWZ2mQ

gralx 7y ago

I've been learning TLA+ for the past two months, hoping I could use it as a formal language for software design generally and not just for concurrent systems. I'm enamored with the idea of using math formalisms to describe a state machine. But now that I've gone through Lamport's (very charming) video tutorials at OP's link and studied some of the specifications at https://github.com/tlaplus/Examples/tree/master/specifications https://github.com/tlaplus/Examples/tree/master/specificatio... I'm less sure now that I can. I'll keep plugging away, but if anyone here has any suggestions or offers any alternatives, I'm all ears.

pron 7y ago
I think TLA+ is a great fit for what you want to do. What problems are you facing? BTW, while state machines are certainly the recommended approach for TLA+ specifications (and for very good reasons), there are others, which may be useful in some cases. For example, here I have a rule-based specification of Tic-Tac-Toe: https://pron.github.io/files/TicTacToe.pdf https://pron.github.io/files/TicTacToe.pdf Instead of describing a state machine, the specification is a conjunction of state machines in a style known as "behavioral programming". Also, you may benefit from looking at the TLA+ subreddit (https://old.reddit.com/r/tlaplus/ https://old.reddit.com/r/tlaplus/) for various posts on TLA+ and formal methods in general, and maybe get some ideas.
- gralx 7y ago
  > I think TLA+ is a great fit for what you want to do. I'm very happy to hear that. > What problems are you facing? Generally, the problem of formally specifying a program in set theory and first-order logic syntax before choosing implementation details, such as the language to program it in. I have to give more thought to how I would describing specific problems. I've started with a program I want to write that I've already modelled informally. I'll edit this post later to explain it.
  - pron 7y ago
    First, just to be precise, system dynamics are specified in TLA+ with TLA, which is a linear-time temporal logic (albeit one that seeks to minimize temporal reasoning); set theory is used "only" for the data part. Second, the whole point of a high-level specification is that it is not dependent on a programming language, and allows you to choose the level of detail that suits you. One of the things that set TLA+ apart is that it allows for very convenient refinements, i.e. you can specify the same system multiple times, at different levels of detail, and show that a more detailed specification indeed implements a more abstract one. Perhaps looking at examples (which you can find on the subreddit I linked and in the sidebar) will give you a better feel for how TLA+ is used for precisely the goal you have in mind. The Practical TLA+ book[1] (which uses PlusCal) also has good examples. [1]: https://www.apress.com/gp/book/9781484238288 https://www.apress.com/gp/book/9781484238288

hcnews 7y ago

This keeps getting re-shared periodically on HN. I wonder what's HN policy around re-sharing same/similar content.

lolptdr 7y ago
I searched and found several instances of a similar link, but HN doesn't stop me from posting it. I'm guessing there's some decay algorithm or it's not checking sub-domains or deep-links.
Tomte 7y ago
If it did not get "attention" (which I interpret as 10+ karma, but that's my interpretation), it may be resubmitted. If the last "attention" is older than a year, resubmitting is also okay. The first part is in the FAQ, the second part has been said by the mods multiple times.

bayareanative 7y ago

Interesting. I've worked concurrent systems in VHDL and Verilog (but not SystemVerilog) stacks, and those using C, C++, Haskell, OCaml, Ruby, Go, Erlang and Rust. I wonder if this approach could formally verify systems like seL4. Here's an approach to verifying concurrent systems using coq: https://www.sciencedirect.com/science/article/pii/S1571066108000765 https://www.sciencedirect.com/science/article/pii/S157106610...

hwayne 7y ago
You might be interested in TLAPS, the TLA+ proof system: https://tla.msr-inria.inria.fr/tlaps/content/Home.html https://tla.msr-inria.inria.fr/tlaps/content/Home.html There's also this essay on proving TLA+ specifications in Isabelle: https://davecturner.github.io/2018/02/12/tla-in-isabelle.html https://davecturner.github.io/2018/02/12/tla-in-isabelle.htm...
pron 7y ago
The main difference between Coq and TLA+ is that Coq is a research tool, intended and designed for use by researchers, while TLA+ is intended as an industry tool, and designed for use by engineers. They are essentially equivalent in their power when it comes to specifying and verifying software (although Coq is more suitable for proving general mathematics), but Coq is used almost exclusively by researchers. The learning curve is very different (one could get productive to the point they specify real nontrivial systems after learning TLA+ within a few days or a couple of weeks, while with Coq this takes many months), and TLA+ has much more automation.

billfruit 7y ago

One thing that bothered me while trying to learn the TLA+ is the two different but equivalent forms or syntax for writing it: a mathematical formula/expression form and code/program form. This topic is difficult as it, and having to deal with not one but two equivalent forms of saying one thing is perhaps a bit hard on a learner. I wish if there was a tutorial of TLA+ that ditched the whole mathematical formula notation, and taught only the code form.

pron 7y ago
They're equivalent in the sense that PlusCal, the pseudo-code-like language compiles to TLA+, the mathematical notation. The book Practical TLA+ teaches pretty much only PlusCal. Eventually, though, to get the full power, even those who start with PlusCal will need to learn at least some TLA+.