Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

TLA+ model checking made symbolic

blog.acolyer.org

Post reply on HN
Print view View original

31–40 of 54 posts

Re: TLA+ model checking made symbolic

#31

Post by QuinnWilton »

tempguy9999 wrote: post #7
QuinnWilton wrote: post #2

Is anybody using TLA+ in production outside of academia? What for? I've always wanted to, but I'm not familiar enough with it to always recognize when it'd be the right tool to reach for. I primarily code in Elixir and Erlang, and have used property testing to perform some level of model checking when working with state machines, and I suspect TLA+ could be helpful for formalizing that a little bit, but it isn't a th…

iterally DDG'ing "tla industry" gets you stuff eg. https://en.wikipedia.org/wiki/TLA%2B#Industry_use . Another 20 seconds gets you https://lamport.azurewebsites.net/tla/industrial-use.html

Sure, but not all of us are building products at the scale of Amazon and Microsoft. When you're shipping something like DynamoDB, the argument for TLA+ is obvious. What's harder to come across are the people finding ways to make use of technologies like this on a smaller scale, and I think that's one place where Hacker News really shines as a way of connecting people.

At least personally, working at a small and understaffed startup, I'm not always going to find the time to put together big case studies on interesting things I do, but it's a lot easier to share a sentence or two on a casual Hacker News thread. I wouldn't be surprised if it's the same for other people.

Re: TLA+ model checking made symbolic

#32

Post by QuinnWilton »

kachnuv_ocasek wrote: post #12
RBerenguel wrote: post #10

Earlier quoted context omitted.

I've written some models for "personal use and validation", and I keep it in my toolbelt (with Alloy) in case my thinking is not clear about something

Could you briefly describe some of the models you played with? It seems cool that someone just specified models and verifies them in their spare time.

You may have seen this blog already, but the author of "Practical TLA+" has a really fascinating blog with some fun toy examples. I'm a fan of this article where they model A Link to the Past with Alloy, to prove that dungeons are "winnable" [0].

The rest of the blog is really interesting too.

[0] https://www.hillelwayne.com/post/alloy-randomizer/

Re: TLA+ model checking made symbolic

#33

Post by QuinnWilton »

kachnuv_ocasek wrote: post #3
QuinnWilton wrote: post #2

Is anybody using TLA+ in production outside of academia? What for? I've always wanted to, but I'm not familiar enough with it to always recognize when it'd be the right tool to reach for. I primarily code in Elixir and Erlang, and have used property testing to perform some level of model checking when working with state machines, and I suspect TLA+ could be helpful for formalizing that a little bit, but it isn't a th…

Just a nitpick: Property testing is nowhere near the level of assurance that model checking provides.

Absolutely! Which is why I'd love to incorporate actual model checking into my work. I said that I make use of some level of model checking, but what I really meant was that I make use of a poor approximation of it.

Edit: I was convinced later in the thread that this isn't a fair comparison :)

Re: TLA+ model checking made symbolic

#34

Post by QuinnWilton »

pron wrote: post #28
QuinnWilton wrote: post #24

Earlier quoted context omitted.

I understand what you're saying, but I think that it's possible to approximate model checking with property testing, by defining your model's invariants as properties, and then generating a list of symbolic commands to run against your model. Like you said, you won't be testing all of the possible inputs, but it can still be a very effective way to detect the kinds of bugs that would otherwise be difficult to discove…

Randomized testing is very good, but it is so fundamentally different from model checking that it's not an approximation in any meaningful sense (except in the sense that both are automated methods that can find bugs). Again, even an explicit-state model checker can quickly check infinite executions. An interesting hybrid between the two is concolic testing (see https://youtu.be/MDzRV3OQtyQ which quickly shows the di…

Thank you for clarifying what you mean!

I was using the same terminlogy as the article, and treating my property tests as informal forms of model checking due to their being unsound, but I can see how that isn't exactly correct.

Re: TLA+ model checking made symbolic

#35

Post by tempguy9999 »

QuinnWilton wrote: post #31
tempguy9999 wrote: post #7

Earlier quoted context omitted.

iterally DDG'ing "tla industry" gets you stuff eg. https://en.wikipedia.org/wiki/TLA%2B#Industry_use . Another 20 seconds gets you https://lamport.azurewebsites.net/tla/industrial-use.html

Sure, but not all of us are building products at the scale of Amazon and Microsoft. When you're shipping something like DynamoDB, the argument for TLA+ is obvious. What's harder to come across are the people finding ways to make use of technologies like this on a smaller scale, and I think that's one place where Hacker News really shines as a way of connecting people. At least personally, working at a small and under…

That's not what was asked for. However I understand where you're coming from and am with you. I wish I had the chance to use TLA, or all the other goodies that seem ruled out by the results now and damn the bugs! mindset.

Re: TLA+ model checking made symbolic

#36

Post by QuinnWilton »

