5 ms·

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

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.
      - kiitos 1y ago
        > 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 You seem to conflate the concepts of "data race" and "race condition", which are not the same thing. Two threads writing to the same memory location without synchronization (without using atomic operations, without going thru a synchronization point like a mutex, etc.) is a data race, and almost certainly also a race condition. If access to that memory location is synchronized, whether thru atomics or otherwise, then there's no data race, but there can still be a race condition. This isn't a pedantic distinction, it's actually pretty important.

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.
    - kiitos 1y ago
      > 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 You seem to conflate the concepts of "data race" and "race condition", which are not the same thing. Two threads writing to the same memory location without synchronization (without using atomic operations, without going thru a synchronization point like a mutex, etc.) is a data race, and almost certainly also a race condition. If access to that memory location is synchronized, whether thru atomics or otherwise, then there's no data race, but there can still be a race condition. This isn't a pedantic distinction, it's actually pretty important.