6 ms·

Principles of TLA+

121 points by pramodbiligiri 9y ago

plinkplonk 9y ago
Very nice. I really appreciate you placing TLA+ in context with alternate approaches. I look forward to seeing the followup posts. PS: How are you generating these pages? Jekyll? something else? EDIT: This probably needs editing -- "nor will reading the posts will not teach you how to write good specifications;" I think you probably meant to write "nor will reading the posts teach you how to write good specifications;"
- pron 9y ago
  Yep, Jekyll. And I've fixed the mistake. Thank you!
deleted 9y ago
[deleted]
michaelmior 9y ago
Leslie Lamport has a video course[0] on TLA+ that's slowly being released. I created an RSS feed[1] that updates as new episods are released. [0] https://lamport.azurewebsites.net/video/videos.html https://lamport.azurewebsites.net/video/videos.html [1] http://fetchrss.com/rss/58d198538a93f8ef3b8b4567741573560.atom http://fetchrss.com/rss/58d198538a93f8ef3b8b4567741573560.at...
avodonosov 9y ago
There are interesting pieces of information, but its very long
nickpsecurity 9y ago
@ pron This is a great write-up I learn quite a bit from but way, way, too long. There's a lot of redundancy in here much like my first sentence. You should try to condense this since the redundancy might make a chunk of the modern crowd think the rest of what they see in the scrollbar will be the same and move on to next article. The last write-up you sent me didn't have that problem. I'm glad I saw this, too, as I recently watched your video citing all the mathematical evidence that correctness may not decompose. I got one or two counterpoints to email you later but overall want your data peer reviewed by people highly experienced in abstractions in large, verification efforts and making VCG's given their output will have to compose, too. Let all the pro's duke it out with arguments, proofs, and attempts at actual projects. I'll reserve judgment until the dust settles. :)
- jacobparker 9y ago
  > I recently watched your video citing all the mathematical evidence that correctness may not decompose For myself and others, are you referring to the video here: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity ?
  - nickpsecurity 9y ago
    Yeah, that was it.
- pron 9y ago
  You are absolutely right about the repetition (and part 1 is my least favorite installment in the series), but reducing it in size took too much time. If you have any editing suggestions, please email me. As to the the "mathematical evidence", it is a published, peer reviewed, 2005 proof, and a rather simple one. Practical experience has little to do with it, because we need to separate two things: the computational complexity of the worst case -- which is provably exponential not only in the number of components but also in the size of the state space of each component -- and cases that arise in practice. This is just like the halting theorem, that states the worst-case undecidability, but does not claim that every instance is undecidable. However, the interesting question is how far are commonly encountered cases from the worst case. When it comes to symbolic model checking (i.e., taking advantage of syntactic structure), even though we would have thought the problem is essentially easier (in the worst case), it is provably just as hard, and moreover, we have years of experience (cited in my post) that common cases are close to the worst-case. When it comes to "decomposability of correctness", I cited no empirical evidence. Nevertheless, it should be noted that no large or even medium-sized software has ever been fully verified, so I don't think anyone believes the problem is easy.
  - nickpsecurity 9y ago
    " it is a published, peer reviewed, 2005 proof, and a rather simple one." Proofs can be wrong or irrelevant in practice. An example is not being able to prove the tetmination of executing arbitrary programs. Sure I can: it's called a watch-dog timer. So, Im wanting it peer reviewed. Plus, it's critical to know for sure that and correctness composition to determine what to invest in for software assurance R&D. "Nevertheless, it should be noted that no large or even medium-sized software has ever been fully verified, so I don't think anyone believes the problem is easy." Never easy. :) However, I still think we should consider counting the deep verifications. You keep saying they havent went upward to verify a program of certain size as if it means something. I know only one that tried (Verisoft for Hyper-V). Most went downward toward the gate level including Verisoft where Microsoft's was just a side item. Verisoft did app correctness to some degree, down to C code, its compiler, the OS, the microkernel, and CPU tying it all together. DeepSpec just tied piles of high-level and low-level code together. So, such methods should allow us to achieve the same amount of complexity going upward using same abstraction and shortcut techniques. We havent done that much upward because they just been working the other way. Now, what they'll ultimately achieve may or may not be that good. Best approach might be to throw DeepSpec's DSL's and tooling at a large, complex application whose code is FOSS and accessible. I suggest an application server with compression, encryption, caching, and error handling as a good way to stress that project from multiple angles.
