[chandlerc1024]

"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.

[nextaccountic]

> 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

[xmcqdpt2]

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.

[Vt71fcAqt7]

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/do...