4 ms·

> TSan is a reliable way of detecting data races in your code, instead of trying to repeatedly run the code in a loop hoping for a data race to occur. I'm sure

> TSan is a reliable way of detecting data races in your code, instead of trying to repeatedly run the code in a loop hoping for a data race to occur. I'm sure this doesn't intend to be misleading but I think it can mislead people anyway. TSan should detect races but just like "repeatedly run the code in a loop" it's not actually checking what you wrote doesn't have races, it's just reporting any which happened during testing. This is valuable - if you eliminate a race you've almost certainly fixed a real bug, maybe a very subtle bug you'd have cursed for years otherwise, but you can't use TSan to prove there are no further bugs of this kind. Tools to prove this stuff are often much harder to bring into a project, but you should put that work in if the difference between "It's probably fine" and "I proved it's correct" sounds necessary to you or for your work. I don't want my pacemaker to be "probably fine" but it's OK if the Youtube music player on my phone wasn't proved correct.

dataflow 1y ago
My (limited) understanding is that the way TSAN works is better than what you're comparing it to. You don't have to rerun TSAN in a loop to finally catch a race. As long as your test has coverage of that scenario (i.e. it executes the lines of interest once within a reasonable time window) it should get caught. Of course, being dynamic, it can't catch code that you never execute during testing, but that's not such a huge problem because you can verify code coverage through other means. It's quite a bit of a different from having to make stars align by looping until some e.g. rare timing issue comes up. The real issue here isn't that TSAN is low-confidence about absence of data races in C++. The issue is that even if it statically proved the absence of data races in the C++ sense, that still wouldn't imply that your algorithm is race-free. Because it's trivial to patch every single instance of a data race by using an atomic to get TSAN to shut up, but that in no way implies the higher-level concurrent algorithm works correctly. (e.g., if two threads perform an atomic load of some variable, then add one, then perform an atomic store back in, they would obviously stomp on each other, but TSAN wouldn't care.) It's more like a UB checker than a correctness verifier.
- withoutboats3 1y ago
  The occurrence of data races depends on the specific non-deterministic sequence of execution of concurrent codepaths. Just because you have 100% code coverage does not mean you've covered every potential execution sequence, and its almost never practical to actually execute every possibility to ensure the absence of data races. Depending on the probability that your data race will occur, it could indeed be something you have to make stars align for TSAN to catch. Not to talk my own book, but there is a well-known alternative to C++ that can actually guarantee the absence of data races.
  - dataflow 1y ago
    It "could" for some algorithms, yes, but for a lot of algorithms, that kind of star alignment simply isn't necessary to find all the data races, was my point. And yes, TLA+ etc. can be helpful, but then you have the problem of matching them up with the code.
    - Maxatar 1y ago
      I feel like in a subtle way you're mixing up data races with race conditions, especially given the example you site about incrementing an atomic variable. TSAN does not check for race conditions in general, and doesn't claim to do so at all as the documentation doesn't include the term race condition anywhere. TSAN is strictly for checking data races and deadlocks. Consequently this claim is false: >The issue is that even if it statically proved the absence of data races in the C++ sense, that still wouldn't imply that your algorithm is race-free. Race-free code means absence of data races, it does not mean absence of the more general race condition. If you search Google Scholar for race free programming you'll find no one uses the term race-free to refer to complete absence of race conditions but rather to the absence of data races.
      - dataflow 1y ago
        There's "data race" in "C++ ISO standard" sense, and then there's "data race" in the general CS literature (as well as all the other terms). Two threads writing a value to the same memory location (even atomically) is usually a data race in the CS/algorithm sense (due to the lack of synchronization), but not the C++ sense. I'm not really interested in pedantic terminology here, just trying get a higher level point across about what you can & can't assume with a clean TSAN (and how not to clean your TSAN errors). Feel free to mentally rewrite my comment with whatever preferred terminology you feel would get my points across.
sebtron 1y ago
TSan also catches data races that end up not having any visible effect, unlike rerunning and hoping to see the program misbehave.
- vlovich123 1y ago
  The false positive on TSAN is so low that it’s worth fixing any false positives although concluding it’s a false positive seems so hard that I always have a nagging feeling as to whether I actually did fix it
  - tialaramex 1y ago
    "Data race which doesn't seem to modify the data" is actually often not a false positive, they're called "Benign data races" and well, go read the literature, it's often difficult to be sure they're truly "benign" and if there's a subtle reason why they aren't that's now a crazy hard to spot bug in your program. So yeah, just fix 'em. Most of them you dodged a bullet, and even when you didn't it will now be easier for the next person to reason about the software.
    - kiitos 1y ago
      Yeah in fact there is no such thing as a benign data race -- https://web.archive.org/web/20181022150257/https://software.intel.com/en-us/blogs/2013/01/06/benign-data-races-what-could-possibly-go-wrong https://web.archive.org/web/20181022150257/https://software....
      - vlovich123 1y ago
        I agree. That doesn’t mean that TSAN doesn’t have false positives even though they may be rare.
        kiitos 1y ago
        Sure, but nobody is gonna rely on TSAN to determine data races in their code :)

