Data races in Rust

The Rustomicon says:

Data races are mostly prevented through Rust's ownership system: it's impossible to alias a mutable reference, so it's impossible to perform a data race.

I did not think any deep about this, since it just says mostly, so is there any case (unsafe doesn't count) in which a Rust code contains data race?

There’s always the possbility of a data race if you try to roll your own check-and-set operation. This particularly shows up when dealing with data outside the process, like in SQL databases or network services.

Yes, I may imagine this situation: two processes (each written in safe Rust) communicate with a SQL database.

But I wonder about a more strict context where there are only safe Rust codes, and the data race happens inside them. More specific: two thread written in safe Rust, and communicate between using a shared memory.

This can easily be seen as a race condition, but can this really be a data race (i.e. two commands using simultaneously the same place in memory, not just "in unspecified order")?


You’re right, it’s a really fine distinction that I’m not used to making: They’re both the same class of error, but with different severity: Simultaneous access is compiler-UB, and could therefore have any result. The possible resuls of the race I described, on the other hand, are at least enumerable.

I'm not sure why it says mostly. It might be because there are some situations where the thing preventing it isn't the ownership system, but something else?


Have the ownership semantics been formally proven to prevent races yet, or is this a case of nobody having found a hole in it yet? The wording may be meant as a hedge against currently-unknown flaws in the protections: Professional judgement plus practical experience is strong evidence, but it can’t provide certainty.

(As I recall, stacked borrows is primarily concerned with unsafe rust, which can bypass most ownership semantics)

I think this paper gives a proof of the general safety of the language + some of the standard library.
Haven't read it though :sweat_smile:


@arnaudgolfouse Thank you. I've just skimmed the paper, and found that:

We have shown in Coq that if a program has a data race, then it has an execution where these checks fail. As a consequence, if we prove that a program cannot get stuck (which implies that the checks always succeed, in all executions), then the program is data-race free.

That means, any program written in \lambda_Rust (i.e. formal model of Rust) is impossible to have data-race.


It's exactly this, ownership is just one component for data-race-freedom, the other components are the Send/Sync traits, which specify which types can be sent across thread boundaries.

Edit: the nomicon says this in the very next sentence :slight_smile:

Interior mutability makes this more complicated, which is largely why we have the Send and Sync traits (see below).


You need to consider the whole paragprah, for context:

A data race has Undefined Behavior, and is therefore impossible to perform in Safe Rust.

The Nomicon is clear: data races are not possible in Safe Rust.

Then it goes on to explain which features of Rust prevent data races and identifies 2 features:

Data races are mostly prevented through Rust's ownership system: it's impossible to alias a mutable reference, so it's impossible to perform a data race.

Data races in Safe Rust are mostly prevented through Ownership/Borrowing: a data race occurs when 2 threads look at the same piece of data simultaneously, and at least one of them writes to it.

The Ownership/Borrowing system generally prevents that, but there's one exception: Interior mutability.

Interior mutability makes this more complicated, which is largely why we have the Send and Sync traits (see below).

To plug the last hole (interior mutability), the Send and Sync traits are used.


My default assumption is that if any program I write ends up with a race condition in the Rust world, as it were, then that is a bug in the Rust compiler or some as yet unfound hole in the Rust memory model that will get fixed.

So far I don't hear of anyone finding such a bug/hole and the above posts indicate that it has been formally proved impossible (Modulo compiler bugs I guess).

What you are describing, SQL database or whatever external service, is something totally different. Outside of the Rust language world. For example I could have two threads in a Rust program that connect to a smart light bulb. One says turn ON, the other says turn OFF. Which one wins?

I'm know little of databases but isn't that what "transactions" are all about?

Sure, but transactions have downsides, especially long-running ones. The same goes for some of the coordination primitives provided by Rust, like Mutexes. My point was really that, though Rust prevents UB-causing race conditions, they can happen at a higher level of abstraction which the compiler can’t do anything about.

The classic example of this sort of race condition occurs in multi-user systems. If you’re presenting information to a human to be acted on, it’s usually a bad idea to hold open a lock while you wait for their response. In that case, there’s two transactions/lock acquisitions: one to fetch the initial information and another to act on the response that came back. Between those, another user could access and change the information the first is also working on.

Rust’s guarantees about how things behave while the lock is held makes it possible to handle this gracefully. That happens in the domain of program logic, though, where the compiler can’t help. A bug there still can cause the sort of hard-to-replicate fault that makes the root cause incredibly hard to track down.

Yes indeed.

As far as I can tell the Rust guarantees about memory use only encompass Rust's domain. That is, the source code you are writing.

Of course you can write all kind of programs that interact badly with external systems, be they databases, remote processes, machines or humans.

I would not expect Rust to do any more.

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.