Rust

Derived Data Choices

Rust’s memory model is a set of choices on the SPACE / TIME / IDENTITY triangle.

Core strategy: prove coherence at compile time.

---

The Two Projections

Each axis exists in two forms:

Axis	Compile-time	Runtime
SPACE	Types, layouts	Bytes in memory
TIME	CFG regions	Execution sequence
IDENTITY	Names	Addresses

The borrow checker works in compile-time projection. It tracks paths like x and x.field (not runtime addresses), analyzes control flow regions (not actual execution), and reasons about types (not bytes). It proves coherence in this abstract model.

Zero-Cost Abstraction

Rust claims “zero-cost abstractions” — safety checks that don’t add runtime overhead.

For the borrow checker, this means:

• Analysis happens at compile time
• Names and regions are erased before execution
• At runtime: just addresses, just execution, no tracking

The cost is compile time and programmer effort. The runtime pays nothing.

---

Vocabulary

Rust’s terminology conflates projections. Before we use these terms, here’s what they mean in the framework.

The Key Translations

Rust says	Suggests	Actually means
&T	“reference”	shared IDENTITY, frozen TIME
&mut T	“mutable reference”	exclusive IDENTITY, TIME flows
“lifetime”	runtime duration	compile-time TIME region
“borrow”	lending	creating IDENTITY relationship
“move”	relocating data	transferring IDENTITY
“borrow checker”	rule checker	coherence prover

The &mut Misconception

&mut T is not about mutation. It’s about exclusive IDENTITY.

The exclusivity is what allows mutation safely. If you’re the only one with access, you can change things without conflict.

&T is not about immutability. It’s about shared IDENTITY. Sharing requires frozen TIME to stay coherent.

Reading Rust with the Framework

When you see	Think
&x	shared IDENTITY to x’s SPACE
&mut x	exclusive IDENTITY to x’s SPACE
'a	compile-time TIME region
let y = x	IDENTITY transfer (if not Copy)
x.clone()	SPACE duplication
drop(x)	SPACE freed at TIME boundary

---

The Coherence Problem

Two paths to the same SPACE. One writes, one reads. The reader sees partial state. This is incoherence.

Sharing freezes. Mutation isolates.

Either:

• Shared IDENTITY → many can access → TIME must freeze (no mutation)
• Exclusive IDENTITY → one can access → TIME can flow (mutation ok)

How Rust Enforces This

The borrow checker analyzes your code at compile time:

1. Tracks names — which variables alias which SPACE
2. Builds a graph — possible execution paths (the CFG)
3. Computes regions — when each reference is live
4. Checks for conflicts — shared + mutation overlapping?

let mut x = 5;
let r = &x;        // shared IDENTITY starts
println!("{}", r); // shared IDENTITY used, then ends
let m = &mut x;    // exclusive starts — OK, no overlap

The borrow checker sees: shared region ends before exclusive begins. No conflict.

let mut x = 5;
let r = &x;        // shared IDENTITY starts
let m = &mut x;    // exclusive starts — ERROR
println!("{}", r); // shared still live here

The borrow checker sees: shared and exclusive regions overlap. Conflict. Rejected.

SPACE Granularity

The borrow checker tracks IDENTITY at a certain granularity:

Path type	Can prove disjoint?	Why
p.x vs p.y	Yes	Struct fields known at compile time
v[0] vs v[1]	No	Indices are runtime values

let mut p = Point { x: 1, y: 2 };
let rx = &mut p.x;
let ry = &mut p.y;  // OK: different fields

let mut v = vec![1, 2, 3];
let r = &mut v[0];
let s = &mut v[1];  // ERROR: both "borrow v"

The checker sees both as “borrow of v” — it can’t prove v[0] ≠ v[1]. More on this in Borrow Checker Internals.

Zero Cost

All analysis happens at compile time. Names are erased. At runtime: just addresses and execution. No tracking, no checks, no overhead.

---

Bindings

Construct	SPACE	TIME	IDENTITY
const	Inlined	Compile	Compile only
static	Data segment	Compile init	Both
static mut	Data segment	Runtime	Both (unsafe)
let	Stack	Runtime	Both
let mut	Stack	Runtime	Both

const — Purely compile-time. No runtime IDENTITY exists. Each use is inlined. Taking &CONST may yield different addresses—there is no single location.

const X: u32 = 5;
let a = &X;
let b = &X;
// a and b may have different addresses

static — Bridges projections. Initialized at compile-time, lives in data segment at runtime. Has a stable address.