dataflow 1y ago

My (limited) understanding is that the way TSAN works is better than what you're comparing it to. You don't have to rerun TSAN in a loop to finally catch a race. As long as your test has coverage of that scenario (i.e. it executes the lines of interest once within a reasonable time window) it should get caught. Of course, being dynamic, it can't catch code that you never execute during testing, but that's not such a huge problem because you can verify code coverage through other means. It's quite a bit of a different from having to make stars align by looping until some e.g. rare timing issue comes up. The real issue here isn't that TSAN is low-confidence about absence of data races in C++. The issue is that even if it statically proved the absence of data races in the C++ sense, that still wouldn't imply that your algorithm is race-free. Because it's trivial to patch every single instance of a data race by using an atomic to get TSAN to shut up, but that in no way implies the higher-level concurrent algorithm works correctly. (e.g., if two threads perform an atomic load of some variable, then add one, then perform an atomic store back in, they would obviously stomp on each other, but TSAN wouldn't care.) It's more like a UB checker than a correctness verifier.

withoutboats3 1y ago
The occurrence of data races depends on the specific non-deterministic sequence of execution of concurrent codepaths. Just because you have 100% code coverage does not mean you've covered every potential execution sequence, and its almost never practical to actually execute every possibility to ensure the absence of data races. Depending on the probability that your data race will occur, it could indeed be something you have to make stars align for TSAN to catch. Not to talk my own book, but there is a well-known alternative to C++ that can actually guarantee the absence of data races.
- dataflow 1y ago
  It "could" for some algorithms, yes, but for a lot of algorithms, that kind of star alignment simply isn't necessary to find all the data races, was my point. And yes, TLA+ etc. can be helpful, but then you have the problem of matching them up with the code.
  - Maxatar 1y ago
    I feel like in a subtle way you're mixing up data races with race conditions, especially given the example you site about incrementing an atomic variable. TSAN does not check for race conditions in general, and doesn't claim to do so at all as the documentation doesn't include the term race condition anywhere. TSAN is strictly for checking data races and deadlocks. Consequently this claim is false: >The issue is that even if it statically proved the absence of data races in the C++ sense, that still wouldn't imply that your algorithm is race-free. Race-free code means absence of data races, it does not mean absence of the more general race condition. If you search Google Scholar for race free programming you'll find no one uses the term race-free to refer to complete absence of race conditions but rather to the absence of data races.
    - dataflow 1y ago
      There's "data race" in "C++ ISO standard" sense, and then there's "data race" in the general CS literature (as well as all the other terms). Two threads writing a value to the same memory location (even atomically) is usually a data race in the CS/algorithm sense (due to the lack of synchronization), but not the C++ sense. I'm not really interested in pedantic terminology here, just trying get a higher level point across about what you can & can't assume with a clean TSAN (and how not to clean your TSAN errors). Feel free to mentally rewrite my comment with whatever preferred terminology you feel would get my points across.

sebtron 1y ago

TSan also catches data races that end up not having any visible effect, unlike rerunning and hoping to see the program misbehave.

vlovich123 1y ago
The false positive on TSAN is so low that it’s worth fixing any false positives although concluding it’s a false positive seems so hard that I always have a nagging feeling as to whether I actually did fix it
- tialaramex 1y ago
  "Data race which doesn't seem to modify the data" is actually often not a false positive, they're called "Benign data races" and well, go read the literature, it's often difficult to be sure they're truly "benign" and if there's a subtle reason why they aren't that's now a crazy hard to spot bug in your program. So yeah, just fix 'em. Most of them you dodged a bullet, and even when you didn't it will now be easier for the next person to reason about the software.
  - kiitos 1y ago
    Yeah in fact there is no such thing as a benign data race -- https://web.archive.org/web/20181022150257/https://software.intel.com/en-us/blogs/2013/01/06/benign-data-races-what-could-possibly-go-wrong https://web.archive.org/web/20181022150257/https://software....
    - vlovich123 1y ago
      I agree. That doesn’t mean that TSAN doesn’t have false positives even though they may be rare.
      - kiitos 1y ago
        Sure, but nobody is gonna rely on TSAN to determine data races in their code :)