8 ms·

I had the privilege of attending this lecture in person. One eerie thing about it was that Dr. Lamport didn't improvise at all - he just read from the slides an

I had the privilege of attending this lecture in person. One eerie thing about it was that Dr. Lamport didn't improvise at all - he just read from the slides and that was all he had to say! Overall it was a good introduction to TLA+ which I think has a big advantage of being very simple to understand and use - no complicated math needed apart from set theory. What I didn't quite understand is how to make sure that your models are implementable in code (if you start with a model) and faithfully describe your actual code and the reality itself. Seems like all bugs will end up lurking in this gap between the model and what is actually executed and there is no reliable way to close this gap.

pron 7y ago
This is a common question among TLA+ beginners. There can be bugs in the implementation. Those would either be bugs due to a mistranslation of the spec -- i.e., an error in the implementation -- or, because the spec also implicitly or explicitly describes the assumptions about the environment, a mismatch between the actual environment (hardware, software stack, user behavior) and the spec -- i.e. an error in the spec. In both cases, having the spec makes finding those bugs easier, and in the first case, the bugs are usually cheap to find and fix. The costliest bugs are in the design, and that's where TLC, a model checker for TLA+, can automatically spot them. Now, what if you want a formal -- i.e. mechanical -- relationship between the code and the spec? In principle, this is possible, and has been done; e.g. see [1] for C, and there have been other, similar projects for Java. In practice, we don't do it. Why? Well, we can't. There is no known technique that can verify anything but small programs/specs for arbitrary correctness properties. The reason is that the scalability of all formal methods has limitations. Currently, we can formally verify a few thousand lines of formal specification. That specification can be either code or a high-level spec. That means that we can either verify very small programs, or a high-level spec that represents a large program. The latter is the only thing available to us to help with large program, and how TLA+ is normally used. Small programs are verified end-to-end (i.e., that the actual code, or even machine code, conforms to a high-level spec) only in very special, niche, cases, and/or at a great cost. What else can we do? We can verify code not against a high-level spec, but against some specification of small, local properties. This way, every code unit is verified separately [2]. This could help catch errors in translation, but, while useful, the benefit is not as great as verifying a high-level spec. This approach, a high-level spec verified formally, translated informally to code, and the code is then verified formally against local properties only, is how Altran UK builds their software; they use the older Z, instead of TLA+ for the high-level spec, and SPARK for code-level verification. Local properties can be verified with languages/tools like SPARK, JML and its various tools for Java, ACSL and various tools for C, and others, including dependent type languages used in research. There is also an affordable way to mechanically check a program's conformance to a TLA+ spec, but only approximately -- it isn't sound. It's called "model-based trace-checking," and the idea is to grab logs from the program, or an entire distributed system, and let TLC check that they conform to a possible execution of the spec. I've written about this technique here [3]. It is important to realize that all kinds of software assurance techniques, from proof assistants to unit tests, come with significant tradeoffs to confidence, effort and scale, and that none can guarantee that a system will not fail. We must choose an appropriate balance for our specific system, usually by employing more than one approach (usually more than two). Personally, I think that high-level TLA+ specifications, checked with the TLC model checker (not with the TLAPS proof assistant) are at a pretty good sweet-spot for a relatively large number of mainstream software projects in terms of cost/benefit compared to other tools and approaches (but should still be combined with testing and code review). [1]: https://cedric.cnam.fr/fichiers/art_3439.pdf https://cedric.cnam.fr/fichiers/art_3439.pdf [2]: You may think that it's possible to verify local properties of local units, and then compose them to ensure conformance to a high-level spec. Unfortunately, this way doesn't beat the scalability limitation, and also works only on very small programs. [3]: https://pron.github.io/files/Trace.pdf https://pron.github.io/files/Trace.pdf
- throwawayjava 7y ago
  > In practice, we don't do it. There are lots of very large Coq code bases that work just fine with code extraction. Scalability of extraction isn't the problem. Is it really true that TLA scales to large programs? Why isn't there a Compcert in TLA? Why isn't there a Flyspec in TLA? And how about stuff like CertiGrad, where just the spec is pretty involved? My impression has always been that Coq/HOL scale and TLA-style systems break down once your spec gets big enough (let alone the impl).
  - pron 7y ago
    > There are lots of very large Coq code bases that work just fine with code extraction. Scalability of extraction isn't the problem. The largest programs ever verified end-to-end with Coq, Isabelle, or any other proof assistant correspond to about ~10KLOC of C, or less than 1/5 of jQuery (although such a small program could require up to 50K or even 100K lines of proofs). And even those certainly-non-trivial-yet-rather-tiny programs took years of efforts by experts. Moreover, concessions in the programs' design and choice of algorithms had to be made in order to make verification feasible at all. And I agree that extraction doesn't suffer from a scalability problem. What does is the ability to verify the spec in the first place. If we could write proofs that correspond to programs with 100K, then extracting an executable would not be the isse, but we can't (or, at least, we don't know how). > Is it really true that TLA scales to large programs? Yes. Again, there's no magic: we can only verify so many lines of a formal spec (of which code is an example). So it's either a small program or a small high-level spec that corresponds to a large program. No known technique can affordably verify large (or even medium, or even non-small) programs, end-to-end, for arbitrary functional correctness properties. > Why isn't there a Compcert in TLA? There are programs fifty times the size of CompCert that used TLA+ (to be honest, most real-world programs are 50x the size of CompCert), but not for end-to-end verification; i.e. there is an informal translation of spec to code. Unlike Coq, which is usually used for research or by researchers, TLA+ is used in industry and by "ordinary" engineers without lengthy training in formal logic, so there aren't many papers written about its use, but here's one[1]. Ironically, another reason you don't see as many papers about verification in TLA+ as in Coq is that its use is much simpler. I once saw a paper about specifying and verifying a program's time-complexity in Coq. No one would ever write such a paper about TLA+, because it's just too easy; a TLA+ beginner could do it in their first week of learning (the main reason there's a paper about using TLA+ for PharOS is because they used TLAPS, the TLA+ proof assistant, rather than the TLC model checker, which made the work academically interesting). In any event, if someone is interested in using any of those tools "in production," I recommend they give them all a try. [1]: https://members.loria.fr/SMerz/papers/abz2016-pharos.html https://members.loria.fr/SMerz/papers/abz2016-pharos.html

