9 ms·

TLA+

230 points by kristianpaul 6y ago

strangecasts 6y ago
Also worth noting that the VS Code extension for TLA+ is steadily improving: https://marketplace.visualstudio.com/items?itemName=alygin.vscode-tlaplus https://marketplace.visualstudio.com/items?itemName=alygin.v... https://open-vsx.org/extension/alygin/vscode-tlaplus https://open-vsx.org/extension/alygin/vscode-tlaplus
- hwayne 6y ago
  Heckin'! One of my favorite things to see in TLA+ adoption is people making more tools to work with it.
exdsq 6y ago
If you're interested in TLA+ I recommend https://learntla.com https://learntla.com which uses the simpler notation PlusCal
mratsim 6y ago
I have successfully used TLA+ to clear my 2-phase "put a thread to sleep" protocol from deadlock and livelocks. I also proved that one of the nasty deadlock bugs I was fighting on Linux (but not on Windows or Mac) was actually glibc missing condition variables wakeup signals from time to time. 100% convinced it's worth learning to debug or verify any kind of distributed or multithreaded synchronization primitive. I was bug hunting for a couple weeks before deciding to learn formal verification / model checking via TLA+. Writeup: https://github.com/mratsim/weave/issues/56 https://github.com/mratsim/weave/issues/56
- MaxBarraclough 6y ago
  Perhaps I'm missing something but shouldn't that bug be filed with the glibc project rather than with the weave project? Has glibc since fixed the issue?
  - mratsim 6y ago
    Weave is my multithreading library. It's just a recap of what I went through for future reference. I unfortunately didn't have time to go through: - compiling glibc from source - converting my code to C - trying to reduce multithreaded synchronization code to a minimal example given how non-deterministic any of those bugs are - do a write-up That said, it seems like people went through the motions 4 months after me in this bug: - https://sourceware.org/bugzilla/show_bug.cgi?id=25847 https://sourceware.org/bugzilla/show_bug.cgi?id=25847 which affects C#, OCaml, Python Someone also fully reimplemented Glibc condition variable in TLA+ to prove that the glibc code was buggy: - https://probablydance.com/2020/10/31/using-tla-in-the-real-world-to-understand-a-glibc-bug/ https://probablydance.com/2020/10/31/using-tla-in-the-real-w... (at the bottom)
    - vinay_ys 6y ago
      This is beautiful and satisfying.
    - pmarreck 6y ago
      Wow. I'd normally respond with (when looking at the very complex relevant glibc code), "complexity is a code smell", but I don't understand the problem space enough to legitimately suggest that here, other than to say that in my experience programming thus far, if you require this much complexity for any part of your system, it is in all likelihood reflective of a design flaw (possibly elsewhere).
      - MaxBarraclough 6y ago
        High-performance concurrency is just the kind of problem that may well require a complex solution.
      - grayhatter 6y ago
        Why do so many people use the word smell to disparage code? The human part of me always feels it's super douchy and elitist, and the engineer part hates it because it's inaccurate and misleading.
- bogomipz 6y ago
  >"100% convinced it's worth learning to debug or verify any kind of distributed or multithreaded synchronization primitive." Might you or anyone else have some resources you could recommend for learning TLA+?
  - cloogshicer 6y ago
    Check out the video course from Leslie Lamport (the creator of TLA+) himself: https://lamport.azurewebsites.net/tla/learning.html https://lamport.azurewebsites.net/tla/learning.html
    - macintux 6y ago
      Leslie is one of those ridiculously over-accomplished people in computer science. I think it's safe to say you've earned respect when people can legitimately recognize your name for multiple, mostly-unrelated achievements, without realizing everything else you've done.
- mratsim 6y ago
  I have compiled my research in formal verification tools and papers here, there are a couple dozens: - https://github.com/mratsim/weave/issues/18 https://github.com/mratsim/weave/issues/18
- thraway123412 6y ago
  I find it suspicious that glibc and musl should have the same bug. Double check your code?
  - mratsim 6y ago
    I checked my code dozens of times over days. I thought I had bugs in my code for sure, I couldn't believe glibc and musl had a bug. Then I decided to spend a couple days to learn formal verification, solved all the bugs it found. It worked on my Mac, it worked on Windows, it was still deadlocking on Linux. I replaced my code with raw futexes, no deadlock anymore. And I added logs that showed signaling happened but the thread signaled wasn't unblocked. The futex<->condvar swap is pretty simple. - https://github.com/mratsim/weave/blob/f41a562/weave/cross_thread_com/event_notifiers.nim#L144-L148 https://github.com/mratsim/weave/blob/f41a562/weave/cross_th...
    - thraway123412 6y ago
      Yes, I saw your screenshots, and I think they demonstrate lack of understanding of how condition variables work. Any use of condition variables where the lock is "never used" screams fundamentally broken to me. No amount of atomics and memory orderings or manually inserted fences/memory barriers can help you if you leave a race window open between checking your predicate and starting to wait on a signal. Condvar signals are not sticky. If nobody is waiting for a signal when you signal, that signal is lost. There is nothing between your atomics and lock & wait to prevent such loss. Also your TLA+ (or rather PlusCal) does not model a condition variable correctly, so it would obviously not detect this issue. You have a sticky boolean variable and await, which blocks the procedure until the condition becomes true. This detects lockups of the class where the condition is never signalled at all, but it does not model the possibility of losing a signal because nobody was waiting for it. I don't believe you discovered a bug in glibc and musl.
