7 ms·

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 t

• kachnuv_ocasek 7y ago
  Just a nitpick: Property testing is nowhere near the level of assurance that model checking provides.
  • QuinnWilton 7y ago
    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 :)
• papermachete 7y ago
  Amazon uses it, even made publications for it.
  • Upvoter33 7y ago
    https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon.... for those who are interested
• unrequited 7y ago
  I've come across this repo which use TLA+ to validate data migrations. https://github.com/Shopify/ghostferry https://github.com/Shopify/ghostferry
  • QuinnWilton 7y ago
    This is really cool! I'm continually blown away by the quality of some of the projects Shopify open sources.
• tempguy9999 7y ago
  iterally DDG'ing "tla industry" gets you stuff eg. https://en.wikipedia.org/wiki/TLA%2B#Industry_use https://en.wikipedia.org/wiki/TLA%2B#Industry_use. Another 20 seconds gets you https://lamport.azurewebsites.net/tla/industrial-use.html https://lamport.azurewebsites.net/tla/industrial-use.html
  • QuinnWilton 7y ago
    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.
    • tempguy9999 7y ago
      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.
      • QuinnWilton 7y ago
        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.
• snak 7y ago
  I've seen it used in RabbitMq, but I also wonder if this is used in the real world or just in academia/few technologies.
• Karrot_Kream 7y ago
  I reach for TLA+ any time I want to temporally model any complicated system and make sure of certain invariants, so usually any distributed system I build. The last really complicated system I used it on was to rewrite a broken message store we had implemented on top of memcached.
• RBerenguel 7y ago
  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
  • kachnuv_ocasek 7y ago
    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.
    • QuinnWilton 7y ago
      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/ https://www.hillelwayne.com/post/alloy-randomizer/
      • hwayne 7y ago
        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.
    • RBerenguel 7y ago
      My spare time is kind of... weird. They were related to concurrency in an actor system, I validated a design and implementation (can’t share much more). I recommend checking Hillel’s blog as suggested, he has excellent examples (and his book is a good starting point for TLA+ and Pluscal as well)
• baq 7y ago
  at the very least it's worth it to watch the video courses by Lamport himself.
• kelvich 7y ago
  Yes, working on distributed database. So far it's quite useful -- it is possible to quickly check correctness of changes that you intend to make in few crucial places in code. It took about a week of learning/experimenting to write a useful spec. Also resulting state machine is not that much different from what you can expect in networking code working with epoll().
• pron 7y ago
  I have used it when working on some subtle/complicated system. BTW, property-based testing and model-checking are not really similar. Model-checking is any automated technique to find an invalidating assignment to some formula or declare there is none (so SAT solvers do model-checking). In the case of programs, model checkers automatically determine whether a program satisfies some property. Unlike property-based tests, they do not run the program on all inputs. In fact, the program is never run at all in the ordinary sense. Even TLC, an explicit state model checker for TLA+, that tries every possible state can check uncountably many executions, each of infinite length in a matter of seconds, where "running" even one of those would take infinite time. It is sometimes easy to think of a model checker as conceptually running the program on every input, but it's also sometimes important to know that model checkers don't actually do that.
  • QuinnWilton 7y ago
    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 discover with more traditional testing methods. Here's an example of what I'm talking about: http://propertesting.com/book_stateful_properties.html http://propertesting.com/book_stateful_properties.html
    • pron 7y ago
      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 https://youtu.be/MDzRV3OQtyQ which quickly shows the difference in power between concolic testing and randomized testing). Concolic testing is one of the most promising areas in formal verification these days. Also, the use of the term "non-formal" in the article you linked is incorrect. If it runs on the computer it is, by definition, formal. The author meant "sound" or "exhaustive" (although, while all model checkers are exhaustive, many -- like the one in this article -- don't actually try each input; they're exhaustiveness implies soundness, not a particular brute-force algorithm. How well they can actually beat brute force is, however, another matter...). BTW, it is possible to use the TLC model checker for randomized tests of TLA+ specifications in a way similar to randomized testing of "stateful properties", as checking random walks of the state graph.
• roskilli 7y ago
  Some of us (read... one of us, and not me, yet) uses TLA+ when theorizing changes to parts of M3DB, which is a distributed time series database. You can see the specs here, the current TLA+ models the consistency model of data being persisted to disk (flush, snapshot), there was at some point TLA+ for describing the quorum writes/reads along with the background tick event loop but that must be elsewhere now. https://github.com/m3db/m3/tree/master/specs https://github.com/m3db/m3/tree/master/specs
• cmarinas 7y ago
  I used it in the context of Linux kernel development to model/verify various algorithms. I gave a presentation last year at Linux Plumbers: http://procode.org/FormalMethodsPlumbers2018.pdf http://procode.org/FormalMethodsPlumbers2018.pdf Slides 4 and 28 list actual bugs found by such modelling. I do find TLA+ (or formal modelling in general) pretty useful for real world cases, only that, unfortunately, I don't always have the time.
  • QuinnWilton 7y ago
    This presentation is exactly the sort of thing I'm interested in, thank you!