tempguy9999 wrote: post #35
QuinnWilton wrote: post #31

Earlier quoted context omitted.

Sure, but not all of us are building products at the scale of Amazon and Microsoft. When you're shipping something like DynamoDB, the argument for TLA+ is obvious. What's harder to come across are the people finding ways to make use of technologies like this on a smaller scale, and I think that's one place where Hacker News really shines as a way of connecting people. At least personally, working at a small and under…

That's not what was asked for. However I understand where you're coming from and am with you. I wish I had the chance to use TLA, or all the other goodies that seem ruled out by the results now and damn the bugs! mindset.

Fair :) My question was meant with more of a conversational slant than an objective one, but I can see how that tone gets lost over text. i.e. It's obvious that some people use TLA+, but I'm interested in what specifically the people here are using it for.

Re: TLA+ model checking made symbolic

#37

Post by trobertson »

southpolesteve wrote: post #21
QuinnWilton wrote: post #2

Is anybody using TLA+ in production outside of academia? What for? I've always wanted to, but I'm not familiar enough with it to always recognize when it'd be the right tool to reach for. I primarily code in Elixir and Erlang, and have used property testing to perform some level of model checking when working with state machines, and I suspect TLA+ could be helpful for formalizing that a little bit, but it isn't a th…

Azure Cosmos DB does. There is a good video about it: https://www.youtube.com/watch?v=kYX6UrY_ooA

And here is the Github of their models: https://github.com/Azure/azure-cosmos-tla

Re: TLA+ model checking made symbolic

#38

Post by hwayne »

QuinnWilton wrote: post #32
kachnuv_ocasek wrote: post #12

Earlier quoted context omitted.

Could you briefly describe some of the models you played with? It seems cool that someone just specified models and verifies them in their spare time.

You may have seen this blog already, but the author of "Practical TLA+" has a really fascinating blog with some fun toy examples. I'm a fan of this article where they model A Link to the Past with Alloy, to prove that dungeons are "winnable" [0]. The rest of the blog is really interesting too. [0] https://www.hillelwayne.com/post/alloy-randomizer/

Feel free to throw an email my way (it's on the website) if you want to chat a bit more about potential use cases.

Re: TLA+ model checking made symbolic

#39

Post by tonyarkles »

QuinnWilton wrote: post #29
tonyarkles wrote: post #20

Earlier quoted context omitted.

I've used it twice "in anger". About a year ago I modelled the LoRaWAN state machine to ensure that I'd caught all of the corner cases (packets that get missed/corrupted). I iterated on my FSM until it no longer had deadlocks, and then basically transcribed it to C and it all worked. I was impressed. Right now, I'm doing a similar thing. I've got a Bluetooth LE device that has a bit of a request/response layer built…

> The TLA+ model basically pointed out that the (finite sized) message buffer can grow without bounds if notifications are missed over and over (e.g. a super shitty RF environment). I've got a strategy that might work for polling it periodically, but I don't know that I would have realized this failure path without modelling it. Obviously I don't know anything about your use case, and I apologize if this comes across…

Oh, the device itself keeps a finite-sized mailbox and deletes the oldest message if it's full.

The concern is that one of the deleted messages might have been important (e.g. informing us that a transmission failed, or informing us that Search & Rescue got the message and is sending a helicopter). The polling is a backup plan that at least gives the phone feedback if it's not working (a failed read informs the phone that the read failed; a failed notification doesn't tell either side that something failed). We can still obviously lose messages if enough of them come in between polling intervals, but it's better than potentially losing messages indefinitely without knowing about it.

The other nice thing is that we can keep metrics for how often the polling process actually finds things that we weren't successfully notified about. That'll either give us leverage to encourage the vendor to switch to indications instead of notifications, or encourage us to find a new vendor :)

Edit: and yes, I 100% appreciate the feedback!

Re: TLA+ model checking made symbolic

#40

Post by QuinnWilton »

tonyarkles wrote: post #39
QuinnWilton wrote: post #29

Earlier quoted context omitted.

> The TLA+ model basically pointed out that the (finite sized) message buffer can grow without bounds if notifications are missed over and over (e.g. a super shitty RF environment). I've got a strategy that might work for polling it periodically, but I don't know that I would have realized this failure path without modelling it. Obviously I don't know anything about your use case, and I apologize if this comes across…

Oh, the device itself keeps a finite-sized mailbox and deletes the oldest message if it's full. The concern is that one of the deleted messages might have been important (e.g. informing us that a transmission failed, or informing us that Search & Rescue got the message and is sending a helicopter). The polling is a backup plan that at least gives the phone feedback if it's not working (a failed read informs the phone…

That makes a lot of sense! Thanks for elaborating :)

If you don't mind me asking, what are you working on / what is your background? It sounds like you're doing a ton of really interesting engineering, involving a lot of moving parts.

Post reply on HN