static mut — Runtime mutation of global IDENTITY. The borrow checker can’t prove safety across the whole program. Every access requires unsafe.

let / let mut — Runtime evaluation, stack SPACE. mut allows rebinding the name, not mutation through it.

---

References

References are how you create IDENTITY to existing SPACE.

Reference	IDENTITY	TIME	Rule
&T	Shared	Frozen	Many allowed
&mut T	Exclusive	Flows	One allowed

This is the coherence rule applied:

&T — Shared IDENTITY:

let x = vec![1, 2, 3];
let r1 = &x;
let r2 = &x;  // OK: multiple shared

Many paths to same SPACE. TIME frozen—no mutation through any path. No conflict possible.

&mut T — Exclusive IDENTITY:

let mut x = vec![1, 2, 3];
let r = &mut x;
r.push(4);  // OK: exclusive access

One path to SPACE. TIME flows—mutation allowed. No conflict possible because no one else can see.

The borrow checker tracks: which names have IDENTITY to which SPACE, during which TIME regions. It proves no shared+exclusive overlap.

---

IDENTITY at Runtime

At runtime, names are gone. Only addresses remain.

RAM can reference itself.

RAM locations have addresses. Addresses are numbers. Numbers are data. Data can be stored in RAM. Therefore: RAM can store addresses of its own locations.

┌─────────┬───────────────┐
│  100    │   5       ← x │ ←──┐
├─────────┼───────────────┤    │
│  108    │  100      ← r │ ───┘
└─────────┴───────────────┘

This enables references, sharing, and complex structures.

Registers have no address.

Registers hold bytes but lack addresses. Taking a reference forces the value to stack.

let x = 5;      // might live in register
let r = &x;     // x now has address (stack)

Cost of sharing:

Cost	Cause
8 bytes	Address storage
Indirection	Follow address to reach data
Forces RAM	Registers have no address

For small types, copying is cheaper than referencing. This is why Copy exists.

---

Stack and Heap

Stack SPACE is automatic. Variables live on the stack. When they go out of scope, their SPACE is reclaimed. The compiler knows the size at compile time.

Heap SPACE is dynamic. For SPACE whose size isn’t known at compile time, or SPACE that outlives the current scope.

let b = Box::new(String::from("hello"));

Box::new(x) allocates SPACE on the heap, puts x there, and returns owning coordinates.

Rust	Ownership	Cleanup
&y	Borrowing	Not responsible
&mut y	Borrowing	Not responsible
Box::new(x)	Owning	Frees heap when dropped

No garbage collector. No manual free(). The compiler inserts cleanup at scope end.

---

Ownership and Move

let v = vec![1, 2, 3];
let w = v;  // IDENTITY transfers to w
// v is now invalid

Axis	What happens
IDENTITY	Transferred — old name invalid
SPACE	Same or new (compiler decides)
Coherence	Only one owner → no aliasing

The borrow checker tracks these transfers. After let w = v, using v is an error—its IDENTITY is gone.

Move semantics eliminate shared IDENTITY by default. No coherence problem if only one owner exists.

---

Copy vs Clone

Duplicating SPACE happens two ways:

Copy — Copy the bytes. Implicit on assignment.

Clone — Call .clone(). Always explicit.

When copying bytes works:

For i32, SPACE is self-contained. Copying bytes produces an independent value.

┌─────────┐    ┌─────────┐
│    5    │    │    5    │
└─────────┘    └─────────┘

When copying bytes fails:

For String, SPACE contains coordinates to heap SPACE:

┌─────────────────┐
│ addr: 0x1234    │     Heap:
│ len: 5          │     ┌───────────┐
│ capacity: 5     │     │ h e l l o │
└─────────────────┘     └───────────┘

Copying bytes would create two owners of the same heap SPACE—two IDENTITYs, coherence problem. Rust requires explicit choice: .clone() for deep copy, Rc::clone() for shared ownership, or move.

Type	Copy?	Clone?	Why
i32	Yes	Yes	Self-contained
&T	Yes	Yes	Coordinates, doesn't own
String	No	Yes	Owns heap—must choose strategy
Vec<T>	No	Yes	Owns heap

---

Shared Ownership

Box<T> is unique IDENTITY to SPACE. One owner, clear responsibility.

What if you need shared IDENTITY to the same SPACE? Who frees it?

Rc<T> / Arc<T>: count the IDENTITYs. When count hits zero, SPACE ends.

Type	IDENTITY	SPACE lifetime	Thread
Box<T>	Unique	Owner ends it	Any
Rc<T>	Shared, counted	Last IDENTITY ends it	Single
Arc<T>	Shared, atomic counted	Last IDENTITY ends it	Multi