storrgie 9y ago
writeup aside, this is a really nice template... similar to tufte margins. I'd love to see the source/style for the site...
- pron 9y ago
  It's a combination of the tufte and monochrome Jekyll templates.
dgreensp 9y ago
Great article, and I look forward to the next! I've been meaning to learn about TLA+ for a while. One thought I didn't see expressed, in all the comparisons of tools and approaches, is that sometimes you don't care about time and state. In purely "transformational" programs, like compilers, for example, all state is incidental complexity, so we can analyze them as pure functions. Meanwhile, all the questions such as whether we can just execute the spec and whether we can prove properties of real programs remain. New web frameworks are trying to keep the parts that deal with time and state as small and self-contained as possible, leaving the rest to be described using functions. Couldn't we say that the factor of "do you care about time" is behind observations such as that TLA+ is mostly popular with concurrent and distributed systems, or that approaches that only look at function contracts often apply to pieces of a program but not the whole? As a more specific statement than, for example, that distributed systems are particularly hard so they necessitate particularly powerful tools.
- pron 9y ago
  > all state is incidental complexity This is an example of the "Whorfian syndrome" of functional programming. Program state is not the same as the problem of "global mutable state" often cited as a cause of programming bugs. When it comes to program analysis, I see no reason why reasoning about state would be any different, let alone more complicated, than reasoning "trasnformationally". It's exactly like the difference between: h(g(f(x))) and let a = f(x) b = g(a) c = h(b) Reasoning about the two is exactly the same, and the program state in both cases is also identical: you have three states. I also disagree that there is no interest in time or space in purely trasformative systems. First, A trasnformative algorithm that is, say, doubly exponential in time or space is just as wrong as a database that fails to give an answer. Second -- and more importantly -- reasoning about a recursive algorithm is exactly like reasoning about state. There is no way to show that Quicksort works without reasoning about state. You may not mention it explicitly in your chosen formalism or you may call it by a different name, but it's there, and you're taking it into consideration. Also, TLA+ is a universal formalism, and, as you'll see in part 2, there's nothing stopping you from representing everything as functions without any passage of time. The reasoning is identical -- there is no added complexity at all, incidental or otherwise -- but may be a matter of personal aesthetic preference. Because TLA+ is a mathematical notation, substitution and "equational reasoning" works just as well even though time can be expressed. I would say that the main difference between TLA+ and the functional approaches, is that in TLA+ you reason purely mathematically, while in the functional approaches you reason within a (complex) programming language. It's very hard to talk about popularity, because, as far as I know, there are no "functional" tools that are used in the industry at all (certainly not without help from academics). Part of the reason may be due to the fact that so far, software companies that require verification usually write reactive realtime software rather than compilers, so they use tools like B-Method, SCADE, SPIN and TLA+. Another reason is that with the exception of the very good, but rather limited Why3, there are simply no industrial-strength verification tools out there aimed at industrial use rather than research.
