9 ms·

A clarification: > Instead of writing proofs, it works using the simple method of running all possible executions of a program. TLA+ is a formal mathematical

by pron 6y ago

A clarification: > Instead of writing proofs, it works using the simple method of running all possible executions of a program. TLA+ is a formal mathematical language designed to describe digital (and hybrid digital-analog) systems. By itself it "does" nothing other than allow writing a formal description of a system, various propositions about it, and their proofs. There are tools, however, for mechanically writing and checking TLA+ proofs with a proof assistant (TLAPS), as well as model-checking them (TLC). The author refers to the latter, but it should be noted that model checkers, including an explicit-state model checker like TLC, don't only not run all possible executions of a program, they don't even run it once. They are "static." Indeed, TLC could, in some situations, check whether an uncountably infinite number of program executions, each of which of infinite length, satisfy some proposition within seconds. Also, the author chose to specify their algorithm in PlusCal, rather than in TLA+, which is pseudocode-like a language that compiles to TLA+ in a straightforward manner and is sometimes more convenient than TLA+ to specify low-level concurrent algorithms (TLA+ is more convenient to specify a higher level view of an entire system). TLA+ is, however, exceptionally pragmatic due to an availability of a model checker for it (in fact, there are now two model checkers for TLA+, TLC and Apalache, using very different algorithm), but mostly because it is exceptionally easy to learn compared to other formal mathematical languages.

elteto 6y ago
This is something I never quite understood with TLA+ (just from reading articles here and there, never actually used it). Let’s say I have a piece of C++ code and a TLA+ model for what it should be doing. How do I validate the C++ code with it?
- vector_spaces 6y ago
  My (probably wrong) understanding is that you don't -- you spec out the system design in TLA+, and use that to check if your design is sound (free of race conditions or certain other kinds of logic bugs). Checking that the TLA+ spec is implemented properly by the (say) C++ code is out of scope
