5 ms·

So what would you call the application of the compiler enforcing non-race condition patterns of it's not a "race checker"? It's still there. It's just a compil

So what would you call the application of the compiler enforcing non-race condition patterns of it's not a "race checker"? It's still there. It's just a compile-time "race checker", not runtime.

tsimionescu 7y ago
Not really, in Rust's case. It's the general borrow checker which handles this. Since in Rust it is illegal for a value to be referenced for writing in one place and referenced for anything else in any other place, regardless of concurrency/parallelism, Rust code is data-race free by design. I still think that GP's comment was a non-sequitur.
- zozbot234 7y ago
  Rust has "interior" mutability, meaning that shared references are not true 'read only' references; they can be used for writing if the type supports such an operation. What makes Rust data-race free is the combination of 'interior' mutability and the Send and Sync traits, which control moving or referencing objects across threads.
morelisp 7y ago
Rust's compiler checks a mathematical proof that, if your types are valid (e.g. you didn't do anything bad during `unsafe`) you do not have any data races. It is a guarantee about your program per se. Go's race detection says (with a high probability) you do or do not have any data races in the paths actually taken during some execution of your program. It is a (probabilistic) guarantee about how you ran your program.
- zozbot234 7y ago
  It's not a mathematical proof in the literal sense (yet), because there are known soundness bugs in Rust that are yet to be addressed; moreover the interaction of borrow checking (including interior mutability) with the traits system is poorly understood and has not been proven to be correct even in a simplified model. It should yield a meaningful level of checking, and if nothing else, the ergonomics is way better than just running a static analysis on C/C++ code (setting aside the question of whether current static analysis tools can even check for possible data races); but you shouldn't rely on it to that extent.
  - morelisp 7y ago
    I don't program Rust regularly or track its status in that much detail, so thanks for the correction. Do you have some links about the known soundness issues? I was under the impression that although it hadn't yet been proven it was still a medium-term goal, and any soundness bugs were considered fairly major. (And yeah, "mathematical proof" is strong regardless since e.g. LLVM is also in there somewhere. But it captures the idea more closely than any comparison of "compile vs. runtime" or "static vs. dynamic" does.)
    - steveklabnik 7y ago
      https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Aopen+label%3A%22I-unsound+%F0%9F%92%A5%22 https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Ao... is the list of soundness bugs. They are considered major, but they’re more compiler bugs than something broken in the language itself. They are taken seriously, but bugs will always happen. Some need upstream fixes, too, so that can take a while.

So what would you call the application of the compiler enforcing non-race condition patterns of it's not a "race checker"? It's still there. It's just a compile-time "race checker", not runtime.

tsimionescu 7y ago

Not really, in Rust's case. It's the general borrow checker which handles this. Since in Rust it is illegal for a value to be referenced for writing in one place and referenced for anything else in any other place, regardless of concurrency/parallelism, Rust code is data-race free by design. I still think that GP's comment was a non-sequitur.

zozbot234 7y ago
Rust has "interior" mutability, meaning that shared references are not true 'read only' references; they can be used for writing if the type supports such an operation. What makes Rust data-race free is the combination of 'interior' mutability and the Send and Sync traits, which control moving or referencing objects across threads.

morelisp 7y ago

Rust's compiler checks a mathematical proof that, if your types are valid (e.g. you didn't do anything bad during `unsafe`) you do not have any data races. It is a guarantee about your program per se. Go's race detection says (with a high probability) you do or do not have any data races in the paths actually taken during some execution of your program. It is a (probabilistic) guarantee about how you ran your program.

zozbot234 7y ago
It's not a mathematical proof in the literal sense (yet), because there are known soundness bugs in Rust that are yet to be addressed; moreover the interaction of borrow checking (including interior mutability) with the traits system is poorly understood and has not been proven to be correct even in a simplified model. It should yield a meaningful level of checking, and if nothing else, the ergonomics is way better than just running a static analysis on C/C++ code (setting aside the question of whether current static analysis tools can even check for possible data races); but you shouldn't rely on it to that extent.
- morelisp 7y ago
  I don't program Rust regularly or track its status in that much detail, so thanks for the correction. Do you have some links about the known soundness issues? I was under the impression that although it hadn't yet been proven it was still a medium-term goal, and any soundness bugs were considered fairly major. (And yeah, "mathematical proof" is strong regardless since e.g. LLVM is also in there somewhere. But it captures the idea more closely than any comparison of "compile vs. runtime" or "static vs. dynamic" does.)
  - steveklabnik 7y ago
    https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Aopen+label%3A%22I-unsound+%F0%9F%92%A5%22 https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Ao... is the list of soundness bugs. They are considered major, but they’re more compiler bugs than something broken in the language itself. They are taken seriously, but bugs will always happen. Some need upstream fixes, too, so that can take a while.