cptwunderlich 6y ago
Relevant: "Hillel Wayne is Designing Distributed Systems with TLA+" https://www.youtube.com/watch?v=qubS_wGgwO0 https://www.youtube.com/watch?v=qubS_wGgwO0
villasv 6y ago
TLA is the awesomest thing I've ever learned, yet the least frequent technique I use as an "enterprise product" software engineer. No regrets. I recommend watching the video series introducing TLA+ by Lamport, what a wonder.
- gwd 6y ago
  TLA has some amazing capabilities, no doubt about it. A few years ago I had to try to fix some security issues in the most complicated code I'd ever worked with [1]. Some of the "attacks" involved race conditions across three different processors: it was incredibly difficult to keep everything in my head. So I entered the key parts of the algorithm in to TLA+. It found all of the races that I'd found in the original algorithm; and then didn't find any issues in my fixed algorithm. That gave me at least some confidence that I'd gotten things mostly right. That said, it's really quite a wonky tool in a number of ways. The almost-C dialect which doesn't have local variables is quite a footgun. And it's quite tightly bound to their particular UI tool, which makes keeping the models in git possible but somewhat quirky. What I'd honestly like more is to be able to make some files which could be compiled either in the real software project, or as part of a formal verification testing step. That way you could verify the properties as part of your CI loop (or perhaps part of more extended testing done elsewhere, if that's too expensive), and also have more confidence that the implementation matched your model. [1] https://xenbits.xen.org/xsa/advisory-299.html https://xenbits.xen.org/xsa/advisory-299.html
  - agstewart 6y ago
    > And it's quite tightly bound to their particular UI tool, which makes keeping the models in git possible but somewhat quirky. I couldn't find a way of tracking the TLA+ Toolkit's files nicely in git, but with a bit of manual work it's possible, using the `tlc-bin` CLI[0]. I used the TLA+ Toolkit to write the spec[1], but wrote the models by hand (eg. [2]). This was before I heard of the VS-Code extension. I think it's quite good now, so there might be a better workflow that avoids the TLA+ toolkit altogether. > What I'd honestly like more is to be able to make some files which could be compiled either in the real software project, or as part of a formal verification testing step. Do you mean you'd like to generate a TLA+ spec from your source code? [0] https://github.com/pmer/tla-bin https://github.com/pmer/tla-bin [1] https://github.com/statechannels/tla-specs/blob/6d7227e2d18331c7a415b27cada2639557e99d48/ForceMove.tla https://github.com/statechannels/tla-specs/blob/6d7227e2d183... [2] https://github.com/statechannels/tla-specs/blob/6d7227e2d18331c7a415b27cada2639557e99d48/Version1.tla https://github.com/statechannels/tla-specs/blob/6d7227e2d183...
iudqnolq 6y ago
In CS212 we're mostly writing simple recursive programs in SML and proving using induction that they evaluate to the correct result. We step through the programs by hand on paper. This seems very different, and I'm wondering if what we're learning has any practical application.
- mistrial9 6y ago
  IMHO your CS212 work is didactic, not applied
- strangecasts 6y ago
  Not familiar with that course, but there are definitely applications for proof-writing to show that code does what you expect and/or satisfies certain properties - the seL4 microkernel [1] is probably the highest-profile example - but it quickly becomes impractical beyond small programs, or if the code wasn't written with proving in mind initially. IMO the most "practical" application for those methods is in strengthening type systems to allow more expressive constraints - one small example that comes to mind is Idris [2] allowing you to explicitly mark certain functions as total [3] and fail type-checking if they don't return a value for every possible input. The main thing to keep in mind with TLA+ is that it's not really meant for validating code, it's more for showing that your design is consistent and satisfies safety requirements (e.g. "no temporary node failure should result in data loss"). However, having a TLA+ specification usually makes the implementation fairly straightforward, especially in languages/environments with message-passing concurrency. You can use TLAPS [4] to write proofs-by-induction similar to yours for TLA+ specifications, but IMO the real power is in model-checking them with TLC, which gives you a lot of the advantages of formal methods with much less proof work. [1] https://github.com/seL4/l4v https://github.com/seL4/l4v [2] https://www.idris-lang.org/ https://www.idris-lang.org/ [3] https://idris.readthedocs.io/en/latest/tutorial/typesfuns.html#totality https://idris.readthedocs.io/en/latest/tutorial/typesfuns.ht... [4] https://tla.msr-inria.inria.fr/tlaps/content/Home.html https://tla.msr-inria.inria.fr/tlaps/content/Home.html
- remexre 6y ago
  That's a different style of proof, based on equational reasoning; Agda [0], Coq [1] and Lean [2] are three theorem provers that work with those proofs better. Being able to quickly and informally perform equational reasoning on functional programs is also what (imo) makes those languages easier to think about, so it's a valuable skill outside of proving. [0]: https://wiki.portal.chalmers.se/agda/pmwiki.php https://wiki.portal.chalmers.se/agda/pmwiki.php [1]: https://coq.inria.fr/ https://coq.inria.fr/ [2]: https://leanprover.github.io/ https://leanprover.github.io/
youerbt 6y ago
TLA+ is a nice tool to help with thinking. It is surprisingly approachable for a formal system, so don't hesitate to try it.
max_ 6y ago
TLA+ is what rekindled my genuine love for mathematices. I am a self taught dev and learning TLA+ gave me the feel of a "real" computer science. Learning how to think of of programs excusively as state machines gives a kind of intellectual clarity I didn't know existed. It is also the only thing that actually improved my dev productivity by magnitudes.
ChrisMarshallNY 6y ago
It looks quite useful; especially for cannot-fail systems, like operating systems, development tools, and Mars Rover firmware. It seems a bit overkill for the kinds of code I write, which represents a design flexibility that makes wet spaghetti look like a load-bearing truss.
zdw 6y ago
How does a program go from TLA+ spec to code that can be executed, and verify that they both do the same thing? Is this a manual (and therefore, subject to human error) process, or do tools exist for automating it?
- k__ 6y ago
  It's a manual process, but I read there are tools that try to automate it. But as far as I understood it, if you know TLA+ and the target language well, it's like writing an article from a good outline.
- jlouis 6y ago
  For TLA it's manual. For other systems, like Coq for instance, you can extract to another language. (Also important are that systems in this space are different. What something like Coq is good for is completely different to what TLA+ is good for. Another idea in the same vein is property-based-testing. Here the concrete code is tested by invoking random test examples, so you are testing the actual code/implementation. But this also means you can't use typical tricks of model checkers where they can regard whole classes of inputs the "same" in a test).