hwayne 9y ago
First of all, as always, huge respect for your work, and I'm looking forward to reading the rest of the posts. There is something I'd like to start a discussion on, though: > nor will reading these posts teach you how to write good specifications; so this series is neither necessary nor sufficient for putting TLA+ to good use, but I think it is both necessary and sufficient for understanding it. Emphasis on the 'good specifications' part: I think this is a _huge_ oversight in the TLA+ community and the biggest barrier to its current adoption. The problem isn't that people don't understand (or can't understand) the theory behind it, yet it's the thing everybody focuses on teaching. The problem is specification: _nobody_ is talking about how to actually use TLA+. In fact, some of the advice given is actively harmful! One example: in _Specifying Systems_, Lamport defines a memory cache with the operator `NoVal == CHOOSE v : v \notin Val`. He explicitly calls this best practice, because adding a `NOVAL` constant would be making the model more complex. Except unbounded CHOOSE is not checkable by TLC! While `NoVal` is nice for abstract specifications, it breaks things in the 99% of cases where you're actually using TLA+. I find it telling that the majority of example TLA+ specs "in the wild" are either abstract algorithms or optimization problems. The things you don't find? How to write good invariants. When you should be using raw TLA+ versus the PlusCal syntax. Example models. Optimization your model checking. The stuff that might get people to start using TLA+ and _keep_ using it. Again, none of these are criticisms of your work or your writing. I just wanted to openly say that if your goal is to get people interested in the theory of TLA+, it's great, but if it is to get people interested in use of it, a lack of good theoretical introductions isn't the main barrier.
- pron 9y ago
  This is precisely the kind of discussion I want to see on the mailing list or /r/tlaplus. HN is not very conducive to internal community discussions.
- pron 9y ago
  > The problem is specification: _nobody_ is talking about how to actually use TLA+. I think that is Lamport's focus; he talks about this more than he talks about the theory. Plus, you have the Dr. TLA+ series. > Lamport defines a memory cache with the operator `NoVal == CHOOSE v : v \notin Val`. He explicitly calls this best practice, because adding a `NOVAL` constant would be making the model more complex. Except unbounded CHOOSE is not checkable by TLC! While `NoVal` is nice for abstract specifications, it breaks things in the 99% of cases where you're actually using TLA+. You definitely should write `NoVal == CHOOSE v : v \notin Val` in your spec (as that clarifies the intent) and override it as a "model value" (i.e., a constant) in TLC. This is best practice. Even `∃ x ∈ Nat` is not checkable by TLC, yet best practice is to leave it like that (as that is the intent), and override `Nat` in TLC. In either case, the more general specification is verifiable in TLAPS. > Example models. Optimization your model checking. The stuff that might get people to start using TLA+ and _keep_ using it. This kind of discussion is very common on the mailing list (there are a lot of hidden gems there), but I would be very happy to see more people write "pro tips" and publishing them. > Again, none of these are criticisms of your work or your writing. I just wanted to openly say that if your goal is to get people interested in the theory of TLA+, it's great, but if it is to get people interested in use of it, a lack of good theoretical introductions isn't the main barrier. My personal goal in this particular series is just to get people interested in the theory. But TLA+ is still extremely young when it comes to "use in the wild". It was virtually nonexistent before 2012, and started slowly gaining traction only around 2014, when Amazon published their report. As you can see, writing short and to the point tips, tricks and guides isn't exactly my forté, but they are extremely important. As this tiny community grows, there will hopefully be those that will fill in the missing gaps. Your own tutorial is a great start.

Very nice. I really appreciate you placing TLA+ in context with alternate approaches. I look forward to seeing the followup posts. PS: How are you generating these pages? Jekyll? something else? EDIT: This probably needs editing -- "nor will reading the posts will not teach you how to write good specifications;" I think you probably meant to write "nor will reading the posts teach you how to write good specifications;"

pron 9y ago
Yep, Jekyll. And I've fixed the mistake. Thank you!

deleted 9y ago

[deleted]

michaelmior 9y ago

Leslie Lamport has a video course[0] on TLA+ that's slowly being released. I created an RSS feed[1] that updates as new episods are released. [0] https://lamport.azurewebsites.net/video/videos.html https://lamport.azurewebsites.net/video/videos.html [1] http://fetchrss.com/rss/58d198538a93f8ef3b8b4567741573560.atom http://fetchrss.com/rss/58d198538a93f8ef3b8b4567741573560.at...

avodonosov 9y ago

There are interesting pieces of information, but its very long

nickpsecurity 9y ago

@ pron This is a great write-up I learn quite a bit from but way, way, too long. There's a lot of redundancy in here much like my first sentence. You should try to condense this since the redundancy might make a chunk of the modern crowd think the rest of what they see in the scrollbar will be the same and move on to next article. The last write-up you sent me didn't have that problem. I'm glad I saw this, too, as I recently watched your video citing all the mathematical evidence that correctness may not decompose. I got one or two counterpoints to email you later but overall want your data peer reviewed by people highly experienced in abstractions in large, verification efforts and making VCG's given their output will have to compose, too. Let all the pro's duke it out with arguments, proofs, and attempts at actual projects. I'll reserve judgment until the dust settles. :)

jacobparker 9y ago
> I recently watched your video citing all the mathematical evidence that correctness may not decompose For myself and others, are you referring to the video here: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity ?
- nickpsecurity 9y ago
  Yeah, that was it.
