5 ms·

>Carbon wants to ship a finished working Carbon language, then bolt on safety (somehow) but, only for some things, not data races for example, so, you still don

>Carbon wants to ship a finished working Carbon language, then bolt on safety (somehow) but, only for some things, not data races for example, so, you still don't actually have Rust's Memory Safety I'm not sure this is correct. As I understand it, Carbon's plan is to add a borrow checker like Rust's. From a recent talk[0][1] by one of the lead developers: >Best candidate for C++ is likely similar to Rust’s borrow checker [0] slides: https://chandlerc.blog/slides/2023-cppnow-carbon-strategy/index.html#/105 https://chandlerc.blog/slides/2023-cppnow-carbon-strategy/in... [1] relevant timestamps: https://youtube.com/watch?v=1ZTJ9omXOQ0&t=1h31m34s https://youtube.com/watch?v=1ZTJ9omXOQ0&t=1h31m34s https://youtube.com/watch?v=1ZTJ9omXOQ0&t=1h9m49s https://youtube.com/watch?v=1ZTJ9omXOQ0&t=1h9m49s

tialaramex 2y ago
Chandler has explicitly said that he doesn't see a reason to solve data races. The borrow checker isn't enough on its own to solve this in Rust, Sean explains (probably deeper in Circle's documentation) that you need to track a new property of types which is infectious, Rust does this with the Send and Sync traits.
- Vt71fcAqt7 2y ago
  You're right. In fact it was in the previous slide[0] from that same talk. Thanks for pointing that out. [0] https://youtube.com/watch?v=1ZTJ9omXOQ0?t=1h8m19s https://youtube.com/watch?v=1ZTJ9omXOQ0?t=1h8m19s
- chandlerc1024 2y ago
  "Chandler has explicitly said that he doesn't see a reason to solve data races." Er, the slide title says that solving this is highly desirable, just not a strict requirement for security purposes. Not sure how that's the same as "doesn't see a reason to solve data races". I see lots of reasons. I just think it is possible to achieve the security goals without it. FWIW, I'm hopeful we'll end up including this in whatever model we end up with for Safe Carbon. It's just a degree of freedom we also shouldn't ignore when designing it.
  - Vt71fcAqt7 2y ago
    Thanks for clarifying that point. It's worth pointing out that the safety strategy doc[0] mentions that >A key subset of safety categories Carbon should address are: >[...] >Data race safety protects against racing memory access: when a thread accesses (read or write) a memory location concurrently with a different writing thread and without synchronizing But then later in the doc it says >It's possible to modify the Rust model several ways in order to reduce the burden on C++ developers: >Don't offer safety guarantees for data races, eliminating RefCell. >[...] >Overall, Carbon is making a compromise around safety in order to give a path for C++ to evolve. [...] One could read this as saying that guaranteed safety against data races is not a goal. Perhaps this doc could be reworded? Maybe something like "Carbon does not see guaranteed safety against data races as strictly necessary to achieve its security goals but we still currently aim for a model that will prevent them." [0] https://github.com/carbon-language/carbon-lang/blob/trunk/docs/project/principles/safety_strategy.md https://github.com/carbon-language/carbon-lang/blob/trunk/do...
  - nextaccountic 2y ago
    > Not sure how that's the same as "doesn't see a reason to solve data races". I see lots of reasons. I just think it is possible to achieve the security goals without it. If Carbon doesn't prevent data races, then how exactly will it achieve memory safety? Will it implement something like OCaml's "Bounding Data Races in Space and Time"? [0] If we ignore compiler optimizations, the problem with data races is that it may make you observe tearing (incomplete writes) and thus it's almost impossible to maintain safety invariants with them. But the job of a safe low level language is to give tools for the programmer to guarantee correctness of the unsafe parts. In the presence of data races, this is infeasible. So even if you find a way to ensure that data races aren't technically UB, data races happening in a low level language surely lead to UB elsewhere. Ultimately this may end up showing as CVEs related to memory safety so I don't think you can achieve your security goals without preventing data races. [0] https://kcsrk.info/papers/pldi18-memory.pdf https://kcsrk.info/papers/pldi18-memory.pdf
    - xmcqdpt2 2y ago
      It is possible to have a memory model that blocks word tearing without full logical data race prevention. Java does it, although it benefits from not having to deal with packed types etc.

tialaramex 2y ago

Chandler has explicitly said that he doesn't see a reason to solve data races. The borrow checker isn't enough on its own to solve this in Rust, Sean explains (probably deeper in Circle's documentation) that you need to track a new property of types which is infectious, Rust does this with the Send and Sync traits.

Vt71fcAqt7 2y ago
You're right. In fact it was in the previous slide[0] from that same talk. Thanks for pointing that out. [0] https://youtube.com/watch?v=1ZTJ9omXOQ0?t=1h8m19s https://youtube.com/watch?v=1ZTJ9omXOQ0?t=1h8m19s
chandlerc1024 2y ago
"Chandler has explicitly said that he doesn't see a reason to solve data races." Er, the slide title says that solving this is highly desirable, just not a strict requirement for security purposes. Not sure how that's the same as "doesn't see a reason to solve data races". I see lots of reasons. I just think it is possible to achieve the security goals without it. FWIW, I'm hopeful we'll end up including this in whatever model we end up with for Safe Carbon. It's just a degree of freedom we also shouldn't ignore when designing it.
- Vt71fcAqt7 2y ago
  Thanks for clarifying that point. It's worth pointing out that the safety strategy doc[0] mentions that >A key subset of safety categories Carbon should address are: >[...] >Data race safety protects against racing memory access: when a thread accesses (read or write) a memory location concurrently with a different writing thread and without synchronizing But then later in the doc it says >It's possible to modify the Rust model several ways in order to reduce the burden on C++ developers: >Don't offer safety guarantees for data races, eliminating RefCell. >[...] >Overall, Carbon is making a compromise around safety in order to give a path for C++ to evolve. [...] One could read this as saying that guaranteed safety against data races is not a goal. Perhaps this doc could be reworded? Maybe something like "Carbon does not see guaranteed safety against data races as strictly necessary to achieve its security goals but we still currently aim for a model that will prevent them." [0] https://github.com/carbon-language/carbon-lang/blob/trunk/docs/project/principles/safety_strategy.md https://github.com/carbon-language/carbon-lang/blob/trunk/do...
- nextaccountic 2y ago
  > Not sure how that's the same as "doesn't see a reason to solve data races". I see lots of reasons. I just think it is possible to achieve the security goals without it. If Carbon doesn't prevent data races, then how exactly will it achieve memory safety? Will it implement something like OCaml's "Bounding Data Races in Space and Time"? [0] If we ignore compiler optimizations, the problem with data races is that it may make you observe tearing (incomplete writes) and thus it's almost impossible to maintain safety invariants with them. But the job of a safe low level language is to give tools for the programmer to guarantee correctness of the unsafe parts. In the presence of data races, this is infeasible. So even if you find a way to ensure that data races aren't technically UB, data races happening in a low level language surely lead to UB elsewhere. Ultimately this may end up showing as CVEs related to memory safety so I don't think you can achieve your security goals without preventing data races. [0] https://kcsrk.info/papers/pldi18-memory.pdf https://kcsrk.info/papers/pldi18-memory.pdf
  - xmcqdpt2 2y ago
    It is possible to have a memory model that blocks word tearing without full logical data race prevention. Java does it, although it benefits from not having to deal with packed types etc.