- dmos62 6y ago
  Think of writing a TLA+ spec as structured thinking with error checking. It helps create a correct algorithm. Having your code implement the algorirthm correctly is a different problem. There was a Racket language that actually syntesized programs from specs (e.g. go from spec of a sorting algo to its implementation automatically), but I forget what it's called. Fun to play around with.
  - Jtsummers 6y ago
    I've seen a couple things on using Racket for code synthesis. My google search revealed Rosette, which wasn't what I was thinking of. The other work may have been in Scheme, using minikanren, but my Google Fu seems weak this morning. https://docs.racket-lang.org/rosette-guide/index.html https://docs.racket-lang.org/rosette-guide/index.html
lukego 6y ago
I'd love to find a "bottom up" description of a language like TLA+. Start from the appropriate primitive (SAT solver? SMT solver?), show how to encode an example model directly, add layers of syntax etc as necessary for more complex examples. I've watched all of Lamport's lectures but it really leaves me wondering what's happening under the hood: what are the primitives and how are TLA+ models mapped onto them. (Lamport likes to say that TLA+ is just mathematics and imply that the engine underneath is not relevant but c'mon.)
- zozbot234 6y ago
  SAT and SMT solvers deal with propositional logic only. TLA+ is based on propositional logic with added modalities (i.e. what a type theorist would call monads) for "time" (in the temporal logic sense) and non-determinism. It is essentially a somewhat bespoke modal logic. Modal logics in general have lower expressive power than FOL, but are conversely more computationally tractable.
  - lukego 6y ago
    Just found the TLAPS Tactics page: https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Tactics.html https://tla.msr-inria.inria.fr/tlaps/content/Documentation/T... Sounds like the first thing TLAPS does is to translate the TLA+ program into SMT and try to prove it with Z3. If that times out then it translates it into a couple of other kinds of provers before giving up (...). Maybe I should look at how TLA+ "hello world" is compiled into SMT as a first step.
- igornotarobot 6y ago
  Depending on the problem that you are trying to solve with TLA+, you may prefer one encoding or another. For instance, here is one encoding for the proof system: https://hal.archives-ouvertes.fr/hal-01768750/ https://hal.archives-ouvertes.fr/hal-01768750/. And here is another encoding for model checking: https://dl.acm.org/doi/10.1145/3360549 https://dl.acm.org/doi/10.1145/3360549
  - romac 6y ago
virgil_disgr4ce 6y ago
How valuable is TLA+ for non-concurrent applications? I've always been interested in formal verification (is TLA+ technically that?).
- colonelcanoe 6y ago
  You can construct formal proofs about a TLA+ spec, using the "TLA proof system" (TLAPS). Or, you can verify properties for "bounded models" of your spec via brute force. The latter is much less overhead, so it's good to use bounded models (with the TLC model checker) to become confident in the spec, then construct proofs if warranted.
- Taikonerd 6y ago
  > How valuable is TLA+ for non-concurrent applications? My understanding is that TLA+ is for concurrent applications, but with a broad definition of "concurrent." For example, it could be... * multiple hosts messaging each other * multiple threads in one process sharing a data structure * multiple API calls that all use the same Postgres DB In other words, any sort of system where different actors can step on each others' toes.
  - Jtsummers 6y ago
    That's definitely the main use. But TLA+ can also be applied to single threaded specifications by encoding various invariants (pre/post conditions on entry and exit, loop invariants).
  - flazzarino 6y ago
    You define variables and code that changes the variables over time. TLA+ lets you observe variable states and assert constraints. The amount of concurrency is up to you, it works fine with a single process. Non-determinism might be a better thing to anchor the value to. For example in a deterministic "normal" programming environment, an if/then/else statement will execute only one out of two possible code paths. You have to run the code with a complementary condition to observe the other code path. In a non-deterministic environment like TLA+ both possible code paths are executed. You can observe state transitions in both possibilities. In a deterministic context the combinatorics of code paths can get out of hand quickly. Non-deterministically you have one set of assertions for all code paths, or patterns of paths.
SEJeff 6y ago
James Hamilton, the architect of AWS and one of the authors of DynamoDB wrote a blog post on formal verification of distributed systems. He specifically mentioned TLA+ as what his team at Amazon used to do this. 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...
ligurio 6y ago
Software companies widely uses TLA+ https://github.com/ligurio/practical-fm https://github.com/ligurio/practical-fm
CyanLite2 6y ago
Microsoft built Azure CosmosDB based on TLA+: https://github.com/Azure/azure-cosmos-tla https://github.com/Azure/azure-cosmos-tla
phtrivier 6y ago
There are two pieces of TLA+ and formal modeling that I don't get. (And I'm pretty sure all the authors and documenters have tried their best at explaining it again and again, but maybe asking the question again is not useless.) 1. Given you have to learn the language, and, at first, you don't know it - how do you even trust that you're writing a proof right, and that you're not simply writing gibberish ? TDD has code execution as an "arbiter of peace". If, when calling a function, you get an unexpected result, then... you did something wrong. If my TLA+ set of rules holds, how do I get confidence that I wrote the right set of rules ? 2. Once I've got a set of rule that I decided to trust, when I implement it and I get bugs (as demonstrated by executable code) ; how do I decide if the most plausible cause is a bug in my code, or a bug in the spec ? Maybe it becomes obvious once you've done it, and I'm sorry to be the million'th to say such nonsense. Sorry.
- deleted 6y ago
  [deleted]
