4 ms·

The case studies are all race conditions in distributed systems. Is TLA+ useful for complex serial systems like compilers, etc.?

drdrey 7y ago
TLA+ is really good at finding problematic traces involving concurrent agents, so it naturally shines in distributed systems. For something that relies on finding problematic inputs (like for compilers), SMT solvers like Z3 are a more natural fit
hwayne 7y ago
It's possible to use TLA+ for complex serial systems, and it can def help there. The thing is that TLA+ is designed to be good at modeling concurrent problems, problems that have a lot of specific challenges you don't see in serial systems. So if you know your system is serial and nondeterministic, then you're probably better off with something that focuses on that part of the design space. To paraphrase Edmund Clarke's Turing lecture[1], the problems of verifying software include "floats, strings, user-defined types, procedures, concurrency, generics, storage, libraries…" If you're not worried about verifying concurrency in your tool, you've got a more resources to devote towards verifying the other things. That's also a space I don't have as much familiarity with, so I don't know what the best tools are there. My vague understand is that at that stage the problem "simplifies" enough that it's a lot easier to verify the code itself. Like how CompCert isn't just a model of a compiler, it's an actual correct compiler. So you can apparently work much closer to the code when verifying serial things. At one point I got a bunch of people in FM to write provably correct versions of Leftpad.[2] Maybe one of those would work best for you? Note also that one of the examples uses proves Java code correct via inline JML annotations. [1]: https://amturing.acm.org/vp/clarke_1167964.cfm https://amturing.acm.org/vp/clarke_1167964.cfm [2]: https://github.com/hwayne/lets-prove-leftpad https://github.com/hwayne/lets-prove-leftpad
- zozbot234 7y ago
  Do you really mean "nondeterministic"? AIUI, what people call 'TLA' was designed by adding a bunch of modalities (you can think of these as "monads" if you like[0]) for nondeterminism and "time" (state transitions) to standard propositional logic. The rest of it is really a matter of what's idiomatic, such as using the nondeterminism modality to account for spec refinement as well. So it would seem that TLA+ should be enough to deal with these cases. [0] Or burritos. Mmm, burritos. /s
  - pron 7y ago
    I think he meant to write deterministic. The exact nature of the logic TLA is not the relevant point here. TLA (and so TLA+) extensively relies on nondeterminism for things like specifying code at arbitrary levels of detail (e.g. you can say, after this step, the list is sorted somehow, without specifying how), interaction with the environment (the user performs one operation of the possible ones, or some arbitrary machine fails) or concurrency in its programming sense (the OS will schedule one of these several operations next).
    - zozbot234 7y ago
      I agree, mostly, but understanding "the exact nature" of a logic (or at least a properly-defined subset of it) is pretty important for using it effectively.
      - pron 7y ago
        If you're interested, I've written a rather detailed explanation of the TLA+ logic. Part 1 is an introduction that explains the design from a UX perspective, part 2 is about the + side of the logic, and parts 3 and 4 are about TLA: https://pron.github.io/tlaplus https://pron.github.io/tlaplus

drdrey 7y ago

TLA+ is really good at finding problematic traces involving concurrent agents, so it naturally shines in distributed systems. For something that relies on finding problematic inputs (like for compilers), SMT solvers like Z3 are a more natural fit

hwayne 7y ago

It's possible to use TLA+ for complex serial systems, and it can def help there. The thing is that TLA+ is designed to be good at modeling concurrent problems, problems that have a lot of specific challenges you don't see in serial systems. So if you know your system is serial and nondeterministic, then you're probably better off with something that focuses on that part of the design space. To paraphrase Edmund Clarke's Turing lecture[1], the problems of verifying software include "floats, strings, user-defined types, procedures, concurrency, generics, storage, libraries…" If you're not worried about verifying concurrency in your tool, you've got a more resources to devote towards verifying the other things. That's also a space I don't have as much familiarity with, so I don't know what the best tools are there. My vague understand is that at that stage the problem "simplifies" enough that it's a lot easier to verify the code itself. Like how CompCert isn't just a model of a compiler, it's an actual correct compiler. So you can apparently work much closer to the code when verifying serial things. At one point I got a bunch of people in FM to write provably correct versions of Leftpad.[2] Maybe one of those would work best for you? Note also that one of the examples uses proves Java code correct via inline JML annotations. [1]: https://amturing.acm.org/vp/clarke_1167964.cfm https://amturing.acm.org/vp/clarke_1167964.cfm [2]: https://github.com/hwayne/lets-prove-leftpad https://github.com/hwayne/lets-prove-leftpad

zozbot234 7y ago
Do you really mean "nondeterministic"? AIUI, what people call 'TLA' was designed by adding a bunch of modalities (you can think of these as "monads" if you like[0]) for nondeterminism and "time" (state transitions) to standard propositional logic. The rest of it is really a matter of what's idiomatic, such as using the nondeterminism modality to account for spec refinement as well. So it would seem that TLA+ should be enough to deal with these cases. [0] Or burritos. Mmm, burritos. /s
- pron 7y ago
  I think he meant to write deterministic. The exact nature of the logic TLA is not the relevant point here. TLA (and so TLA+) extensively relies on nondeterminism for things like specifying code at arbitrary levels of detail (e.g. you can say, after this step, the list is sorted somehow, without specifying how), interaction with the environment (the user performs one operation of the possible ones, or some arbitrary machine fails) or concurrency in its programming sense (the OS will schedule one of these several operations next).
  - zozbot234 7y ago
    I agree, mostly, but understanding "the exact nature" of a logic (or at least a properly-defined subset of it) is pretty important for using it effectively.
    - pron 7y ago
      If you're interested, I've written a rather detailed explanation of the TLA+ logic. Part 1 is an introduction that explains the design from a UX perspective, part 2 is about the + side of the logic, and parts 3 and 4 are about TLA: https://pron.github.io/tlaplus https://pron.github.io/tlaplus