• tonyarkles 7y ago
  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 on top of the standard characteristic read/write stuff (it's a BLE Iridium modem, if you're curious). I didn't make the device, I'm just writing mobile apps that interact with it. There's a lot going on here: - apps transition through different states (foreground, background, suspended). There's different things we can do when the app is in different states (e.g. there isn't really a good way to initiate a BLE characteristic read on the iOS side when the app is suspended) - the Bluetooth hardware transitions through multiple states (off, on, not authorized) - the BLE connection transitions through multiple states (disconnected, initial connection, services & characteristics discovered, etc) - the stateful protocol involves writing to a characteristic and receiving either 1 or 2 messages back, later on. Transmitting to the Iridium constellation can take a minute if the modem has to reconnect to the satellites. This transmission may fail (which we will be told about), but a failed transmission remains queued on the device and may succeed later. - The BLE-Iridium devices notifies the mobile device when something happens via BLE Notifications. Notifications are unreliable, so there's a chance we could miss receiving a notification the device has sent us. This has already shaken out one potential show stopper: if the app is suspended, it can be woken up by a BLE notification to let us know there's new data available; however, if we miss that notification (it's not a reliable notification), there's no good way to poll the device to see if there's data available when the app is suspended. (Using only the available BLE APIs) 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. I may also end up pushing back to the vendor to see if they can implement BLE Indications (reliable) as well as BLE Notifications (unreliable). If a BLE Indication fails, the BLE device should disconnect, which will trigger CoreBluetooth stuff that allows us to reconnect and poll without having to do some hacky timer-related stuff. Can't rely on sending a silent push notification either, since the device will be used in remote areas where there's likely no data coverage.
• southpolesteve 7y ago
  Azure Cosmos DB does. There is a good video about it: https://www.youtube.com/watch?v=kYX6UrY_ooA https://www.youtube.com/watch?v=kYX6UrY_ooA
  • trobertson 7y ago
    And here is the Github of their models: https://github.com/Azure/azure-cosmos-tla https://github.com/Azure/azure-cosmos-tla
• im_down_w_otp 7y ago
  We use TLA+. There's nothing particularly magical about TLA+. There are a variety of modeling languages and model checking toolkits out there. I've yet to encounter someone in industries that have commonly adopted model definition & checking who uses TLA+. It's popularity seems highest among folks in newer SaaS/IT arenas than elsewhere. More often I run into folks using SCADE's model checker. Tied for a distant 2nd, I'd say I've run into more folks who work with NuSMV, CADP, and mCRL2 than TLA+. This could also be mostly sample bias, and it's worth noting that the folks who use any of these things are in the very extreme minority of architects & developers that I speak to in automotive, med. tech., industrial automation, etc. Though, like I said, we use TLA+. Not for any particularly good reason than it was a sufficient tool among the variety of comparable tools for what we needed to do, but I expect that if we had to go back and do it all over again we'd have selected something else. The specification language has some annoying warts, the checking performance isn't comparatively very good, and the provided IDE works in almost exactly the opposite way any of us wish it would work. To the point that one of our engineers figured out how to wire it all up through Emacs so we could stop monkeying around with TLA Toolbox for 90% of the work. Of course, everything has problems, so TLA+ isn't notoriously different here. We've just used it in anger more than other things. For whatever it's worth, I also used to be an Erlang developer and used to play around a bit with McErlang, which I think might be a dead project now. However, there's an active project called Concuerror (https://concuerror.com/ https://concuerror.com/) which kind of covers the same domain. I don't know how well it works or what its level of maturity is, but it is very interesting in this one very important regard... it's model checking against your actual program implementation. That's an enormous and fantastic difference. Model conformance of concrete implementation to your design (and checked) model is an enormous problem, and tools which can close or remove that gap can be enormously valuable. What I don't know is the level of sophistication of Concuerror, nor if it is able to check for the kinds of properties you care about in your systems.
  • QuinnWilton 7y ago
    Concuerror is a very cool tool! I've been very impressed with some of the bugs I've seen it detect. It's definitely a tool I'd like to make more use of. Thanks for the insightful comment, it's given me a lot of things to research!
• Ixiaus 7y ago
  I use it in production at my job, I primarily use it to catch sneaky bugs in designs before implementing them and to produce something tangible to talk over with other engineers once I've settled on a design. It's worth learning and using IMHO.
• dmytroi 7y ago
  I'm starting to use TLA+ to verify lock-free algorithms. The tool is essential when all your code fits on the screen, yet you can't comprehend what is going on and miss a race here and there. So far it's more a personal interest, but I'm advocating for spending more time verifying critical pieces of our code base like MPMC containers, synchronization primitives, etc. PS. Doing C/C++/C# in gamedev.