- fpgaminer 6y ago
  TLA+ is fear driven development. If you have any fears that your TLA+ model or proofs might have been written wrong, your job is to encode those fears as further TLA+ proofs. The last TLA+ specification I wrote was only about two pages long. The actual model was a handful of lines. A handful of definitions. And then a page and a half of proofs and proof proofs. So it's easy to look over your spec exhaustively. And if there's any part of it you aren't sure about, or think you might have written wrong, then write more proofs that show that it you can't have written it wrong that way. The IDE provides lots of feedback and ways to debug. So like learning any language, you'll spend your formative time just trying out different parts of the TLA+ semantics and introspecting the outputs to make sure the models are behaving the way you expect them to. TLA+ is very much like doing math. If you do it wrong, you get answers that don't make sense. And it's easy to check if you're doing it wrong, by doing something you _know_ is wrong. If you get a "right" answer, you know you are making a mistake or don't understand a semantic correctly. The joy is that TLA+ allows you to write out these proof proofs and have them checked every time along with the rest of your spec. > how do I decide if the most plausible cause is a bug in my code, or a bug in the spec ? Your implementation and your TLA+ model share the same state data structures (though the TLA+ model might have a simplified representation of those states, eliding unimportant details). If you suspect your spec, you just copy the broken state sequence your implementation is encountering into your TLA+ model. If the model displays the same behavior you know your spec is wrong. If it doesn't, you know your implementation is wrong.

