17 ms·

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

by 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.
  - pron 6y ago
    > There's no reason why one couldn't use a "code-level" (end-to-end) interactive proof tool to verify TLA+-like specs. Sure, and that is what TLA+, together with its tools, aim to do. The problem is the relation between the spec, that you can precisely verify, and the program it aims to abstract. The advantage TLA+ has over code-level tools in this respect is that those tools use code as their specification language -- i.e. a formal language that is deterministic enough to efficiently compile/interpret and execute. But TLA+ allows you to specify at an arbitrary level, even levels with a lot of nondeterminism that precludes compilation, hence the difference between it and code. For example, in TLA+ you can say, suppose I have a subroutine that sorts, and then build and check your specification on top of that without actually writing a sorting routine that can be executed. Similarly, you can say something like, "some hashing function is used" without actually writing any specific hashing function. This way, you can write a specification that's small enough to be verified, yet captures the interesting aspects of a system that's made of too much code to verify at the code level.
    - zozbot234 6y ago
      > But TLA+ allows you to specify at an arbitrary level, even levels with a lot of nondeterminism that precludes compilation, hence the difference between it and code. ... Similarly, you can say something like, "some hashing function is used" without actually writing any specific hashing function. This can also be done in many end-to-end tools. Typically, these tools allow for end-to-end proof based on the actual code; they don't require it.
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.

by elteto 6y ago

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.
- pron 6y ago
  > There's no reason why one couldn't use a "code-level" (end-to-end) interactive proof tool to verify TLA+-like specs. Sure, and that is what TLA+, together with its tools, aim to do. The problem is the relation between the spec, that you can precisely verify, and the program it aims to abstract. The advantage TLA+ has over code-level tools in this respect is that those tools use code as their specification language -- i.e. a formal language that is deterministic enough to efficiently compile/interpret and execute. But TLA+ allows you to specify at an arbitrary level, even levels with a lot of nondeterminism that precludes compilation, hence the difference between it and code. For example, in TLA+ you can say, suppose I have a subroutine that sorts, and then build and check your specification on top of that without actually writing a sorting routine that can be executed. Similarly, you can say something like, "some hashing function is used" without actually writing any specific hashing function. This way, you can write a specification that's small enough to be verified, yet captures the interesting aspects of a system that's made of too much code to verify at the code level.
  - zozbot234 6y ago
    > But TLA+ allows you to specify at an arbitrary level, even levels with a lot of nondeterminism that precludes compilation, hence the difference between it and code. ... Similarly, you can say something like, "some hashing function is used" without actually writing any specific hashing function. This can also be done in many end-to-end tools. Typically, these tools allow for end-to-end proof based on the actual code; they don't require it.

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.