pron 9y ago
You are absolutely right about the repetition (and part 1 is my least favorite installment in the series), but reducing it in size took too much time. If you have any editing suggestions, please email me. As to the the "mathematical evidence", it is a published, peer reviewed, 2005 proof, and a rather simple one. Practical experience has little to do with it, because we need to separate two things: the computational complexity of the worst case -- which is provably exponential not only in the number of components but also in the size of the state space of each component -- and cases that arise in practice. This is just like the halting theorem, that states the worst-case undecidability, but does not claim that every instance is undecidable. However, the interesting question is how far are commonly encountered cases from the worst case. When it comes to symbolic model checking (i.e., taking advantage of syntactic structure), even though we would have thought the problem is essentially easier (in the worst case), it is provably just as hard, and moreover, we have years of experience (cited in my post) that common cases are close to the worst-case. When it comes to "decomposability of correctness", I cited no empirical evidence. Nevertheless, it should be noted that no large or even medium-sized software has ever been fully verified, so I don't think anyone believes the problem is easy.
- nickpsecurity 9y ago
  " it is a published, peer reviewed, 2005 proof, and a rather simple one." Proofs can be wrong or irrelevant in practice. An example is not being able to prove the tetmination of executing arbitrary programs. Sure I can: it's called a watch-dog timer. So, Im wanting it peer reviewed. Plus, it's critical to know for sure that and correctness composition to determine what to invest in for software assurance R&D. "Nevertheless, it should be noted that no large or even medium-sized software has ever been fully verified, so I don't think anyone believes the problem is easy." Never easy. :) However, I still think we should consider counting the deep verifications. You keep saying they havent went upward to verify a program of certain size as if it means something. I know only one that tried (Verisoft for Hyper-V). Most went downward toward the gate level including Verisoft where Microsoft's was just a side item. Verisoft did app correctness to some degree, down to C code, its compiler, the OS, the microkernel, and CPU tying it all together. DeepSpec just tied piles of high-level and low-level code together. So, such methods should allow us to achieve the same amount of complexity going upward using same abstraction and shortcut techniques. We havent done that much upward because they just been working the other way. Now, what they'll ultimately achieve may or may not be that good. Best approach might be to throw DeepSpec's DSL's and tooling at a large, complex application whose code is FOSS and accessible. I suggest an application server with compression, encryption, caching, and error handling as a good way to stress that project from multiple angles.

storrgie 9y ago

writeup aside, this is a really nice template... similar to tufte margins. I'd love to see the source/style for the site...

pron 9y ago
It's a combination of the tufte and monochrome Jekyll templates.

dgreensp 9y ago

Great article, and I look forward to the next! I've been meaning to learn about TLA+ for a while. One thought I didn't see expressed, in all the comparisons of tools and approaches, is that sometimes you don't care about time and state. In purely "transformational" programs, like compilers, for example, all state is incidental complexity, so we can analyze them as pure functions. Meanwhile, all the questions such as whether we can just execute the spec and whether we can prove properties of real programs remain. New web frameworks are trying to keep the parts that deal with time and state as small and self-contained as possible, leaving the rest to be described using functions. Couldn't we say that the factor of "do you care about time" is behind observations such as that TLA+ is mostly popular with concurrent and distributed systems, or that approaches that only look at function contracts often apply to pieces of a program but not the whole? As a more specific statement than, for example, that distributed systems are particularly hard so they necessitate particularly powerful tools.

pron 9y ago
> all state is incidental complexity This is an example of the "Whorfian syndrome" of functional programming. Program state is not the same as the problem of "global mutable state" often cited as a cause of programming bugs. When it comes to program analysis, I see no reason why reasoning about state would be any different, let alone more complicated, than reasoning "trasnformationally". It's exactly like the difference between: h(g(f(x))) and let a = f(x) b = g(a) c = h(b) Reasoning about the two is exactly the same, and the program state in both cases is also identical: you have three states. I also disagree that there is no interest in time or space in purely trasformative systems. First, A trasnformative algorithm that is, say, doubly exponential in time or space is just as wrong as a database that fails to give an answer. Second -- and more importantly -- reasoning about a recursive algorithm is exactly like reasoning about state. There is no way to show that Quicksort works without reasoning about state. You may not mention it explicitly in your chosen formalism or you may call it by a different name, but it's there, and you're taking it into consideration. Also, TLA+ is a universal formalism, and, as you'll see in part 2, there's nothing stopping you from representing everything as functions without any passage of time. The reasoning is identical -- there is no added complexity at all, incidental or otherwise -- but may be a matter of personal aesthetic preference. Because TLA+ is a mathematical notation, substitution and "equational reasoning" works just as well even though time can be expressed. I would say that the main difference between TLA+ and the functional approaches, is that in TLA+ you reason purely mathematically, while in the functional approaches you reason within a (complex) programming language. It's very hard to talk about popularity, because, as far as I know, there are no "functional" tools that are used in the industry at all (certainly not without help from academics). Part of the reason may be due to the fact that so far, software companies that require verification usually write reactive realtime software rather than compilers, so they use tools like B-Method, SCADE, SPIN and TLA+. Another reason is that with the exception of the very good, but rather limited Why3, there are simply no industrial-strength verification tools out there aimed at industrial use rather than research.