- pron 6y ago
  You're asking the wrong question. Unless your program is very small or the property you wish to check is very simple, nothing can fully "validate" it. The question should be, is TLA+ more beneficial than just testing in improving program correctness? Humanity currently lacks the means to verify "deep" properties of code at any reasonable scale. Any tool that works at the code level either focuses on very simple properties (memory safety), complex but local properties of a small code-unit (Ada SPARK, Java's OpenJML), or deep properties of tiny programs (like seL4 and CompCert). These can be very important, but none truly offer the ability to "verify code" with some repeatable process at a generally-interesting scale. TLA+ could be used to do the same -- e.g. there is a C to TLA+ compiler -- but then it suffers from the same scale/depth/cost limitation of all code-level tools. So given that we can't just choose to verify a program, the question we want to answer is a different one: what is a good way, in a cost/benefit sense to achieve the correctness we want. Then you can ask whether TLA+ can offer such a way that is "better" in that sense than what you do now, which is likely testing. Those who have tried it, including myself, have come to the conclusion that in cases where the algorithm/design is sufficiently interesting or subtle, the answer is absolutely yes. The way TLA+ achieves it better than code level tools is that it allows you to describe your system at the level appropriate for answering your most important questions about it, and that level can be a much higher one than the code. So, to answer your question, the mere act of precisely expressing your system and correctness criteria in some chosen level of detail using very simple mathematics (high-school or first-year-college level), and then model-checking some interesting instances, is a good way (in the cost/benefit sense) to find bugs and make your program more correct. You compare it to the code by inspection. No, it does not give you 100% guarantees, but nothing else can, either. It is still worthwhile to do in addition to testing, as overall it can easier and cheaper in many cases to detect certain rare-yet-catstrophic bugs. Having said that, there are various techniques being explored that can check whether your program matches the TLA+ specification more mechanically than just by inspection, that might not be sound (i.e. give a 100% guarantee) but increase confidence while being cheap.
  - zozbot234 6y ago
    > Humanity currently lacks the means to verify "deep" properties of code at any reasonable scale. Any tool that works at the code level either focuses on very simple properties (memory safety), complex but local properties of a small code-unit (Ada SPARK, Java's OpenJML), or deep properties of tiny programs (like seL4 and CompCert). This may be true in a sense, but then a TLA+ specification is also a "tiny program" of sorts. There's no reason why one couldn't use a "code-level" (end-to-end) interactive proof tool to verify TLA+-like specs. Even model checking can be subsumed elegantly within such a tool; a model checking run is simply a search for a refutation (as opposed to a positive proof) of some claimed properties wrt. the proposed spec.
- User23 6y ago
  A better question to ask is how do I formally derive a program that satisfies a given specification? Then validation is just mathematical “checking your work” and is easy or even trivial.
  - pron 6y ago
    Except that's another question to which the answer is currently, "you don't", at least not at any interesting scale, not with TLA+ and not with anything else. But TLA+ is a tool aimed to help achieve correctness effectively, i.e. get a good cost/benefit for it. Between the highly scalable, low-confidence, testing, and the high-confidence, low-scale end-to-end verification, there's a huge swath of software correctness techniques, and the flexible TLA+ tries to hit a rather large swathe of that spectrum. In other words, we ask, is this better than what we do now in a sufficiently large portion of cases, rather than is this the silver bullet? The answer to the second question is no. I think the answer to the first one is yes.
    - User23 6y ago
      Formal program derivation satisfying a given specification has been around for well over half a century now. Hoare logic and the predicate calculus are entirely adequate for formal derivation in any language with well-documented semantics. Lamport himself has contributed significantly to the field. Unfortunately the American dominated programming industry has a strange phobia about mathematical reasoning[1]. The irrationality is exposed by patently ridiculous statements like that formal derivation doesn't scale. If you believe that, then you can't believe any nontrivial results from the hard physical sciences or pure mathematics. The actuality is that formal derivation makes building nontrivial constructs considerably easier. It is a tool, and like any tool when used properly it acts as a capability multiplier. [1] This is doubly confusing to me because it's not a matter of difficulty. Anyone with the mental horsepower to learn a modern programming language is easily capable of gaining proficiency in the predicate calculus.
      - zozbot234 6y ago
        > Hoare logic and the predicate calculus are entirely adequate for formal derivation in any language with well-documented semantics. Formal verification, yes. Formal derivation of a correct program from a spec, I really don't think so. In particular, I don't know of an easy way of deriving the required induction hypotheses/loop invariants to prove correctness of a program which includes recursion or loops.
- k__ 6y ago
  You don't validate the C++ code, you validate the algorithm before you implement it with C++. You have an idea for an algorithm, write it down with TLA+. TLA+ tells you if you screwed something up. You refine the algorithm until TLA+ says it's okay now. You implement the refined algorithm with the programming language of your choice. Everything that happens from that point is outside of TLA+'s power.
- jen20 6y ago
  For a fantastic intro to the basics and purpose of TLA+, I'd strongly recommend Scott Wlaschin's [1] talk from NDC Oslo this year. Like other academic-seeming subjects, Scott does a great job of applying it to real-world programming. That said, the answer to your exact question is that it doesn't validate the C++, it validates the algorithm. It's your job to ensure the C++ implements the algorithm as validated! [1]: https://www.youtube.com/watch?v=tqwcz-Yt9gQ https://www.youtube.com/watch?v=tqwcz-Yt9gQ
  - pron 6y ago
    I wish people use "real" (pretty-printed) TLA+ syntax -- the syntax used when reading a spec -- when giving presentations rather than SANY's LaTeX-like ASCII syntax used to type them. The read/write ratio for maths, including TLA^+ specifications, is higher than for programs, and so there are two concrete syntaxes optimised for those two different modes. I think most people know that on the computer, maths is usually typed differently from how it's read, and they expect to read the maths, not the LaTeX source used to typeset it. It isn't any different for TLA^(+).
- Twirrim 6y ago
  An anecdotal example of the use of TLA+ The service I worked for in AWS had to built a key service, about 18 months-ish after launch. If the service got anything wrong, it would wipe out the customer's data. Evaluating the conditions and making the right decisions wasn't that complicated, but it was complicated enough as it involved multiple service components to meet certain scaling properties. The need to not do the wrong thing was crucial, and so the decision was made to use TLA+ to make sure things were correct. Two senior engineers had designed the overall process and it had been through architectural review (so almost all the senior engineers in the team had seen and reviewed it, and in this case I know at least one well respected principal engineer had been involved. Potential problems had been identified and resolved). Everyone felt confident, but we wanted to be sure. The engineers spent about a week getting up to speed with TLA+, and then started writing up the formal proof of the process, defining the valid states etc. before letting the model checker at it. Problems were found. A number of them, in fact, mostly things that are hard to just mentally reason about that come with the increased complexity of the service being made from multiple parts that would need to communicate. A number of the bugs were of the type that would be unlikely to get exposed by any kind of unit/integration/functional testing. This is where the strong value proposition is for the use of TLA+, catching logical issues that are hard to reason about or test for, and Amazon has been using it to increasing amounts across services. The engineers involved, settled in to a refine/re-run cycle until they had eliminated the bugs. A final review was done of the TLA+ model and everyone was happy. After that they settled in to implementation phase, and they found that the way the model had ended up, it was relatively quick and simple to implement in Java. The model pretty much outlined everything that was needed in code. It became almost "fill in the blanks" coding, and there was a lot less mental effort involved for all in this stage. The initial optimistic estimate for the project was around 6 months, with extensive allowance for "shadow mode" running and verifying. The reality was that even with the time taken to learn, it was around 4 months from start to end, even including the time for engineers to learn TLA+ from scratch, and the service was launched with a high degree of confidence. The trick is that from here, you really need to think about keeping the model up to date. It should be seen as being as important as any other tests you've written for your actual code.
jlokier 6y ago
> TLC could, in some situations, check whether an uncountably infinite number of program executions I'd love to see an example of an uncountably infinite number of program executions checked. The set of all computable values as countable, after all.
- jlokier 6y ago
  Ah, I think I see it. The set of infinite, non-deterministic execution traces is uncountable (same reason real numbers composed of infinite sequences of digits from a finite set are uncountable). On the other hand, the set of infinite execution traces which can result from any deterministic, finite-size program is countable (because the set of programs is). But programs take inputs. And the set of possible inputs to an infinite execution trace is uncountable (same reason as reals, above). The prover needs to show that a program behaves correctly when given any sequence of inputs, even if the program never terminates and keeps taking new inputs forever. That requires proofs over an uncountable set of infinite execution traces.
- pron 6y ago
  Not all computations produce a value; most don't. Consider this TLA+ specification: VARIABLE x □(x ∈ 0..9) or, written in a form that can be checked by TLC: VARIABLE x x ∈ 0..9 ∧ □[x' ∈ 0..9]_x It says "x is a variable that is always an integer between 0 and 9, and it describes a system that nondeterministically assigns a number 0-9 to the variable x at each step, forever. It has an uncountable number of executions, each of infinite length, yet because it has a small number of states -- ten to be precise -- TLC can easily and quickly check many propositions about it. It is true that most of the behaviours don't have a corresponding determistic Turing machine and so most of those sequences are not computable, but it is not only a perfectly valid specification, but also a reasonable abstraction of real systems (e.g. a program that forever asks the user to input an integer between 0 and 9). On the other hand, this specification describes a system that picks an arbitrary natural number and then counts down to zero. It has only countably many executions (one for each initial number chosen), and each of them is finite in length -- i.e. they all terminate (I've omitted a liveness condition necessary to state that each computation will actually terminate, as it would mean little to those not familiar with TLA+ [1]): VARIABLE x x ∈ Nat ∧ □[x > 0 ∧ x' = x - 1]_x And yet TLC cannot check it because it has infinitely many states and TLC is an explicit-state model checker. In practice, we let TLC check a derived specification that overrides the value of Nat, the set of all natural numbers, with some finite set. [1]: To those familiar with TLA+, the real specification is: VARIABLE x LET Next ≜ x > 0 ∧ x' = x - 1 IN x ∈ Nat ∧ □[Next]_x ∧ WF_x(Next)
