7 ms·

Finding Goroutine Bugs with TLA+

125 points by headalgorithm 6y ago

wanghq 6y ago
TLA: It's the thing I wish I know but haven't got a chance to learn.
- jaytaylor 6y ago
  I feel similarly, except it's the thing I wish was _easier_ to learn! <3
  - Jtsummers 6y ago
    Hillel's book is good, as is his online tutorial (https://learntla.com/introduction/ https://learntla.com/introduction/).
  - dwohnitmok 6y ago
    Going through Lamport's video lectures (https://lamport.azurewebsites.net/video/videos.html https://lamport.azurewebsites.net/video/videos.html) is a great way to get the basics down. It proceeds at a fairly lesiurely pace so if you just block off some amount of time every day (say a video or two a day which usually works out to 30min - 1 hour depending on how well you want to practice the concepts in the video) you'll be able to use TLA+ by the end of a week or so.
  - Joker_vD 6y ago
    It's so low-level, every time I try to look into it I am reminded of the 6th normal form, it's such a mess to gather all the parts of the condition into one big conjunction...
- amelius 6y ago
  You'd now be building more robust software, except 100 times slower.
  - pron 6y ago
    TLA+ makes development faster, not slower (once you get a feel for how to use it). I mean, it would be slower if you'd spend time writing mechanically-checked formal proofs, but that's working 10x for just slightly more confidence than you can get with TLC (a model-checker for TLA+) alone, so in almost all cases people just stick to specifying and model-checking.
    - Jtsummers 6y ago
      I was working on something similar to say, stepped away, and saw your post. So I'll add to it: TLA+'s place is as part of your design process (you have one, right?). It's the thing you do before committing any code to the project or radically restructuring an existing project (prototype code fits in the design process, but it shouldn't be considered committed most of the time). By spending a bit of time thinking about the design, and using tools like TLA+ to validate that design, you can save yourself months and years of heartache down the road. By way of anecdote, some colleagues were working on a concurrent algorithm, needing to share data between two embedded processors talking over a databus. A bit more time spent on the design, versus the rather slapdash approach they took, would've saved them 6 months of debugging and tweaking until it worked. The issues were subtle, so it "worked" but wasn't totally correct and tracing the errors they were seeing back to that code was non-obvious (and hard, debugging embedded isn't trivial). It was quite literally a case where skipping a couple weeks of design cost them months later.
      - sagichmal 6y ago
        > TLA+'s place is as part of your design process ... By spending a bit of time thinking about the design, and using tools like TLA+ to validate that design I think you dramatically underestimate the amount of effort required to produce a formal model of any nontrivial system, and overestimate the stability of system definitions in response to changing business requirements.
        ahelwer 6y ago
        Eh. I used TLA+ for a few projects inside Microsoft. It probably takes a couple of weeks to write a spec for a complicated problem. Then less time to implement it, because all the heavy lifting has already been done - in many cases you're directly transcribing the spec logic without having to think very hard. The sort of things for which you write specs are generally "core" functionality that doesn't change very often. If people are constantly mucking around in that area without writing specs, your system will be a pile of crap.
justicezyx 6y ago
The barrier to TLA+ remains the high-cost of rewriting a piece of code in another language. The translation process itself could be error prone. The disintegrated concepts requires considerable amount of mental effort. I am very interested in using the host language (the language that used to write the software one wants to verify) compiler to compile into a TLA+ spec.
- exdsq 6y ago
  I believe the main use case of TLA+ is to first design the code as a spec and then implement it, rather than the other way around.
  - kinmi 6y ago
    I'd like to learn more: how would one go about ensuring the implementation was an accurate implementation of the specification? Is there a process for doing this?
    - thamer 6y ago
      There's no perfect answer and it's always been a limitation to take into account. There are model-checking solutions which take a spec and generate code, but you don't get this with TLA+. In a way, you could make the same argument about writing tests: the code paths you exercise in your CI environment are not quite the same as what's running in prod, and neither is the environment in which the code is running (e.g. the load your process or host is under, the memory pressure, etc). That said, don't let this small gap and the lack of a perfect solution discourage you from using model checking, there is still a lot to gain from adding it as one more tool in your toolbox.
    - Jtsummers 6y ago
      To the best of my knowledge there's no universal, formal method to translate the spec into code and verify the code properly implements the spec. Just like without TLA+, you're left to conduct your own testing and analysis to verify your code is correct, but with TLA+ you at least have a specification to verify it against (even if it's tedious). That said, some languages offer more capabilities and tooling to support this. Check out Frama-C and its Mthread plugin [0] (NB: I have no experience with either) for something that could help. In Ada there's SPARK, but I'm not sure the extent that it helps with verifying concurrency properties. In some languages, like Erlang, Elixir, and Go, the concurrency mechanism is sufficiently well integrated into the languages that it becomes very clear while reading the code what's happening (especially if you properly segment your code into functions and modules to aid in readability). These can make the analysis much easier to perform. And regardless of language, if you have a specification and design the code tends to come out much cleaner, which makes the manual task of reviewing and verifying these critical parts less onerous. Additionally, it's not as hard to conceive of tests when you have the simpler spec to look at versus the much larger code constructed from it. [0] https://frama-c.com/mthread.html https://frama-c.com/mthread.html
pron 6y ago
I think this spec tries to do two things, only one of which fits in with the purpose of TLA+. I think this is caused by some ambiguity regarding the source of the bug: is it due to a difficulty writing a subtle algorithm, or is it due to a difficulty understanding the Go language's semantics. If it's the latter, then TLA+ isn't the right tool, and neither is SPIN. There are other tools for verifying language semantics. If it's the former -- i.e. the author of the spec knows the meaning of each line and its intent -- then TLA+ is a very good tool, but then a simpler spec could suffice, perhaps something like this: https://pron.github.io/files/Channels.pdf https://pron.github.io/files/Channels.pdf
- hwayne 6y ago
  The point was to do demonstrate the bug while staying close to the Go example. You can find the bug at a higher level, but then there's the objection that you're not finding the bug in the Go code, you're finding the bug in simpler toy code. That raises the further objection that we only find the bug because we were looking for it, which is why I showed we find the bug even if we do a straightforward translation of the code.
  - pron 6y ago
    I understand, but I think this strikes at the core of our pedagogical differences regarding TLA+ -- after all, TLA+ is super-Turing-complete, and even TLC can check a subset of TLA+ that is still effectively Turing-completish. Of course you can specify at any level in TLA+, and people have even written compilers from C and Java to TLA+. But doing so suffers from the same scalability problems that all code-level verification techniques suffer from. The question we're asking is how best to get people to use TLA+. Do you show them what model-checking can do and then show that TLA+ can model virtually anything and TLC can check many things, and do so at the code-level because that is something they already know from programming -- but then they ask, as they do in this discussion, why you need TLA+ at all if all you're doing is translating Go to some other language -- or do you first try to show them the TLA+'s real strength, which is mathematical modelling of systems, but that is a new concept that is different from programming and can be foreign to them? It's a hard problem, and maybe the right approach is to do both, which is what you're doing if we take this post together with others you've written. But I think it's worth mentioning that in this case, this is not the spec someone who knows both TLA+ and Go well would likely write. BTW, I'm trying to remember which of those two features sold me on TLA+, and I think it was the combination of both. I knew the limitations of model-checkers (and had worked with NASA's Java model-checker before) that I knew that a model-checker alone wouldn't give me what I need for the complex distributed system I was working on, and mathematical modelling alone of something so subtle wouldn't have sufficed either without some help checking (cheaply!) if my ideas were right or wrong. So neither aspect would have sold me in isolation, I think.
jeffbee 6y ago
This program finds the problem not because TLA+ is nifty, but because it sweeps out the parameter space, which is exactly what the original Go program should have done in a unit test. What happens when `len(pss)` is just below, at, or just above, or way above `concurrencyProcesses`? That is the type of question that unit tests are supposed to address. Go has a perfectly good deadlock detector. The real problem cannot be solved by re-modelling in a different high-level language, because the real problem with that code is it gets `pss` from a library call and `concurrencyProcesses` from a global variable, when they should both be function parameters a test case can exercise.
- guessmyname 6y ago
  This is why I invest more time Fuzzing [1] than writing software models or formal specifications. Google’s gofuzz [2] and dvyukov’s go-fuzz [3] libraries have been instrumental for my success every time I embark on a journey to write a complex system with concurrency in its heart. The list of bugs I have found in my co-workers programs was so big we decided to spend a month configuring the fuzzing tests and our continuous integration environment to do it automatically. Code quality increased by an order of magnitude and we are now more confident about the code we ship to production. [1] https://en.wikipedia.org/wiki/Fuzzing https://en.wikipedia.org/wiki/Fuzzing [2] https://github.com/google/gofuzz https://github.com/google/gofuzz [3] https://github.com/dvyukov/go-fuzz https://github.com/dvyukov/go-fuzz
- justsomeuser 6y ago
  Once you have enough variables you would not be able to write enough unit tests to ensure every safety property of your design. TLA is math, not a typical programming language.
bsaul 6y ago
the conversation in this thread completely changed my view of formal verification tools. I used to think of them as "code" verifier. I know realize they're actually "whiteboard drawings" verifiers. Which makes it much more usable right away. I believe my mistake was due to the fact that most articles on the subject start by showing you a faulty piece of code.
- SubjectToChange 6y ago
  The field of formal methods covers both code correctness and higher level proofs.

125 points by headalgorithm 6y ago

wanghq 6y ago

TLA: It's the thing I wish I know but haven't got a chance to learn.

jaytaylor 6y ago
I feel similarly, except it's the thing I wish was _easier_ to learn! <3
- Jtsummers 6y ago
  Hillel's book is good, as is his online tutorial (https://learntla.com/introduction/ https://learntla.com/introduction/).
- dwohnitmok 6y ago
  Going through Lamport's video lectures (https://lamport.azurewebsites.net/video/videos.html https://lamport.azurewebsites.net/video/videos.html) is a great way to get the basics down. It proceeds at a fairly lesiurely pace so if you just block off some amount of time every day (say a video or two a day which usually works out to 30min - 1 hour depending on how well you want to practice the concepts in the video) you'll be able to use TLA+ by the end of a week or so.
- Joker_vD 6y ago
  It's so low-level, every time I try to look into it I am reminded of the 6th normal form, it's such a mess to gather all the parts of the condition into one big conjunction...
amelius 6y ago
You'd now be building more robust software, except 100 times slower.
- pron 6y ago
  TLA+ makes development faster, not slower (once you get a feel for how to use it). I mean, it would be slower if you'd spend time writing mechanically-checked formal proofs, but that's working 10x for just slightly more confidence than you can get with TLC (a model-checker for TLA+) alone, so in almost all cases people just stick to specifying and model-checking.
  - Jtsummers 6y ago
    I was working on something similar to say, stepped away, and saw your post. So I'll add to it: TLA+'s place is as part of your design process (you have one, right?). It's the thing you do before committing any code to the project or radically restructuring an existing project (prototype code fits in the design process, but it shouldn't be considered committed most of the time). By spending a bit of time thinking about the design, and using tools like TLA+ to validate that design, you can save yourself months and years of heartache down the road. By way of anecdote, some colleagues were working on a concurrent algorithm, needing to share data between two embedded processors talking over a databus. A bit more time spent on the design, versus the rather slapdash approach they took, would've saved them 6 months of debugging and tweaking until it worked. The issues were subtle, so it "worked" but wasn't totally correct and tracing the errors they were seeing back to that code was non-obvious (and hard, debugging embedded isn't trivial). It was quite literally a case where skipping a couple weeks of design cost them months later.
    - sagichmal 6y ago
      > TLA+'s place is as part of your design process ... By spending a bit of time thinking about the design, and using tools like TLA+ to validate that design I think you dramatically underestimate the amount of effort required to produce a formal model of any nontrivial system, and overestimate the stability of system definitions in response to changing business requirements.
      - ahelwer 6y ago
        Eh. I used TLA+ for a few projects inside Microsoft. It probably takes a couple of weeks to write a spec for a complicated problem. Then less time to implement it, because all the heavy lifting has already been done - in many cases you're directly transcribing the spec logic without having to think very hard. The sort of things for which you write specs are generally "core" functionality that doesn't change very often. If people are constantly mucking around in that area without writing specs, your system will be a pile of crap.

justicezyx 6y ago

The barrier to TLA+ remains the high-cost of rewriting a piece of code in another language. The translation process itself could be error prone. The disintegrated concepts requires considerable amount of mental effort. I am very interested in using the host language (the language that used to write the software one wants to verify) compiler to compile into a TLA+ spec.

exdsq 6y ago
I believe the main use case of TLA+ is to first design the code as a spec and then implement it, rather than the other way around.
- kinmi 6y ago
  I'd like to learn more: how would one go about ensuring the implementation was an accurate implementation of the specification? Is there a process for doing this?
  - thamer 6y ago
    There's no perfect answer and it's always been a limitation to take into account. There are model-checking solutions which take a spec and generate code, but you don't get this with TLA+. In a way, you could make the same argument about writing tests: the code paths you exercise in your CI environment are not quite the same as what's running in prod, and neither is the environment in which the code is running (e.g. the load your process or host is under, the memory pressure, etc). That said, don't let this small gap and the lack of a perfect solution discourage you from using model checking, there is still a lot to gain from adding it as one more tool in your toolbox.
  - Jtsummers 6y ago
    To the best of my knowledge there's no universal, formal method to translate the spec into code and verify the code properly implements the spec. Just like without TLA+, you're left to conduct your own testing and analysis to verify your code is correct, but with TLA+ you at least have a specification to verify it against (even if it's tedious). That said, some languages offer more capabilities and tooling to support this. Check out Frama-C and its Mthread plugin [0] (NB: I have no experience with either) for something that could help. In Ada there's SPARK, but I'm not sure the extent that it helps with verifying concurrency properties. In some languages, like Erlang, Elixir, and Go, the concurrency mechanism is sufficiently well integrated into the languages that it becomes very clear while reading the code what's happening (especially if you properly segment your code into functions and modules to aid in readability). These can make the analysis much easier to perform. And regardless of language, if you have a specification and design the code tends to come out much cleaner, which makes the manual task of reviewing and verifying these critical parts less onerous. Additionally, it's not as hard to conceive of tests when you have the simpler spec to look at versus the much larger code constructed from it. [0] https://frama-c.com/mthread.html https://frama-c.com/mthread.html

pron 6y ago

I think this spec tries to do two things, only one of which fits in with the purpose of TLA+. I think this is caused by some ambiguity regarding the source of the bug: is it due to a difficulty writing a subtle algorithm, or is it due to a difficulty understanding the Go language's semantics. If it's the latter, then TLA+ isn't the right tool, and neither is SPIN. There are other tools for verifying language semantics. If it's the former -- i.e. the author of the spec knows the meaning of each line and its intent -- then TLA+ is a very good tool, but then a simpler spec could suffice, perhaps something like this: https://pron.github.io/files/Channels.pdf https://pron.github.io/files/Channels.pdf

hwayne 6y ago
The point was to do demonstrate the bug while staying close to the Go example. You can find the bug at a higher level, but then there's the objection that you're not finding the bug in the Go code, you're finding the bug in simpler toy code. That raises the further objection that we only find the bug because we were looking for it, which is why I showed we find the bug even if we do a straightforward translation of the code.
- pron 6y ago
  I understand, but I think this strikes at the core of our pedagogical differences regarding TLA+ -- after all, TLA+ is super-Turing-complete, and even TLC can check a subset of TLA+ that is still effectively Turing-completish. Of course you can specify at any level in TLA+, and people have even written compilers from C and Java to TLA+. But doing so suffers from the same scalability problems that all code-level verification techniques suffer from. The question we're asking is how best to get people to use TLA+. Do you show them what model-checking can do and then show that TLA+ can model virtually anything and TLC can check many things, and do so at the code-level because that is something they already know from programming -- but then they ask, as they do in this discussion, why you need TLA+ at all if all you're doing is translating Go to some other language -- or do you first try to show them the TLA+'s real strength, which is mathematical modelling of systems, but that is a new concept that is different from programming and can be foreign to them? It's a hard problem, and maybe the right approach is to do both, which is what you're doing if we take this post together with others you've written. But I think it's worth mentioning that in this case, this is not the spec someone who knows both TLA+ and Go well would likely write. BTW, I'm trying to remember which of those two features sold me on TLA+, and I think it was the combination of both. I knew the limitations of model-checkers (and had worked with NASA's Java model-checker before) that I knew that a model-checker alone wouldn't give me what I need for the complex distributed system I was working on, and mathematical modelling alone of something so subtle wouldn't have sufficed either without some help checking (cheaply!) if my ideas were right or wrong. So neither aspect would have sold me in isolation, I think.

jeffbee 6y ago

This program finds the problem not because TLA+ is nifty, but because it sweeps out the parameter space, which is exactly what the original Go program should have done in a unit test. What happens when `len(pss)` is just below, at, or just above, or way above `concurrencyProcesses`? That is the type of question that unit tests are supposed to address. Go has a perfectly good deadlock detector. The real problem cannot be solved by re-modelling in a different high-level language, because the real problem with that code is it gets `pss` from a library call and `concurrencyProcesses` from a global variable, when they should both be function parameters a test case can exercise.

guessmyname 6y ago
This is why I invest more time Fuzzing [1] than writing software models or formal specifications. Google’s gofuzz [2] and dvyukov’s go-fuzz [3] libraries have been instrumental for my success every time I embark on a journey to write a complex system with concurrency in its heart. The list of bugs I have found in my co-workers programs was so big we decided to spend a month configuring the fuzzing tests and our continuous integration environment to do it automatically. Code quality increased by an order of magnitude and we are now more confident about the code we ship to production. [1] https://en.wikipedia.org/wiki/Fuzzing https://en.wikipedia.org/wiki/Fuzzing [2] https://github.com/google/gofuzz https://github.com/google/gofuzz [3] https://github.com/dvyukov/go-fuzz https://github.com/dvyukov/go-fuzz
justsomeuser 6y ago
Once you have enough variables you would not be able to write enough unit tests to ensure every safety property of your design. TLA is math, not a typical programming language.

bsaul 6y ago

the conversation in this thread completely changed my view of formal verification tools. I used to think of them as "code" verifier. I know realize they're actually "whiteboard drawings" verifiers. Which makes it much more usable right away. I believe my mistake was due to the fact that most articles on the subject start by showing you a faulty piece of code.

SubjectToChange 6y ago
The field of formal methods covers both code correctness and higher level proofs.