pron 7y ago

This is a common question among TLA+ beginners. There can be bugs in the implementation. Those would either be bugs due to a mistranslation of the spec -- i.e., an error in the implementation -- or, because the spec also implicitly or explicitly describes the assumptions about the environment, a mismatch between the actual environment (hardware, software stack, user behavior) and the spec -- i.e. an error in the spec. In both cases, having the spec makes finding those bugs easier, and in the first case, the bugs are usually cheap to find and fix. The costliest bugs are in the design, and that's where TLC, a model checker for TLA+, can automatically spot them. Now, what if you want a formal -- i.e. mechanical -- relationship between the code and the spec? In principle, this is possible, and has been done; e.g. see [1] for C, and there have been other, similar projects for Java. In practice, we don't do it. Why? Well, we can't. There is no known technique that can verify anything but small programs/specs for arbitrary correctness properties. The reason is that the scalability of all formal methods has limitations. Currently, we can formally verify a few thousand lines of formal specification. That specification can be either code or a high-level spec. That means that we can either verify very small programs, or a high-level spec that represents a large program. The latter is the only thing available to us to help with large program, and how TLA+ is normally used. Small programs are verified end-to-end (i.e., that the actual code, or even machine code, conforms to a high-level spec) only in very special, niche, cases, and/or at a great cost. What else can we do? We can verify code not against a high-level spec, but against some specification of small, local properties. This way, every code unit is verified separately [2]. This could help catch errors in translation, but, while useful, the benefit is not as great as verifying a high-level spec. This approach, a high-level spec verified formally, translated informally to code, and the code is then verified formally against local properties only, is how Altran UK builds their software; they use the older Z, instead of TLA+ for the high-level spec, and SPARK for code-level verification. Local properties can be verified with languages/tools like SPARK, JML and its various tools for Java, ACSL and various tools for C, and others, including dependent type languages used in research. There is also an affordable way to mechanically check a program's conformance to a TLA+ spec, but only approximately -- it isn't sound. It's called "model-based trace-checking," and the idea is to grab logs from the program, or an entire distributed system, and let TLC check that they conform to a possible execution of the spec. I've written about this technique here [3]. It is important to realize that all kinds of software assurance techniques, from proof assistants to unit tests, come with significant tradeoffs to confidence, effort and scale, and that none can guarantee that a system will not fail. We must choose an appropriate balance for our specific system, usually by employing more than one approach (usually more than two). Personally, I think that high-level TLA+ specifications, checked with the TLC model checker (not with the TLAPS proof assistant) are at a pretty good sweet-spot for a relatively large number of mainstream software projects in terms of cost/benefit compared to other tools and approaches (but should still be combined with testing and code review). [1]: https://cedric.cnam.fr/fichiers/art_3439.pdf https://cedric.cnam.fr/fichiers/art_3439.pdf [2]: You may think that it's possible to verify local properties of local units, and then compose them to ensure conformance to a high-level spec. Unfortunately, this way doesn't beat the scalability limitation, and also works only on very small programs. [3]: https://pron.github.io/files/Trace.pdf https://pron.github.io/files/Trace.pdf

