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

https://lamport.azurewebsites.net/tla/tla.html

by lolptdr • 7 years ago

148 32 7 years ago

lamport.azurewebsites.net

yingw787• 7 years 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• 7 years ago

PyCon usually uploads talks within a day or two of their presentation. There should be a PyCon 2019 YouTube channel already.

manaskarekar• 7 years ago

PyCon 2019 https://www.youtube.com/channel/UCxs2IIVXaEHHA4BtTiWZ2mQ

gralx6• 7 years 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/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.

pron8• 7 years 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 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/) for various posts on TLA+ and formal methods in general, and maybe get some ideas.

gralx6• 7 years 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.

sktrdie2• 7 years ago

I can't believe finally someone mentions behavioral programming here on HN. I'm a huge proponent of it and have written some in the context of React https://lmatteis.github.io/react-behavioral/

How does it compare with TLA+ though? I've tried reading through your document, but I can't seem to understand how the interweaving is done and the blocking.

hcnews• 7 years ago

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

lolptdr• 7 years 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• 7 years 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• 7 years 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/S157106610...

hwayne4• 7 years ago

You might be interested in TLAPS, the TLA+ proof system: 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.htm...

pron8• 7 years 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• 7 years 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.

pron8• 7 years 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+.

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

Related Stories