This solves SPACE × IDENTITY. But contents are immutable—TIME is frozen.

To combine shared ownership with mutation, you need interior mutability.

---

Interior Mutability

The borrow checker is sound but incomplete:

• If it accepts → definitely safe
• If it rejects → might still be safe

Interior mutability handles the “might still be safe” cases by moving verification to runtime. Same rule, different when checked.

Type	Checked when	Cost	Thread
&T / &mut T	Compile	Zero	Any
Cell<T>	Runtime	Copy in/out	Single
RefCell<T>	Runtime	Borrow count	Single
Mutex<T>	Runtime	Lock	Multi
RwLock<T>	Runtime	Lock	Multi
Atomic*	Runtime	Hardware	Multi
UnsafeCell<T>	Never	Zero	Any

Cell — Copy values in/out. No references into contents.

let x = Cell::new(5);
x.set(10);       // mutate through shared ref
let v = x.get(); // returns copy

RefCell — Runtime borrow checker. Panics on violation.

let x = RefCell::new(vec![1, 2, 3]);
let r = x.borrow();      // shared
let s = x.borrow();      // OK
// x.borrow_mut();       // PANIC: already borrowed

Mutex — Serialize TIME. Only one accessor at a time.

let x = Mutex::new(vec![1, 2, 3]);
let mut guard = x.lock().unwrap();
guard.push(4);
// other threads block until guard drops

When to use:

Situation	Use
Simple flag, single thread	Cell<T>
Complex data, single thread	RefCell<T>
Shared across threads	Mutex<T>
Read-heavy, multi-thread	RwLock<T>
Counter, multi-thread	AtomicU64
Borrow checker accepts code	None needed

---

Thread Safety

Trait	Meaning
Send	IDENTITY can transfer across thread boundary
Sync	Shared IDENTITY (&T) safe across threads

// Rc<T> is !Send and !Sync — single-thread only
// Arc<T> is Send and Sync — multi-thread safe
// Mutex<T>: T is Send → Mutex<T> is Send + Sync

The borrow checker proves these at compile time. If your code compiles, thread safety is proven.

---

Summary

Problem	Rust's Solution
When to evaluate?	const (compile) vs let (runtime)
Where to store?	Inlined / stack / heap / static
Aliasing + mutation?	Borrow checker: shared OR exclusive
Global state?	static with atomics or interior mutability
Cross-thread sharing?	Send / Sync traits
Escaping the rules?	unsafe — you prove coherence

Rust's bet: prove coherence in compile-time projection. Pay with complexity. Gain zero-cost guarantees at runtime.

Equivalences

const ≅ inlined value ≅ no runtime IDENTITY
static ≅ single replica ≅ bridges projections
&T ≅ read replica ≅ shared IDENTITY, frozen TIME
&mut T ≅ exclusive lock ≅ unique IDENTITY, TIME flows
Mutex<T> ≅ distributed lock ≅ serialize TIME
move ≅ transfer ≅ IDENTITY changes hands
Clone ≅ snapshot ≅ new IDENTITY, new SPACE
unsafe ≅ "trust me" ≅ you prove coherence

---

Borrow Checker Internals

You’ve seen what the borrow checker enforces. Here’s how it works.

The Pipeline

The borrow checker operates entirely in compile-time projection:

Source Code
     │
     ▼
┌───────────────┐
│  Lower to MIR │ ← IDENTITY ops explicit
└───────────────┘
     │
     ▼
┌───────────────┐
│   Build CFG   │ ← branching TIME
└───────────────┘
     │
     ▼
┌───────────────┐
│   Liveness    │ ← "will this IDENTITY be used?"
└───────────────┘
     │
     ▼
┌───────────────┐
│    Region     │ ← compute minimal TIME spans
│   Inference   │
└───────────────┘
     │
     ▼
┌───────────────┐
│   Conflict    │ ← SPACE × TIME × IDENTITY check
│   Detection   │
└───────────────┘
     │
  ▼       ▼
 OK     ERROR

Phase 1: MIR

MIR makes IDENTITY operations explicit:

_2 = &(*_1)     // borrow: create IDENTITY
_3 = use(_2)   // use: access through IDENTITY
drop(_2)       // end: IDENTITY released

Phase 2: CFG

The function becomes a directed graph. Each node is a program point, edges are possible transitions.

TIME in a program is not linear. The CFG captures all possible orderings.

Phase 3: Liveness

Liveness asks: “From this point, on some future path, will this IDENTITY be used?”