throwawayjava 7y ago
> In practice, we don't do it. There are lots of very large Coq code bases that work just fine with code extraction. Scalability of extraction isn't the problem. Is it really true that TLA scales to large programs? Why isn't there a Compcert in TLA? Why isn't there a Flyspec in TLA? And how about stuff like CertiGrad, where just the spec is pretty involved? My impression has always been that Coq/HOL scale and TLA-style systems break down once your spec gets big enough (let alone the impl).
- pron 7y ago
  > There are lots of very large Coq code bases that work just fine with code extraction. Scalability of extraction isn't the problem. The largest programs ever verified end-to-end with Coq, Isabelle, or any other proof assistant correspond to about ~10KLOC of C, or less than 1/5 of jQuery (although such a small program could require up to 50K or even 100K lines of proofs). And even those certainly-non-trivial-yet-rather-tiny programs took years of efforts by experts. Moreover, concessions in the programs' design and choice of algorithms had to be made in order to make verification feasible at all. And I agree that extraction doesn't suffer from a scalability problem. What does is the ability to verify the spec in the first place. If we could write proofs that correspond to programs with 100K, then extracting an executable would not be the isse, but we can't (or, at least, we don't know how). > Is it really true that TLA scales to large programs? Yes. Again, there's no magic: we can only verify so many lines of a formal spec (of which code is an example). So it's either a small program or a small high-level spec that corresponds to a large program. No known technique can affordably verify large (or even medium, or even non-small) programs, end-to-end, for arbitrary functional correctness properties. > Why isn't there a Compcert in TLA? There are programs fifty times the size of CompCert that used TLA+ (to be honest, most real-world programs are 50x the size of CompCert), but not for end-to-end verification; i.e. there is an informal translation of spec to code. Unlike Coq, which is usually used for research or by researchers, TLA+ is used in industry and by "ordinary" engineers without lengthy training in formal logic, so there aren't many papers written about its use, but here's one[1]. Ironically, another reason you don't see as many papers about verification in TLA+ as in Coq is that its use is much simpler. I once saw a paper about specifying and verifying a program's time-complexity in Coq. No one would ever write such a paper about TLA+, because it's just too easy; a TLA+ beginner could do it in their first week of learning (the main reason there's a paper about using TLA+ for PharOS is because they used TLAPS, the TLA+ proof assistant, rather than the TLC model checker, which made the work academically interesting). In any event, if someone is interested in using any of those tools "in production," I recommend they give them all a try. [1]: https://members.loria.fr/SMerz/papers/abz2016-pharos.html https://members.loria.fr/SMerz/papers/abz2016-pharos.html