230 points by kristianpaul 6y ago

Also worth noting that the VS Code extension for TLA+ is steadily improving: https://marketplace.visualstudio.com/items?itemName=alygin.vscode-tlaplus https://marketplace.visualstudio.com/items?itemName=alygin.v... https://open-vsx.org/extension/alygin/vscode-tlaplus https://open-vsx.org/extension/alygin/vscode-tlaplus

hwayne 6y ago
Heckin'! One of my favorite things to see in TLA+ adoption is people making more tools to work with it.

exdsq 6y ago

If you're interested in TLA+ I recommend https://learntla.com https://learntla.com which uses the simpler notation PlusCal

mratsim 6y ago

I have successfully used TLA+ to clear my 2-phase "put a thread to sleep" protocol from deadlock and livelocks. I also proved that one of the nasty deadlock bugs I was fighting on Linux (but not on Windows or Mac) was actually glibc missing condition variables wakeup signals from time to time. 100% convinced it's worth learning to debug or verify any kind of distributed or multithreaded synchronization primitive. I was bug hunting for a couple weeks before deciding to learn formal verification / model checking via TLA+. Writeup: https://github.com/mratsim/weave/issues/56 https://github.com/mratsim/weave/issues/56

MaxBarraclough 6y ago
Perhaps I'm missing something but shouldn't that bug be filed with the glibc project rather than with the weave project? Has glibc since fixed the issue?
- mratsim 6y ago
  Weave is my multithreading library. It's just a recap of what I went through for future reference. I unfortunately didn't have time to go through: - compiling glibc from source - converting my code to C - trying to reduce multithreaded synchronization code to a minimal example given how non-deterministic any of those bugs are - do a write-up That said, it seems like people went through the motions 4 months after me in this bug: - https://sourceware.org/bugzilla/show_bug.cgi?id=25847 https://sourceware.org/bugzilla/show_bug.cgi?id=25847 which affects C#, OCaml, Python Someone also fully reimplemented Glibc condition variable in TLA+ to prove that the glibc code was buggy: - https://probablydance.com/2020/10/31/using-tla-in-the-real-world-to-understand-a-glibc-bug/ https://probablydance.com/2020/10/31/using-tla-in-the-real-w... (at the bottom)
  - vinay_ys 6y ago
    This is beautiful and satisfying.
  - pmarreck 6y ago
    Wow. I'd normally respond with (when looking at the very complex relevant glibc code), "complexity is a code smell", but I don't understand the problem space enough to legitimately suggest that here, other than to say that in my experience programming thus far, if you require this much complexity for any part of your system, it is in all likelihood reflective of a design flaw (possibly elsewhere).
    - MaxBarraclough 6y ago
      High-performance concurrency is just the kind of problem that may well require a complex solution.
    - grayhatter 6y ago
      Why do so many people use the word smell to disparage code? The human part of me always feels it's super douchy and elitist, and the engineer part hates it because it's inaccurate and misleading.
bogomipz 6y ago
>"100% convinced it's worth learning to debug or verify any kind of distributed or multithreaded synchronization primitive." Might you or anyone else have some resources you could recommend for learning TLA+?
- cloogshicer 6y ago
  Check out the video course from Leslie Lamport (the creator of TLA+) himself: https://lamport.azurewebsites.net/tla/learning.html https://lamport.azurewebsites.net/tla/learning.html
  - macintux 6y ago
    Leslie is one of those ridiculously over-accomplished people in computer science. I think it's safe to say you've earned respect when people can legitimately recognize your name for multiple, mostly-unrelated achievements, without realizing everything else you've done.
mratsim 6y ago
I have compiled my research in formal verification tools and papers here, there are a couple dozens: - https://github.com/mratsim/weave/issues/18 https://github.com/mratsim/weave/issues/18
thraway123412 6y ago
I find it suspicious that glibc and musl should have the same bug. Double check your code?
- mratsim 6y ago
  I checked my code dozens of times over days. I thought I had bugs in my code for sure, I couldn't believe glibc and musl had a bug. Then I decided to spend a couple days to learn formal verification, solved all the bugs it found. It worked on my Mac, it worked on Windows, it was still deadlocking on Linux. I replaced my code with raw futexes, no deadlock anymore. And I added logs that showed signaling happened but the thread signaled wasn't unblocked. The futex<->condvar swap is pretty simple. - https://github.com/mratsim/weave/blob/f41a562/weave/cross_thread_com/event_notifiers.nim#L144-L148 https://github.com/mratsim/weave/blob/f41a562/weave/cross_th...
  - thraway123412 6y ago
    Yes, I saw your screenshots, and I think they demonstrate lack of understanding of how condition variables work. Any use of condition variables where the lock is "never used" screams fundamentally broken to me. No amount of atomics and memory orderings or manually inserted fences/memory barriers can help you if you leave a race window open between checking your predicate and starting to wait on a signal. Condvar signals are not sticky. If nobody is waiting for a signal when you signal, that signal is lost. There is nothing between your atomics and lock & wait to prevent such loss. Also your TLA+ (or rather PlusCal) does not model a condition variable correctly, so it would obviously not detect this issue. You have a sticky boolean variable and await, which blocks the procedure until the condition becomes true. This detects lockups of the class where the condition is never signalled at all, but it does not model the possibility of losing a signal because nobody was waiting for it. I don't believe you discovered a bug in glibc and musl.