doonesbury 6y ago
>don't only not run all possible executions of a program, they don't even run it once. Can you please clarify? A tla+ spec (or pluscal to tla+) is supposed to verify against all possible interleavings of reachable states like spin. You seem to be saying something different
- pron 6y ago
  The model checker TLC, like SPIN, does verify "against all interleavings" but it doesn't "run" all of them; in fact, it runs none of them. Conceptually, it gives you the answer about all of them, but the algorithm doesn't actually run them.
  - salawat 6y ago
    Define "against all interleavings", or is that something I'd understand after reading TLA+'s documentation? I think I get the drift, I'm just wanting to confirm "read the docs" is the only missing bit.
  - doonesbury 6y ago
    OK, that's clearer. Thank you. Certainly not nit-picking, but it's worth pointing out in passing that computing the state to check qll the interleavings --- albeit not actually running each path through the reachable states but looking for safety or livness violations --- requires real work being super exponential in the worst case.

by pron 6y ago

elteto 6y ago

This is something I never quite understood with TLA+ (just from reading articles here and there, never actually used it). Let’s say I have a piece of C++ code and a TLA+ model for what it should be doing. How do I validate the C++ code with it?

vector_spaces 6y ago
My (probably wrong) understanding is that you don't -- you spec out the system design in TLA+, and use that to check if your design is sound (free of race conditions or certain other kinds of logic bugs). Checking that the TLA+ spec is implemented properly by the (say) C++ code is out of scope
pron 6y ago
You're asking the wrong question. Unless your program is very small or the property you wish to check is very simple, nothing can fully "validate" it. The question should be, is TLA+ more beneficial than just testing in improving program correctness? Humanity currently lacks the means to verify "deep" properties of code at any reasonable scale. Any tool that works at the code level either focuses on very simple properties (memory safety), complex but local properties of a small code-unit (Ada SPARK, Java's OpenJML), or deep properties of tiny programs (like seL4 and CompCert). These can be very important, but none truly offer the ability to "verify code" with some repeatable process at a generally-interesting scale. TLA+ could be used to do the same -- e.g. there is a C to TLA+ compiler -- but then it suffers from the same scale/depth/cost limitation of all code-level tools. So given that we can't just choose to verify a program, the question we want to answer is a different one: what is a good way, in a cost/benefit sense to achieve the correctness we want. Then you can ask whether TLA+ can offer such a way that is "better" in that sense than what you do now, which is likely testing. Those who have tried it, including myself, have come to the conclusion that in cases where the algorithm/design is sufficiently interesting or subtle, the answer is absolutely yes. The way TLA+ achieves it better than code level tools is that it allows you to describe your system at the level appropriate for answering your most important questions about it, and that level can be a much higher one than the code. So, to answer your question, the mere act of precisely expressing your system and correctness criteria in some chosen level of detail using very simple mathematics (high-school or first-year-college level), and then model-checking some interesting instances, is a good way (in the cost/benefit sense) to find bugs and make your program more correct. You compare it to the code by inspection. No, it does not give you 100% guarantees, but nothing else can, either. It is still worthwhile to do in addition to testing, as overall it can easier and cheaper in many cases to detect certain rare-yet-catstrophic bugs. Having said that, there are various techniques being explored that can check whether your program matches the TLA+ specification more mechanically than just by inspection, that might not be sound (i.e. give a 100% guarantee) but increase confidence while being cheap.
- zozbot234 6y ago
  > Humanity currently lacks the means to verify "deep" properties of code at any reasonable scale. Any tool that works at the code level either focuses on very simple properties (memory safety), complex but local properties of a small code-unit (Ada SPARK, Java's OpenJML), or deep properties of tiny programs (like seL4 and CompCert). This may be true in a sense, but then a TLA+ specification is also a "tiny program" of sorts. There's no reason why one couldn't use a "code-level" (end-to-end) interactive proof tool to verify TLA+-like specs. Even model checking can be subsumed elegantly within such a tool; a model checking run is simply a search for a refutation (as opposed to a positive proof) of some claimed properties wrt. the proposed spec.
User23 6y ago
A better question to ask is how do I formally derive a program that satisfies a given specification? Then validation is just mathematical “checking your work” and is easy or even trivial.
- pron 6y ago
  Except that's another question to which the answer is currently, "you don't", at least not at any interesting scale, not with TLA+ and not with anything else. But TLA+ is a tool aimed to help achieve correctness effectively, i.e. get a good cost/benefit for it. Between the highly scalable, low-confidence, testing, and the high-confidence, low-scale end-to-end verification, there's a huge swath of software correctness techniques, and the flexible TLA+ tries to hit a rather large swathe of that spectrum. In other words, we ask, is this better than what we do now in a sufficiently large portion of cases, rather than is this the silver bullet? The answer to the second question is no. I think the answer to the first one is yes.
  - User23 6y ago
    Formal program derivation satisfying a given specification has been around for well over half a century now. Hoare logic and the predicate calculus are entirely adequate for formal derivation in any language with well-documented semantics. Lamport himself has contributed significantly to the field. Unfortunately the American dominated programming industry has a strange phobia about mathematical reasoning[1]. The irrationality is exposed by patently ridiculous statements like that formal derivation doesn't scale. If you believe that, then you can't believe any nontrivial results from the hard physical sciences or pure mathematics. The actuality is that formal derivation makes building nontrivial constructs considerably easier. It is a tool, and like any tool when used properly it acts as a capability multiplier. [1] This is doubly confusing to me because it's not a matter of difficulty. Anyone with the mental horsepower to learn a modern programming language is easily capable of gaining proficiency in the predicate calculus.
    - zozbot234 6y ago
      > Hoare logic and the predicate calculus are entirely adequate for formal derivation in any language with well-documented semantics. Formal verification, yes. Formal derivation of a correct program from a spec, I really don't think so. In particular, I don't know of an easy way of deriving the required induction hypotheses/loop invariants to prove correctness of a program which includes recursion or loops.
k__ 6y ago
You don't validate the C++ code, you validate the algorithm before you implement it with C++. You have an idea for an algorithm, write it down with TLA+. TLA+ tells you if you screwed something up. You refine the algorithm until TLA+ says it's okay now. You implement the refined algorithm with the programming language of your choice. Everything that happens from that point is outside of TLA+'s power.
jen20 6y ago
For a fantastic intro to the basics and purpose of TLA+, I'd strongly recommend Scott Wlaschin's [1] talk from NDC Oslo this year. Like other academic-seeming subjects, Scott does a great job of applying it to real-world programming. That said, the answer to your exact question is that it doesn't validate the C++, it validates the algorithm. It's your job to ensure the C++ implements the algorithm as validated! [1]: https://www.youtube.com/watch?v=tqwcz-Yt9gQ https://www.youtube.com/watch?v=tqwcz-Yt9gQ
- pron 6y ago
  I wish people use "real" (pretty-printed) TLA+ syntax -- the syntax used when reading a spec -- when giving presentations rather than SANY's LaTeX-like ASCII syntax used to type them. The read/write ratio for maths, including TLA^+ specifications, is higher than for programs, and so there are two concrete syntaxes optimised for those two different modes. I think most people know that on the computer, maths is usually typed differently from how it's read, and they expect to read the maths, not the LaTeX source used to typeset it. It isn't any different for TLA^(+).
Twirrim 6y ago
An anecdotal example of the use of TLA+ The service I worked for in AWS had to built a key service, about 18 months-ish after launch. If the service got anything wrong, it would wipe out the customer's data. Evaluating the conditions and making the right decisions wasn't that complicated, but it was complicated enough as it involved multiple service components to meet certain scaling properties. The need to not do the wrong thing was crucial, and so the decision was made to use TLA+ to make sure things were correct. Two senior engineers had designed the overall process and it had been through architectural review (so almost all the senior engineers in the team had seen and reviewed it, and in this case I know at least one well respected principal engineer had been involved. Potential problems had been identified and resolved). Everyone felt confident, but we wanted to be sure. The engineers spent about a week getting up to speed with TLA+, and then started writing up the formal proof of the process, defining the valid states etc. before letting the model checker at it. Problems were found. A number of them, in fact, mostly things that are hard to just mentally reason about that come with the increased complexity of the service being made from multiple parts that would need to communicate. A number of the bugs were of the type that would be unlikely to get exposed by any kind of unit/integration/functional testing. This is where the strong value proposition is for the use of TLA+, catching logical issues that are hard to reason about or test for, and Amazon has been using it to increasing amounts across services. The engineers involved, settled in to a refine/re-run cycle until they had eliminated the bugs. A final review was done of the TLA+ model and everyone was happy. After that they settled in to implementation phase, and they found that the way the model had ended up, it was relatively quick and simple to implement in Java. The model pretty much outlined everything that was needed in code. It became almost "fill in the blanks" coding, and there was a lot less mental effort involved for all in this stage. The initial optimistic estimate for the project was around 6 months, with extensive allowance for "shadow mode" running and verifying. The reality was that even with the time taken to learn, it was around 4 months from start to end, even including the time for engineers to learn TLA+ from scratch, and the service was launched with a high degree of confidence. The trick is that from here, you really need to think about keeping the model up to date. It should be seen as being as important as any other tests you've written for your actual code.

jlokier 6y ago

> TLC could, in some situations, check whether an uncountably infinite number of program executions I'd love to see an example of an uncountably infinite number of program executions checked. The set of all computable values as countable, after all.

jlokier 6y ago
Ah, I think I see it. The set of infinite, non-deterministic execution traces is uncountable (same reason real numbers composed of infinite sequences of digits from a finite set are uncountable). On the other hand, the set of infinite execution traces which can result from any deterministic, finite-size program is countable (because the set of programs is). But programs take inputs. And the set of possible inputs to an infinite execution trace is uncountable (same reason as reals, above). The prover needs to show that a program behaves correctly when given any sequence of inputs, even if the program never terminates and keeps taking new inputs forever. That requires proofs over an uncountable set of infinite execution traces.
pron 6y ago
Not all computations produce a value; most don't. Consider this TLA+ specification: VARIABLE x □(x ∈ 0..9) or, written in a form that can be checked by TLC: VARIABLE x x ∈ 0..9 ∧ □[x' ∈ 0..9]_x It says "x is a variable that is always an integer between 0 and 9, and it describes a system that nondeterministically assigns a number 0-9 to the variable x at each step, forever. It has an uncountable number of executions, each of infinite length, yet because it has a small number of states -- ten to be precise -- TLC can easily and quickly check many propositions about it. It is true that most of the behaviours don't have a corresponding determistic Turing machine and so most of those sequences are not computable, but it is not only a perfectly valid specification, but also a reasonable abstraction of real systems (e.g. a program that forever asks the user to input an integer between 0 and 9). On the other hand, this specification describes a system that picks an arbitrary natural number and then counts down to zero. It has only countably many executions (one for each initial number chosen), and each of them is finite in length -- i.e. they all terminate (I've omitted a liveness condition necessary to state that each computation will actually terminate, as it would mean little to those not familiar with TLA+ [1]): VARIABLE x x ∈ Nat ∧ □[x > 0 ∧ x' = x - 1]_x And yet TLC cannot check it because it has infinitely many states and TLC is an explicit-state model checker. In practice, we let TLC check a derived specification that overrides the value of Nat, the set of all natural numbers, with some finite set. [1]: To those familiar with TLA+, the real specification is: VARIABLE x LET Next ≜ x > 0 ∧ x' = x - 1 IN x ∈ Nat ∧ □[Next]_x ∧ WF_x(Next)

doonesbury 6y ago

>don't only not run all possible executions of a program, they don't even run it once. Can you please clarify? A tla+ spec (or pluscal to tla+) is supposed to verify against all possible interleavings of reachable states like spin. You seem to be saying something different

pron 6y ago
The model checker TLC, like SPIN, does verify "against all interleavings" but it doesn't "run" all of them; in fact, it runs none of them. Conceptually, it gives you the answer about all of them, but the algorithm doesn't actually run them.
- salawat 6y ago
  Define "against all interleavings", or is that something I'd understand after reading TLA+'s documentation? I think I get the drift, I'm just wanting to confirm "read the docs" is the only missing bit.
- doonesbury 6y ago
  OK, that's clearer. Thank you. Certainly not nit-picking, but it's worth pointing out in passing that computing the state to check qll the interleavings --- albeit not actually running each path through the reachable states but looking for safety or livness violations --- requires real work being super exponential in the worst case.