Computed via backward dataflow. The IDENTITY must be valid at all points where it’s live.

Phase 4: Region Inference

A region is a set of CFG points. Regions form a lattice under subset ordering.

The solver finds the minimal region satisfying all constraints. Fixed-point iteration: expand regions until stable.

Phase 5: Conflict Detection

With regions computed, check for conflicts:

ERROR if:
  ∃ borrows B1, B2 of same SPACE where:
    - regions overlap
    - AND one is exclusive
    - AND B1 ≠ B2

SPACE Granularity Deep Dive

The borrow checker tracks paths:

• x — the whole binding
• x.field — a struct field (statically known)
• x[i] — an array element (runtime index)

Struct fields: statically known, can prove disjoint.

Array indices: runtime values, can’t prove i ≠ j in general.

Workarounds:

// split_at_mut divides into disjoint slices
let (left, right) = v.split_at_mut(1);
let r = &mut left[0];
let s = &mut right[0];  // OK: different slices

Decidability

The borrow checker uses decidable approximation:

Perfect question	Approximation
“Will this branch run?”	“Assume all branches might run”
“Same address?”	“Same base → might alias”
“Will this be used?”	“Might be used on some path”

Sound but incomplete:

• OK → definitely safe
• ERROR → might be safe (false positives exist)

This is why interior mutability exists: to handle false positives.

Rejected Valid Programs

Can’t prove branch won’t run:

let mut x = 5;
let r = &mut x;
if false {
    println!("{}", r);  // never runs
}
let s = &x;  // ERROR: r might be used

Can’t distinguish indices:

let mut v = vec![1, 2, 3];
let r = &mut v[0];
let s = &mut v[1];  // ERROR: two borrows of v

Curry-Howard

Types are propositions. Programs are proofs.

&'a T is a proof of: “There exists SPACE containing T, and IDENTITY to it is valid for TIME span ‘a.”

A successful borrow check means: “All IDENTITY/TIME claims are consistent.”

---

Memory Ordering

Atomics make operations indivisible. But when does a write in one TIME line become visible in another?

Hardware defers coherence:

• Store buffers: Writes queue locally before reaching RAM.
• Caches: Each core copies values locally. Writes don’t instantly propagate.
• Reordering: CPU executes out of order for performance.

All three: optimizations assuming single TIME line. Multiple TIME lines expose the deferred sync.

The Orderings

Relaxed — Atomic access only. No visibility guarantees.

Acquire/Release — Coherence at sync points.

Release: everything before this point visible before this write.

Acquire: everything after this sees writes from before a Release.

TIME line A:                TIME line B:

write x = 1
write y = 2
Release(flag = true)  ───>  Acquire(flag)
                            read y  // sees 2
                            read x  // sees 1

SeqCst — Total order. All TIME lines observe same sequence. Expensive.

Ordering	Guarantee	Use
Relaxed	Operation is atomic	Counters
Release	Writes before visible to Acquire	Producer
Acquire	Reads after see writes before Release	Consumer
AcqRel	Both	Read-modify-write
SeqCst	Global total order	When in doubt

---

Syntax

Rust overloads & and mut based on position.

Position Rules

Position	&mut x means
Expression (right of =)	Produce reference to x
Pattern (left of =)	Expect reference, bind target
Type (right of :)	Type “reference to T”

Examples

Expression:

let p = &mut x;  // produce exclusive IDENTITY

Pattern:

let &mut target = some_ref;  // follow IDENTITY, bind target

Primitives

Primitive	What
&	shared IDENTITY
&mut	exclusive IDENTITY
mut	rebindable binding

&mut is one token. There is no mut&.

Rebind vs mutate:

let mut x = &y;
x = &z;         // rebind: x now points elsewhere

let x = &mut y;
*x = 5;         // mutate: change what x points to

Clarifying Syntax

What if operations were explicit?

Current	Clarified	Meaning
let x = y	let x = move_or_copy(y)	compiler chooses
let x = &y	let x = shared(y)	shared IDENTITY
let x = &mut y	let x = exclusive(y)	exclusive IDENTITY
let mut x = 5	let rebindable(x) = 5	binding can change
let &x = r	let x = *r	dereference

Framework Translation

Rust	Framework
value	Occupies SPACE
binding	Name referring to SPACE
reference	IDENTITY pointing to SPACE
scope	TIME boundary for validity
&x (expression)	Create shared IDENTITY
&mut x (expression)	Create exclusive IDENTITY
&x (pattern)	Follow IDENTITY, bind result