cptwunderlich 6y ago

Relevant: "Hillel Wayne is Designing Distributed Systems with TLA+" https://www.youtube.com/watch?v=qubS_wGgwO0 https://www.youtube.com/watch?v=qubS_wGgwO0

villasv 6y ago

TLA is the awesomest thing I've ever learned, yet the least frequent technique I use as an "enterprise product" software engineer. No regrets. I recommend watching the video series introducing TLA+ by Lamport, what a wonder.

gwd 6y ago
TLA has some amazing capabilities, no doubt about it. A few years ago I had to try to fix some security issues in the most complicated code I'd ever worked with [1]. Some of the "attacks" involved race conditions across three different processors: it was incredibly difficult to keep everything in my head. So I entered the key parts of the algorithm in to TLA+. It found all of the races that I'd found in the original algorithm; and then didn't find any issues in my fixed algorithm. That gave me at least some confidence that I'd gotten things mostly right. That said, it's really quite a wonky tool in a number of ways. The almost-C dialect which doesn't have local variables is quite a footgun. And it's quite tightly bound to their particular UI tool, which makes keeping the models in git possible but somewhat quirky. What I'd honestly like more is to be able to make some files which could be compiled either in the real software project, or as part of a formal verification testing step. That way you could verify the properties as part of your CI loop (or perhaps part of more extended testing done elsewhere, if that's too expensive), and also have more confidence that the implementation matched your model. [1] https://xenbits.xen.org/xsa/advisory-299.html https://xenbits.xen.org/xsa/advisory-299.html
- agstewart 6y ago
  > And it's quite tightly bound to their particular UI tool, which makes keeping the models in git possible but somewhat quirky. I couldn't find a way of tracking the TLA+ Toolkit's files nicely in git, but with a bit of manual work it's possible, using the `tlc-bin` CLI[0]. I used the TLA+ Toolkit to write the spec[1], but wrote the models by hand (eg. [2]). This was before I heard of the VS-Code extension. I think it's quite good now, so there might be a better workflow that avoids the TLA+ toolkit altogether. > What I'd honestly like more is to be able to make some files which could be compiled either in the real software project, or as part of a formal verification testing step. Do you mean you'd like to generate a TLA+ spec from your source code? [0] https://github.com/pmer/tla-bin https://github.com/pmer/tla-bin [1] https://github.com/statechannels/tla-specs/blob/6d7227e2d18331c7a415b27cada2639557e99d48/ForceMove.tla https://github.com/statechannels/tla-specs/blob/6d7227e2d183... [2] https://github.com/statechannels/tla-specs/blob/6d7227e2d18331c7a415b27cada2639557e99d48/Version1.tla https://github.com/statechannels/tla-specs/blob/6d7227e2d183...

iudqnolq 6y ago

In CS212 we're mostly writing simple recursive programs in SML and proving using induction that they evaluate to the correct result. We step through the programs by hand on paper. This seems very different, and I'm wondering if what we're learning has any practical application.

mistrial9 6y ago
IMHO your CS212 work is didactic, not applied
strangecasts 6y ago
Not familiar with that course, but there are definitely applications for proof-writing to show that code does what you expect and/or satisfies certain properties - the seL4 microkernel [1] is probably the highest-profile example - but it quickly becomes impractical beyond small programs, or if the code wasn't written with proving in mind initially. IMO the most "practical" application for those methods is in strengthening type systems to allow more expressive constraints - one small example that comes to mind is Idris [2] allowing you to explicitly mark certain functions as total [3] and fail type-checking if they don't return a value for every possible input. The main thing to keep in mind with TLA+ is that it's not really meant for validating code, it's more for showing that your design is consistent and satisfies safety requirements (e.g. "no temporary node failure should result in data loss"). However, having a TLA+ specification usually makes the implementation fairly straightforward, especially in languages/environments with message-passing concurrency. You can use TLAPS [4] to write proofs-by-induction similar to yours for TLA+ specifications, but IMO the real power is in model-checking them with TLC, which gives you a lot of the advantages of formal methods with much less proof work. [1] https://github.com/seL4/l4v https://github.com/seL4/l4v [2] https://www.idris-lang.org/ https://www.idris-lang.org/ [3] https://idris.readthedocs.io/en/latest/tutorial/typesfuns.html#totality https://idris.readthedocs.io/en/latest/tutorial/typesfuns.ht... [4] https://tla.msr-inria.inria.fr/tlaps/content/Home.html https://tla.msr-inria.inria.fr/tlaps/content/Home.html
remexre 6y ago
That's a different style of proof, based on equational reasoning; Agda [0], Coq [1] and Lean [2] are three theorem provers that work with those proofs better. Being able to quickly and informally perform equational reasoning on functional programs is also what (imo) makes those languages easier to think about, so it's a valuable skill outside of proving. [0]: https://wiki.portal.chalmers.se/agda/pmwiki.php https://wiki.portal.chalmers.se/agda/pmwiki.php [1]: https://coq.inria.fr/ https://coq.inria.fr/ [2]: https://leanprover.github.io/ https://leanprover.github.io/

youerbt 6y ago

TLA+ is a nice tool to help with thinking. It is surprisingly approachable for a formal system, so don't hesitate to try it.

max_ 6y ago

TLA+ is what rekindled my genuine love for mathematices. I am a self taught dev and learning TLA+ gave me the feel of a "real" computer science. Learning how to think of of programs excusively as state machines gives a kind of intellectual clarity I didn't know existed. It is also the only thing that actually improved my dev productivity by magnitudes.

ChrisMarshallNY 6y ago

It looks quite useful; especially for cannot-fail systems, like operating systems, development tools, and Mars Rover firmware. It seems a bit overkill for the kinds of code I write, which represents a design flexibility that makes wet spaghetti look like a load-bearing truss.

zdw 6y ago

How does a program go from TLA+ spec to code that can be executed, and verify that they both do the same thing? Is this a manual (and therefore, subject to human error) process, or do tools exist for automating it?

k__ 6y ago
It's a manual process, but I read there are tools that try to automate it. But as far as I understood it, if you know TLA+ and the target language well, it's like writing an article from a good outline.
jlouis 6y ago
For TLA it's manual. For other systems, like Coq for instance, you can extract to another language. (Also important are that systems in this space are different. What something like Coq is good for is completely different to what TLA+ is good for. Another idea in the same vein is property-based-testing. Here the concrete code is tested by invoking random test examples, so you are testing the actual code/implementation. But this also means you can't use typical tricks of model checkers where they can regard whole classes of inputs the "same" in a test).
dmos62 6y ago
Think of writing a TLA+ spec as structured thinking with error checking. It helps create a correct algorithm. Having your code implement the algorirthm correctly is a different problem. There was a Racket language that actually syntesized programs from specs (e.g. go from spec of a sorting algo to its implementation automatically), but I forget what it's called. Fun to play around with.
- Jtsummers 6y ago
  I've seen a couple things on using Racket for code synthesis. My google search revealed Rosette, which wasn't what I was thinking of. The other work may have been in Scheme, using minikanren, but my Google Fu seems weak this morning. https://docs.racket-lang.org/rosette-guide/index.html https://docs.racket-lang.org/rosette-guide/index.html