hwayne 9y ago

First of all, as always, huge respect for your work, and I'm looking forward to reading the rest of the posts. There is something I'd like to start a discussion on, though: > nor will reading these posts teach you how to write good specifications; so this series is neither necessary nor sufficient for putting TLA+ to good use, but I think it is both necessary and sufficient for understanding it. Emphasis on the 'good specifications' part: I think this is a _huge_ oversight in the TLA+ community and the biggest barrier to its current adoption. The problem isn't that people don't understand (or can't understand) the theory behind it, yet it's the thing everybody focuses on teaching. The problem is specification: _nobody_ is talking about how to actually use TLA+. In fact, some of the advice given is actively harmful! One example: in _Specifying Systems_, Lamport defines a memory cache with the operator `NoVal == CHOOSE v : v \notin Val`. He explicitly calls this best practice, because adding a `NOVAL` constant would be making the model more complex. Except unbounded CHOOSE is not checkable by TLC! While `NoVal` is nice for abstract specifications, it breaks things in the 99% of cases where you're actually using TLA+. I find it telling that the majority of example TLA+ specs "in the wild" are either abstract algorithms or optimization problems. The things you don't find? How to write good invariants. When you should be using raw TLA+ versus the PlusCal syntax. Example models. Optimization your model checking. The stuff that might get people to start using TLA+ and _keep_ using it. Again, none of these are criticisms of your work or your writing. I just wanted to openly say that if your goal is to get people interested in the theory of TLA+, it's great, but if it is to get people interested in use of it, a lack of good theoretical introductions isn't the main barrier.

pron 9y ago
This is precisely the kind of discussion I want to see on the mailing list or /r/tlaplus. HN is not very conducive to internal community discussions.
pron 9y ago
> The problem is specification: _nobody_ is talking about how to actually use TLA+. I think that is Lamport's focus; he talks about this more than he talks about the theory. Plus, you have the Dr. TLA+ series. > Lamport defines a memory cache with the operator `NoVal == CHOOSE v : v \notin Val`. He explicitly calls this best practice, because adding a `NOVAL` constant would be making the model more complex. Except unbounded CHOOSE is not checkable by TLC! While `NoVal` is nice for abstract specifications, it breaks things in the 99% of cases where you're actually using TLA+. You definitely should write `NoVal == CHOOSE v : v \notin Val` in your spec (as that clarifies the intent) and override it as a "model value" (i.e., a constant) in TLC. This is best practice. Even `∃ x ∈ Nat` is not checkable by TLC, yet best practice is to leave it like that (as that is the intent), and override `Nat` in TLC. In either case, the more general specification is verifiable in TLAPS. > Example models. Optimization your model checking. The stuff that might get people to start using TLA+ and _keep_ using it. This kind of discussion is very common on the mailing list (there are a lot of hidden gems there), but I would be very happy to see more people write "pro tips" and publishing them. > Again, none of these are criticisms of your work or your writing. I just wanted to openly say that if your goal is to get people interested in the theory of TLA+, it's great, but if it is to get people interested in use of it, a lack of good theoretical introductions isn't the main barrier. My personal goal in this particular series is just to get people interested in the theory. But TLA+ is still extremely young when it comes to "use in the wild". It was virtually nonexistent before 2012, and started slowly gaining traction only around 2014, when Amazon published their report. As you can see, writing short and to the point tips, tricks and guides isn't exactly my forté, but they are extremely important. As this tiny community grows, there will hopefully be those that will fill in the missing gaps. Your own tutorial is a great start.