Fearless Concurrency: The Same Rule, Applied Across Threads

A data race has a precise definition, given in the lesson Threads and Shared State: two accesses to the same memory location, from different threads, at least one a write, with no ordering between them.

Read that against the previous lesson. Multiple accesses to one location is aliasing. At least one write is mutation. A data race is aliasing plus mutation, which is exactly the intersection the borrow checker forbids.

So the guarantee falls out. Rust did not add thread-safety analysis on top of the borrow checker; the borrow checker was already prohibiting the condition that makes data races possible, and extending it across threads is a matter of bookkeeping rather than new machinery.

That is the substance behind the phrase fearless concurrency. It is not a claim that concurrent programming becomes easy. It is the narrower claim that one specific and vicious class of bug, the kind that appears once a week under load and cannot be reproduced, is rejected at compile time.

The remaining difficulties are undiminished, and the last step of this lesson is about them.

Extending the rule across threads needs two facts about each type, and Rust encodes them as traits with no methods.

Send means a value of this type can be moved to another thread. Most types are Send. A type holding a non-atomic reference count is not, because two threads incrementing it without synchronisation is itself a race.

Sync means a value can be shared by reference across threads: T is Sync exactly when &T is Send. A type with interior mutability that is not synchronised is not Sync, because two threads holding shared references could both mutate.

The important property is that both are automatically derived. A struct is Send if all its fields are Send, and Sync if all its fields are Sync. Nobody annotates ordinary types; the traits propagate through composition.

That is what makes the system usable at scale. Thread safety is a structural property computed from a type's contents, not a claim a library author makes in documentation and a user has to trust.

The spawning function then simply requires them, and the whole check is that one bound.

The mechanism is visible in what fails to compile.

use std::rc::Rc;
use std::thread;

let counter = Rc::new(0);            // non-atomic reference count
let c = Rc::clone(&counter);

thread::spawn(move || {              // rejected at compile time
    println!("{c}");
});
// error: `Rc<i32>` cannot be sent between threads safely

Rc is a reference-counted pointer whose count is a plain integer, incremented and decremented without synchronisation. Sending one to another thread would let two threads update that count concurrently, corrupting it and causing a double free or a leak.

The fix is the atomic version, and the type system directs you to it:

use std::sync::Arc;
let counter = Arc::new(0);           // atomic reference count: Send + Sync

What is worth noticing is the failure mode. In a language without these traits, the same program compiles, runs correctly in testing, and corrupts its refcount occasionally under load. Here it is a compile error naming the exact type and the exact reason, before the program has ever run.

Sharing something mutable across threads needs the borrow rule satisfied at runtime rather than at compile time, and the standard combination does exactly that.

use std::sync::{Arc, Mutex};
use std::thread;

let total = Arc::new(Mutex::new(0));
let mut handles = vec![];

for _ in 0..8 {
    let total = Arc::clone(&total);
    handles.push(thread::spawn(move || {
        let mut guard = total.lock().unwrap();   // exclusive access
        *guard += 1;
    }));                                          // guard drops: unlocked
}
for h in handles { h.join().unwrap(); }
assert_eq!(*total.lock().unwrap(), 8);

Arc provides shared ownership so several threads can hold the value. Mutex provides exclusive access so only one mutates at a time. Together they satisfy the rule dynamically.

Two details are the point. The data is inside the mutex rather than beside it, so there is no way to reach it without locking. Forgetting to take the lock is not an error you can make, because the data is unreachable without the guard.

And the guard is a value whose drop releases the lock, per the ownership lesson. Forgetting to unlock is likewise not expressible.

The same rule is enforced at three different points, and the choice is an engineering decision rather than a correctness one.

Compile-time checking is free and rejects some correct programs. Runtime checking accepts more programs and costs a check plus the possibility of a panic. Locking accepts still more and costs blocking.

The right-hand branch is the one worth dwelling on. A channel moves ownership from one thread to another, so at no point do two threads own the same value. The borrow rule is satisfied trivially, because there is nothing shared to reason about.

That is why message passing is often the better answer, and Rust's ownership model makes the transfer explicit rather than conventional: sending a value moves it, so using it after sending is a compile error rather than a subtle bug.

The general instruction: prefer transferring ownership to sharing it, and reach for a mutex only when the data genuinely must be shared.

The guarantee is precise and narrower than the marketing, and being clear about the gap matters more than the guarantee itself.

Deadlocks are not prevented. Two threads acquiring two mutexes in opposite orders will deadlock, and it compiles. No aliasing rule is violated: each thread holds exclusive access to what it has, and waits forever for the other. Lock ordering discipline is still on you.

Race conditions in the general sense are not prevented. A data race is a memory-level phenomenon. A logical race, where the program's outcome depends on scheduling, is a design property. Check-then-act across two separate lock acquisitions is racy and perfectly legal.

Livelock and starvation are not prevented. Threads can make no progress while violating nothing.

Correctness is not implied. A program can be free of data races and still compute the wrong answer.

The distinction to hold: Rust eliminates data races, the memory-level ones that produce corruption and non-determinism. It does not eliminate race conditions, the design-level ones. The two are routinely conflated, and only the first is what the type system addresses.

There is a reason to believe the guarantee beyond the argument in this lesson, and it connects directly to the formal verification path.

The type system's soundness is not obvious, because the standard library is full of types implemented with unsafe code: Arc, Mutex, Vec and the rest all do things the borrow checker cannot verify. If any of them is wrong, safe code can be made to misbehave, and the guarantee collapses.

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers and Derek Dreyer addressed this in "RustBelt: Securing the Foundations of the Rust Programming Language", POPL 2018. It gives the first formal, machine-checked safety proof for a realistic subset of Rust, built as a semantic model via a logical relation.

The design that makes it tractable is extensibility. Rather than proving the whole standard library at once, the framework states verification conditions a library using unsafe features must satisfy to count as a safe extension. Each library is then discharged separately.

One detail is worth knowing: the work uncovered a previously unknown soundness bug in Rust itself. That is the strongest possible argument for doing the proof, and a good illustration of the verification cursus's point that a proof's value is often what it finds rather than what it confirms.

The split down the middle of that table is the honest summary. Everything the type system can see is prevented; everything requiring a global argument about program behaviour is not.

That maps precisely onto the boundary the lesson What Undecidability Costs Real Tools draws. Deadlock freedom is a semantic property of a whole program, and Rice's theorem puts it out of reach of any type checker. Data race freedom was made checkable by choosing a sufficient syntactic condition, aliasing XOR mutability, that a compiler can verify locally.

That is the transferable idea, and it is worth more than the language: find a local, checkable condition that implies the global property you want, and accept that it will reject some programs that were fine.