lukego 6y ago

I'd love to find a "bottom up" description of a language like TLA+. Start from the appropriate primitive (SAT solver? SMT solver?), show how to encode an example model directly, add layers of syntax etc as necessary for more complex examples. I've watched all of Lamport's lectures but it really leaves me wondering what's happening under the hood: what are the primitives and how are TLA+ models mapped onto them. (Lamport likes to say that TLA+ is just mathematics and imply that the engine underneath is not relevant but c'mon.)

zozbot234 6y ago
SAT and SMT solvers deal with propositional logic only. TLA+ is based on propositional logic with added modalities (i.e. what a type theorist would call monads) for "time" (in the temporal logic sense) and non-determinism. It is essentially a somewhat bespoke modal logic. Modal logics in general have lower expressive power than FOL, but are conversely more computationally tractable.
- lukego 6y ago
  Just found the TLAPS Tactics page: https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Tactics.html https://tla.msr-inria.inria.fr/tlaps/content/Documentation/T... Sounds like the first thing TLAPS does is to translate the TLA+ program into SMT and try to prove it with Z3. If that times out then it translates it into a couple of other kinds of provers before giving up (...). Maybe I should look at how TLA+ "hello world" is compiled into SMT as a first step.
igornotarobot 6y ago
Depending on the problem that you are trying to solve with TLA+, you may prefer one encoding or another. For instance, here is one encoding for the proof system: https://hal.archives-ouvertes.fr/hal-01768750/ https://hal.archives-ouvertes.fr/hal-01768750/. And here is another encoding for model checking: https://dl.acm.org/doi/10.1145/3360549 https://dl.acm.org/doi/10.1145/3360549
- romac 6y ago

virgil_disgr4ce 6y ago

How valuable is TLA+ for non-concurrent applications? I've always been interested in formal verification (is TLA+ technically that?).

colonelcanoe 6y ago
You can construct formal proofs about a TLA+ spec, using the "TLA proof system" (TLAPS). Or, you can verify properties for "bounded models" of your spec via brute force. The latter is much less overhead, so it's good to use bounded models (with the TLC model checker) to become confident in the spec, then construct proofs if warranted.
Taikonerd 6y ago
> How valuable is TLA+ for non-concurrent applications? My understanding is that TLA+ is for concurrent applications, but with a broad definition of "concurrent." For example, it could be... * multiple hosts messaging each other * multiple threads in one process sharing a data structure * multiple API calls that all use the same Postgres DB In other words, any sort of system where different actors can step on each others' toes.
- Jtsummers 6y ago
  That's definitely the main use. But TLA+ can also be applied to single threaded specifications by encoding various invariants (pre/post conditions on entry and exit, loop invariants).
- flazzarino 6y ago
  You define variables and code that changes the variables over time. TLA+ lets you observe variable states and assert constraints. The amount of concurrency is up to you, it works fine with a single process. Non-determinism might be a better thing to anchor the value to. For example in a deterministic "normal" programming environment, an if/then/else statement will execute only one out of two possible code paths. You have to run the code with a complementary condition to observe the other code path. In a non-deterministic environment like TLA+ both possible code paths are executed. You can observe state transitions in both possibilities. In a deterministic context the combinatorics of code paths can get out of hand quickly. Non-deterministically you have one set of assertions for all code paths, or patterns of paths.

SEJeff 6y ago

James Hamilton, the architect of AWS and one of the authors of DynamoDB wrote a blog post on formal verification of distributed systems. He specifically mentioned TLA+ as what his team at Amazon used to do this. 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...

ligurio 6y ago

Software companies widely uses TLA+ https://github.com/ligurio/practical-fm https://github.com/ligurio/practical-fm

CyanLite2 6y ago

Microsoft built Azure CosmosDB based on TLA+: https://github.com/Azure/azure-cosmos-tla https://github.com/Azure/azure-cosmos-tla

phtrivier 6y ago

There are two pieces of TLA+ and formal modeling that I don't get. (And I'm pretty sure all the authors and documenters have tried their best at explaining it again and again, but maybe asking the question again is not useless.) 1. Given you have to learn the language, and, at first, you don't know it - how do you even trust that you're writing a proof right, and that you're not simply writing gibberish ? TDD has code execution as an "arbiter of peace". If, when calling a function, you get an unexpected result, then... you did something wrong. If my TLA+ set of rules holds, how do I get confidence that I wrote the right set of rules ? 2. Once I've got a set of rule that I decided to trust, when I implement it and I get bugs (as demonstrated by executable code) ; how do I decide if the most plausible cause is a bug in my code, or a bug in the spec ? Maybe it becomes obvious once you've done it, and I'm sorry to be the million'th to say such nonsense. Sorry.

deleted 6y ago
[deleted]
fpgaminer 6y ago
TLA+ is fear driven development. If you have any fears that your TLA+ model or proofs might have been written wrong, your job is to encode those fears as further TLA+ proofs. The last TLA+ specification I wrote was only about two pages long. The actual model was a handful of lines. A handful of definitions. And then a page and a half of proofs and proof proofs. So it's easy to look over your spec exhaustively. And if there's any part of it you aren't sure about, or think you might have written wrong, then write more proofs that show that it you can't have written it wrong that way. The IDE provides lots of feedback and ways to debug. So like learning any language, you'll spend your formative time just trying out different parts of the TLA+ semantics and introspecting the outputs to make sure the models are behaving the way you expect them to. TLA+ is very much like doing math. If you do it wrong, you get answers that don't make sense. And it's easy to check if you're doing it wrong, by doing something you _know_ is wrong. If you get a "right" answer, you know you are making a mistake or don't understand a semantic correctly. The joy is that TLA+ allows you to write out these proof proofs and have them checked every time along with the rest of your spec. > how do I decide if the most plausible cause is a bug in my code, or a bug in the spec ? Your implementation and your TLA+ model share the same state data structures (though the TLA+ model might have a simplified representation of those states, eliding unimportant details). If you suspect your spec, you just copy the broken state sequence your implementation is encountering into your TLA+ model. If the model displays the same behavior you know your spec is wrong. If it doesn't, you know your implementation is wrong.