Carbon memory safety
Goal of Carbon’s memory safety design
Smooth and incremental transition from C++ to memory safety in Carbon
- Result needs to be memory safe
- Expressivity to represent common C++ code patterns
- Makes the transition smooth
- Incremental in two ways
- Migrate to Carbon a little at a time
- Incrementally add safety once migrated
Two modes: permissive and strict
- Permissive mode, along with C++ interop, supports incremental migration
- Allows code that doesn’t yet have safety annotations
- Strict Carbon is fully memory safe
- The destination; goal is to migrate all code to strict mode
Strict Carbon is fully memory safe
- Temporal: Preventing “use after free” (UAF) at compile time
- Spatial: Runtime bounds checking as in 🦀 Rust and being added to C++
- Type, initialization, null pointer, and data race safety
Expressivity
- Non-exclusive mutable pointers
- Directly proving existing correct C++ code is memory safe
- Support for C++ features like inheritance and specialization
- More expressive than Rust, but with a complexity and verbosity cost
- Allows smooth migration of C++
- Code patterns translate without cliffs, rearchitecting, or lots of unsafe
Temporal safety
Preventing use after free at compile time
Anatomy of a use after free (C++)
#include <vector>
#include <cstdio>
int main() {
`<1>std::vector<int> x { 1, 20, 300 }`;
`<2>int* p = &x[0]`;
`<3>x.push_back(4000)`;
printf("%d\n", `<4>*p`); // <- 💣💥
}
- Allocation
- Capture a pointer into allocation
- Free or reallocation
- Use of dangling pointer
Anatomy of a use after free (Carbon)
import Core library "io";
fn Run() {
// ``buf(T)`` is Carbon's equivalent of C++'s
// ``std::vector<T>`` or Rust's ``Vec<T>``
`<1>var x: buf(i32) = (1, 20, 300)`;
`<2>var p: i32* = &x[0]`;
`<3>x.PushBack(4000)`;
// ❌ Compiler error: use of ``p`` after it was
// invalidated by ``x.PushBack(4000)``.
Core.Print(`<4>*p`);
}
- Allocation
- Capture a pointer into allocation
- Free or reallocation
- Prevents use of dangling pointer
No safety annotations in the calling code
import Core library "io";
fn Run() {
// ``buf(T)`` is Carbon's equivalent of C++'s
// ``std::vector<T>`` or Rust's ``Vec<T>``
var x: `<1>buf`(i32) = (1, 20, 300);
`<2>var p: i32* = &x[0]`;
`<3>x.PushBack(4000)`;
// ❌ Compiler error: use of ``p`` after it was
// invalidated by ``x.PushBack(4000)``.
Core.Print(*p);
}
- The safety annotations are on the
buftype- Explains how to safely use that type’s API
- Need something to connect the capture
pto the invalidation byPushBack
Place sets written using ^
- A variable has storage at some location in memory
var x: i32 = 1;
- A place represent the information we know about that location at compile-time
- The place of
xis written^x
- The place of
- A place set is a compile-time representation of set of places, also written using
^- The type for pointers and references include a place set specifying which places are accessible
- A container type will have a place set describing the places for its elements
How Carbon detects the error
import Core library "io";
fn Run() {
var `<2>x`: `<1>buf(i32)` = (1, 20, 300);
var p: `<4>i32*` = &`<3>x[0]`;
`<5>x.PushBack(4000)`;
// ❌ Compiler error: use of ``p`` after it was
// invalidated by ``x.PushBack(4000)``.
Core.Print(`<6>*p`);
}
class `<1>buf(T: ...)` {
disjoint `<2>owned ^Elts` of T;
impl as `<3>IndexRefWith`(i32)
fn (ref self, arg: i32)
-> `<4>^Elts ref T`;
fn PushBack(ref self, x: T)
`<5>invalidate(^Elts)`;
}
xowns a heap allocation.
&x[0]has type^x.Elts i32*.
^x.Eltstracks wherepcan point (may be omitted for locals).
- Call to
PushBackhas aninvalidate(^x.Elts)safety effect, invalidatingp.- The compiler checks that functions mark all needed effects.
- Use of invalidated pointer
pis a compile error.
Ingredients
import Core library "io";
fn Run() {
var x: buf(i32) = (1, 20, 300);
var p: `<2>i32* = &x[0]`;
x.PushBack(4000);
// `<4>❌ Compiler error`: use of ``p`` after it was
// invalidated by ``x.PushBack(4000)``.
Core.Print(*p);
}
class buf(T: ...) {
disjoint `<3>owned` `<1>^Elts` of T;
impl as IndexRefWith(i32)
fn (ref self, arg: i32)
-> `<1>^Elts` ref T;
fn PushBack(ref self, x: T)
`<4>invalidate`(`<1>^Elts`);
}
- Places and place set expressions: like
^Elts
- Alias tracking: which place sets can overlap?
- Ownership: types say their objects own some places
- Invalidation: by functions marked with safety effects
Places and place sets
^: the “places of” operator
- Every binding has a place
var `<1>x`: i32;
var p: `<2>^x` i32* = &x;
^xis the place where the variablexis stored
- Pointer types include the set of possible places they can point to
pcan point to^x
- When you take the address of a particular variable using
&x, you get its runtime address- The
^“places of” operator is parallel: it gets its compile-time place - So the type of
&xis a pointer to the^xplace
- The
Place set expressions
- Fields
class C {
var x: i32;
var y: i32;
}
var c: C = {.x = 1, .y = 2};
var px: ^c.x i32 = &c.x;
var py: `^c.y` i32 = &c.y;
var p_union: `^(c.x, c.y)` i32 = if F() then px else py;
var p_any: `^c.any` i32 = p_union;
Place set expressions
- Places in an owned allocation:
^x.Elts- Owning types have a named place set member, e.g.
Elts - Don’t distinguish between
x[0]andx[1]
- Owning types have a named place set member, e.g.
- Place set parameters
Similarities to Rust’s lifetimes
In both cases:
- Additional parameters to functions and types for safety
- Capturing a compile-time approximation of runtime behavior
- Used only for safety checking
Differences from Rust
Carbon places ^x
- Places are about space (memory)
- We ask if sets of places overlap
- Grounded in expressions using locals, parameters, fields
Rust lifetimes 'a
- Lifetimes are about time (source regions)
- We ask if a lifetime outlives another
- Abstract generic parameters
Alias tracking
What could this pointer reference?
Alias tracking
Three kinds:
- Aliasing between parameters
- Aliasing of parameters by returns
- Aliasing in data structures
Aliasing between parameters
By default, parameters may overlap
fn OverlapError(ref b: buf(i32), ref s: i32) invalidate(^b.Elts) {
b.PushBack(s);
// ❌ Error: ``s`` may overlap ``^b.Elts``,
// invalidated by ``b.PushBack(s)``.
s = b.Size();
}
b.PushBack(s) invalidates anything that could overlap an element of b.
Aliasing between parameters
Problematic caller
fn OverlapError(ref b: buf(i32), ref s: i32) invalidate(^b.Elts) {
b.PushBack(s);
// ❌ Error: ``s`` may overlap ``^b.Elts``,
// invalidated by ``b.PushBack(s)``.
s = b.Size();
}
fn ProblematicCaller() {
var b: buf(i32) = (1, 20, 300);
OverlapError(`ref b, ref b[0]`);
}
Aliasing between parameters
Fix: ^ to mark disjoint parameter
fn Fixed(ref b: buf(i32), `^` ref s: i32) invalidate(^b.Elts) {
b.PushBack(s);
// ✅ Okay: caller is required to ensure
// ``s`` doesn't overlap elements of ``b``.
s = b.Size();
}
fn ErrorNowInCaller() {
var b: buf(i32) = (1, 20, 300);
// ❌ Error: ``b[0]`` may overlap ``^b.any``,
// ``Fixed`` requires them to be disjoint.
Fixed(`ref b, ref b[0]`);
var s: i32 = 1;
// ✅ Okay: Every ``var`` gets its own
// storage, so ``s`` is disjoint.
Fixed(`ref b, ref s`);
}
Overlapping / disjoint parameters
- Have a whole vocabulary for expressing different “may overlap” vs. disjoint relationships between parameters
^for a disjoint parameter is the simplest annotation
- Every binding has its own place
- Use
^with a new name to introduce a new place set that can be used in multiple places ^defaultcontains all places that are not otherwise given a named container^anyincludes everything that can be referenced from any parameter
More to this than I’m going to go into
fn F(ref a1: i32, ref a2: i32,
^ ref b1: i32, ^ ref b2: i32,
^C ref c1: i32, ^C ref c2: i32,
^any ref d: {.x: i32, .y: i32});
Aliasing between parameters
🦀 Not an issue in Rust
- “Shared XOR mutable” means reference parameters can’t interact
- Parameter aliasing is additional information needed for safe non-exclusive mutable references
Aliasing of parameters by returns
By default, returns are allowed to reference ^default.any:
fn First(`<0>ref b: buf(i32)`) -> `<0>i32*` {
return &b[0];
}
fn UseAfterFree() {
var b: buf(i32) = (1, 20, 300);
`<1>var p: i32* = First(ref b)`;
// ✅ Okay: prints "1".
Core.Print(*p);
`<2>b.PushBack(4000)`;
// ❌ Error: ``*p`` may overlap ``^b.Elts``,
// invalidated by ``b.PushBack(4000)``.
Core.Print(*p);
}
^defaultcontains only^b, so the return type is^b.any i32*
pgets type^b.any i32*
^b.Eltsoverlaps^b.any, sopis invalidated as before
Use any of the parameter place names in returns
fn F(ref a1: i32, ref a2: i32,
^ ref b1: i32, ^ ref b2: i32,
^C ref c1: i32, ^C ref c2: i32,
^any ref e: {.x: i32, .y: i32})
-> `^____` ref i32;
- default is
^default.any= {^a1,^a2,^b1,^b2} - place of any parameter:
^a1,^a2,^b1,^b2,^c1,^c2 - fields:
^e.x,^e.y - named place sets:
^C= {^c1,^c2} ^any= {^a1,^a2,^b1,^b2,^c1,^c2,^e.x,^e.y}- any member:
^e.any= {^e.x,^e.y} - union:
^(a1, b1, C)is {^a1,^b1,^c1,^c2}
More similar to Rust than parameters
But still different
- 🦀 Rust says “return borrows from this parameter”
- Parameter must outlive the return (preventing use after free)
- What you can do with that parameter is limited until the borrow is done
- Enforces “shared XOR mutable”
- Connected by using the same lifetime parameter
- Carbon says “return may reference this field of this parameter”
- More precise: specific to a field
- No restrictions on parameter while being referenced
- Return’s reference is invalidated when parameter is
- Connected by the return referencing parameters by name
Aliasing in data structures
Types with external pointers
- No default for place parameters in a class definition
- Pointer fields must specify explicitly what they can point to
- To reference something external, the class needs to have a place parameter
- No other way to reference something outside the class
class HasPtr(`^A of i32`) {
var p: `^A` i32*;
}
fn Example() {
var i: i32 = 1;
var has_ptr: HasPtr(`^i`) = {.p = &i};
}
🦀 Rust similarly requires a lifetime parameter when fields reference something outside that struct. The relationship is similar as for returns.
Automatic aliasing for locals
- Few safety annotations needed for locals
- More concise
- More like C++
- Uses flow-sensitive analysis for precision
- Reduces invalidations
- Analysis comes after overload resolution
- Overloads selected is an input into the analysis
Ownership and invalidation
Two intertwined concepts
- Invalidation effect
- An example of safety effects, which are used for other parts of the safety story
- Propagated up the call stack
- Explicitly in function signatures
- Increases precision by making invalidation opt-in instead of assumed
- Similar to how knowing places are disjoint allows us to reduce invalidations
- Ownership
- Single owner per allocation
- Can only invalidate by writing to the owner
- Owner is never invalidated
buf again
class buf(T: ...) {
// Declare ownership of a set of places.
`<4>disjoint` `<1>owned ^Elts` of T;
// Destroys elements, invalidating pointers
// to them and anything they own.
fn Clear(ref self) invalidate(`<2>^Elts.any`);
// May reallocate, causing a relocation of elements
// and invalidating pointers to them.
fn PushBack(ref self, x: T) invalidate(`<3>^Elts`);
}
- Destruction invalidates more than relocation
- Don’t have to invalidate a separate allocation when relocating
disjoint owned ^Eltsmeans^Eltsrefers to a separate allocation
Ownership means “independent fate”
- Fields share fate with their containing object
- Owned data can be invalidated earlier
- Like when the buffer is resized
- Ownership of data can be transferred
- Owned data can outlive its original owner as a result
- Can survive the owner being relocated
Transfer of ownership
- Two effects that are refinements of
invalidate:mixandmove - Local pointer types with automatic place sets are updated
- Allows less invalidation when relocating
class buf(T: ...) {
disjoint owned ^Elts of T;
// Transfers ownership
fn Swap(ref self, ref other: Self)
move(^self, ^other) move(^other, ^self);
}
fn UsesSwap() {
var x: buf(i32) = (1, 2, 3);
var y: buf(i32) = (4, 5)
var p: i32* = &x[0];
var q: ^(x, y).Elts i32* = &y[0];
x.Swap(ref y);
// ``p`` and ``q`` still valid after ``Swap``
Use(p, q);
}
Owners are never invalidated
fn Run() {
var x: buf(i32) = (1, 20, 300);
var p: i32* = &x[0];
`<1>x.PushBack(4000)`;
// ``p`` invalidated by ``x.PushBack``.
// ❌ Core.Print(*p);
// ✅ ``x`` is the owner, so still valid.
`<2>p = &x[0]`;
// ✅ Okay, ``p`` is valid again; may have
// a different value if ``x`` reallocated.
`<3>Core.Print(*p)`;
}
Allows recovery after invalidation
Always a single owner
- Owner enforces invariants
- Never invalid
- No double free
- Automatically avoid leaks
- Ownership is transferred, never duplicated
- Two objects are disjoint if their owners are disjoint
- Used to reduce unnecessary invalidations
Owning enforcement in very few types
- Few fundamental owning types:
Box,HeapArray: does heap allocationInlineStorage: used by sum types, and for small-size optimization
- Okay that they have unsafe code
- Other owning types like
bufare built on top
How do we make reference counted types like std::shared_ptr<T> safe?
- Shared ownership modelled as pointers to a single owner
- That pointer means those types have a place parameter
- Unlike 🦀 Rust where
RcandArcdon’t have lifetime parameters
- Unlike 🦀 Rust where
- May reference the same owned data if their place arguments overlap
- Non-owning pointers to that place set are invalidated when any shared owner is freed
- But shared owners remain valid (by using
unsafeinternally)
- But shared owners remain valid (by using
Type erasure
Type erasure: generics
Here we have an interface (like a Rust trait). Different types will implement this interface in different ways. What effects should the method in the interface have?
interface Notified {
fn Event(ref self) ???;
}
- A generic user of the
Notifiedinterface will use whatever effect is in the interface - To be safe, a type’s implementation of this interface must have a subset of the interface’s safety effects
Type erasure: generics
Here we have an interface (like a Rust trait). Different types will implement this interface in different ways. What effects should the method in the interface have?
interface Notified {
fn Event(ref self) unknown;
}
- A generic user of the
Notifiedinterface will use whatever effect is in the interface - To be safe, a type’s implementation of this interface must have a subset of the interface’s safety effects
unknownis the maximum effect that the type allows, invalidating anything reachable that is owned by something writable
Type erasure: generics
interface Notified {
fn Event(ref self) unknown;
}
- Can use a non-owning type to avoid invalidation
- Use
std::spaninstead ofstd::vectorif you aren’t changing the vector’s size - Leverages Carbon’s freedom to have multiple pointers to the same thing
- Use
- Casting to
constalso limits effects
Type erasure: inheritance
base class B(^A) {
virtual fn F(ref self) unknown;
}
class D(^X, ^Y) {
extend base: B(^(X, Y));
override fn F(ref self);
}
Virtual methods in base class must have safety effects that encompass derived implementation effects
- Similar to an interface.
Type erasure: inheritance
base class B(^A) {
virtual fn F(ref self) unknown;
}
class D(^X, ^Y) {
extend base: B(^(X, Y));
override fn F(ref self);
var p: ^X i32*;
var q: ^Y i32*;
}
Additionally need to track aliasing
- Base class must have place parameters that encompass place parameters of derived classes
- Maintains invariant that pointers can only reference external objects from type parameters
Type erasure: erased place parameters
`<1>interface I`;
`<2>fn Generic`[`<8>T`: I](ref z: `<8>T`, ref w: `<8>T`);
`<3>class C(^A)`;
`<4>impl C(^B) as I`;
fn `<5>ConcreteCaller`(`<6>^ ref x`: C(`<7>^D`), `<6>^ ref y`: C(`<7>^D`)) {
`<8>Generic`(ref x, ref y);
}
^x.anyand^y.anyinConcreteCallerare disjoint
- but both
xandycan reference^D
- Call to
GenericdeducesTto beC(^D)
- So inside
Generic,^z.anyand^w.anyoverlap - Invariant: every reachable place must have a place name in the local scope
- When the generic call erases
^D, those places get added to^z.anyand^w.any
- When the generic call erases
Expressivity
Support for common C++ patterns
Expressivity is important
Benefits:
- Can show more things memory safe
- Adds flexibility when structuring code
- Enables migration of C++ code to Carbon
Goal: Represent common C++ coding patterns in strict Carbon with minimal use of unsafe and rearchitecting.
Mutability without exclusivity
// Parameters can optionally alias
fn Swap(`<2>ref x: i32`, `<2>ref y: i32`) {
// Implementation works even if &x == &y.
let tmp: i32 = x;
x = y;
y = tmp;
}
fn FisherYatesShuffle(ref vec: buf(i32)) {
for (i: i32 in Core.IntRange(vec.Size() - 2)) {
let j: i32 = Random(i, vec.Size());
// Two simultaneous mutable references into ``vec``
Swap(`<1>ref vec[i]`, `<1>ref vec[j]`);
}
}
- 🦀 Would need changes to work under Rust’s “shared XOR mutable” restriction
- The two references may point to the same element
- Unsafe code making an aliasing pointer won’t introduce UB
Self reference
- An object can have pointers to other fields in the same instance
class Form {
var first: strbuf;
var last: strbuf;
var current: ^(first, last) strbuf*;
}
- This is used in some small-size optimization implementations
- Pointer either points to an inline buffer or heap allocation
C++ features supported by Carbon but not Rust
Carbon has a large commitment to supporting C++ features independent of safety
- Inheritance
- Specialization
- Templates
- Implicit conversions
- Function overloading
- …
Other kinds of safety
Same mechanisms
The same mechanisms used to enforce use-after-free:
- Safety effects (like invalidation)
- Places and place sets
- Function input requirements (like overlap/disjoint)
- Types
are also used to enforce other safety properties.
Thread safety goals
- Straight translation of Clang’s
-Wthread-safetythread-safety annotations - Prevent data races
Not trying to prevent deadlock, no guarantee of forward progress
Thread safety approach
- Each mutex has a place set of
guardedvariables - Safety effects for important events (similar to invalidation)
- Acquiring or releasing locks
- Sharing places across threads
- Status tracked in flow-sensitive state and function signatures
- Shared places can only be passed to
sharedparameters - Lock requirements are function constraints
- Shared places can only be passed to
- Restrict access to
shareddata unlessguardedby a lock that is held sharedis an addition beyond the C++ annotations
Thread safety example
class BankAccount {
private:
std::mutex mu;
int balance `<1>GUARDED_BY(mu)`;
void Withdraw(int amount)
`<2>REQUIRES(mu)` {
balance -= amount;
}
void Deposit(int amount) {
`<7>balance += amount; // ⚠️ Warning`
}
public:
void TransferFrom(BankAccount& b,
int amount) {
`<5>mu.lock()`;
b.Withdraw(amount); // ⚠️ Warning
Deposit(amount);
mu.unlock();
}
};
class BankAccount {
private var mu: Core.Mutex;
private `<1>guarded(mu)` var balance: i32;
private fn Withdraw(
`<4>shared` ref self, amount: i32)
`<2>where locked(mu)` {
`<3>self.balance -= amount`;
}
private fn Deposit(`<9>ref` self, amount: i32) {
`<7>self.balance += amount;`
}
fn TransferFrom(`<9>shared ref` self,
shared ref b: Self, amount: i32)`<10> `{
`<5>self.mu.Lock()`;
`<6>b.Withdraw(amount); // ❌ Error`
`<8>self.Deposit(amount); // ❌ Error`
`<10>self.mu.Unlock()`;
}
}
- Deeply immutable until you reach something with interior mutability
- 🦀 Rust: getting that
&reference to share across threads uses a shared borrow - Carbon: gets a similar result using sharing safety effects
Differences from Rust
- Approach to interior mutability
- 🦀 Rust: a mutex contains the guarded data
- Carbon: a mutex guards other variables
- Use of shared references
- 🦀 Rust: pervasive
- Carbon: only when sharing across threads
- Carbon doesn’t mark thread safety on types
- Contrast with 🦀 Rust’s
SendandSynctraits - Can always make a
sharedreference to an object - Methods opt-in to working on a
sharedreference
- Contrast with 🦀 Rust’s
Differences from Rust
- Approach to interior mutability
- Use of shared references
- Carbon doesn’t mark thread safety on types
- Contrast with 🦀 Rust’s
SendandSynctraits - Can always make a
sharedreference to an object - Methods opt-in to working on a
sharedreference
- Contrast with 🦀 Rust’s
class BankAccount {
// Can operate on shared references
private fn Withdraw(`<1>shared ref` self, amount: i32) ...;
// Can't operate on shared references
private fn Deposit(`<2>ref` self, amount: i32);
}
Initialization safety
- Safety effects mark functions that perform initialization or destructive move
- Flow-sensitive state tracks initialization status for locals
- No full path-sensitivity or correlated conditions
- No inlining
- Just simple static rules
- For non-locals, fields and parameters are required to be initialized unless a wrapper type is used
- Similar to 🦀 Rust’s
MaybeUninit
- Similar to 🦀 Rust’s
Migrating C++ → strict Carbon
Using permissive mode and interop
Incremental migration from C++ → strict Carbon
Non-goals
- Adding safety annotations to C++ code
- Proving arbitrary C++ code is safe
Incremental migration from C++ → strict Carbon
Instead, our goals are:
- Mechanical migration of C++ to permissive Carbon
- Deploy safety annotations and safety checking in Carbon
- Incremental steps for each these migrations
- Fine-grained C++ → Carbon migration
- Safety annotations can be introduced gradually
- Flexible order and layering
Incremental migration from C++ → strict Carbon
How we achieve those goals
Permissive mode acts as an intermediate step between C++ and strict Carbon
- Allows a mechanical migration from C++
- Syntax and semantics of Carbon
- Safety checks are relaxed, no safety annotations required
C++
↓
permissive Carbon
↓
strict Carbon
Incremental migration from C++ → strict Carbon
How we achieve those goals
C++ interop in both directions
- Migrate in smaller pieces
- In any order
- Permissive Carbon can call C++ freely
- Strict Carbon can call C++, with restrictions
Carbon ⇄ C++
Every step improves safety
- Permissive Carbon is safer than C++
- Less undefined behavior (UB)
- Strict checking doesn’t introduce UB even when interacting with permissive or unsafe code
“unsafe”
unsafe: Escape hatch to perform dangerous unchecked operations
- No
unsafeblocks, justunsafeoperations - Operations that would be considered dangerous in C++ are marked
unsafeeven in permissive mode (reinterpret or const cast) - Anything that can’t be checked is an
unsafeoperation in strict mode - Calls to unsafe functions must be marked
unsafe
Multi-step migration strategy
- Migrate C++ → permissive Carbon
- Define safety contract in permissive Carbon
- Uses Carbon-specific safety annotations
- Affects strict Carbon callers
- Switch Carbon from permissive → strict
- Requires fixing violations or
unsafe
- Requires fixing violations or
Alternatively:
- Define safety contract with a Carbon wrapper
- Implemented with C++ interop
- Migrate C++ to Carbon later
Example: C++ → permissive Carbon
C++ code
class Tournament {
private:
std::vector<Location> venues_;
std::vector<Team> teams_;
public:
auto EliminationRound(
const Matches& semis) -> void {
// ...
teams_.resize(new_size);
}
auto Venue(const Matches& semis) const
-> const Location*;
// ...
};
Permissive Carbon
class Tournament {
private venues_: buf(Location);
private teams_: buf(Team);
fn EliminationRound(
ref self, semis: Matches) {
// ...
self.teams_.Resize(new_size);
}
fn Venue(self, semis: Matches)
-> const Location*;
// ...
}
Example: C++ → permissive Carbon
C++ code
class Tournament {
public:
auto EliminationRound(
const Matches& semis) -> void;
auto Venue(const Matches& semis) const
-> const Location*;
};
auto Finals(
Tournament& t,
const Matches& semis) -> void {
const Location* l = t.Venue(semis);
t.EliminationRound(semis);
ScheduleGame(l, t);
}
Permissive Carbon
class Tournament {
fn EliminationRound(
ref self, semis: Matches);
fn Venue(self, semis: Matches)
-> const Location*;
}
fn Finals(
ref t: Tournament,
semis: Matches) {
let l: const Location* = t.Venue(semis);
t.EliminationRound(semis);
ScheduleGame(l, ref t);
}
Example: permissive → strict (step 1)
Permissive Carbon
class Tournament {
private venues_: buf(Location);
private teams_: buf(Team);
fn EliminationRound(
ref self, semis: Matches) {
// ...
self.teams_.Resize(new_size);
}
fn Venue(self, semis: Matches)
-> const Location*;
// ...
}
Strict Carbon
class Tournament {
private venues_: buf(Location);
private teams_: buf(Team);
fn EliminationRound(
ref self, semis: Matches) {
// ...
// ❌ Error: call to ``Resize``
// invalidates ``^teams_.Elts``,
// effect not in function signature.
`self.teams_.Resize(new_size)`;
}
fn Venue(self, semis: Matches)
-> const Location*;
// ...
}
Example: permissive → strict (step 1)
Strict Carbon with error
class Tournament {
private venues_: buf(Location);
private teams_: buf(Team);
fn EliminationRound(
ref self, semis: Matches) {
// ...
// ❌ Error: call to ``Resize``
// invalidates `<3>^teams_.Elts`,
// `<2>effect not in function signature`.
self.teams_.Resize(new_size);
}
fn Venue(self, semis: Matches)
-> const Location*;
// ...
}
Strict Carbon (fixed)
class Tournament {
private venues_: buf(Location);
private teams_: buf(Team);
alias `<3>^Teams = ^teams_.Elts`;
fn EliminationRound(
ref self, semis: Matches)
`<2>invalidate`(`<3>^Teams`) {
// ...
self.teams_.Resize(new_size);
}
fn Venue(self, semis: Matches)
-> const Location*;
// ...
}
Example: permissive → strict (step 2)
Permissive Carbon
fn Finals(ref t: Tournament,
semis: Matches) {
let l: const Location* = t.Venue(semis);
t.EliminationRound(semis);
ScheduleGame(l, ref t);
}
Strict Carbon
class Tournament {
fn EliminationRound(
ref self, semis: Matches)
`<3>invalidate(^Teams)`;
fn Venue(self, semis: Matches)
-> const Location*;
}
fn Finals(ref t: Tournament,
semis: Matches) {
let l: const Location* = t.Venue(semis);
`<3>t.EliminationRound(semis)`;
// ❌ Error: use of ``l`` after invalidation
// by ``t.EliminationRound(semis)``
ScheduleGame(`<4>l`, ref t);
// ❌ Error: call to ``t.EliminationRound``
// invalidates ``^t.Teams``, effect not in
// function signature.
}
Example: permissive -> strict (step 2)
Strict Carbon with errors
class Tournament {
fn EliminationRound(
ref self, semis: Matches)
invalidate(^Teams);
fn Venue(self, semis: Matches)
-> const Location*;
}
fn Finals(ref t: Tournament,
semis: Matches) {
let l: const Location* = t.Venue(semis);
t.EliminationRound(semis);
// ❌ Error: use of ```<2>l``` after invalidation
// by ``t.EliminationRound(semis)``
ScheduleGame(l, ref t);
// ❌ Error: call to ``t.EliminationRound``
// invalidates ```<4>^t.Teams```, effect not in
// function signature.
}
Strict Carbon (fixed)
class Tournament {
alias `<3>^Venues = ^venues_.Elts`;
fn EliminationRound(
ref self, semis: Matches)
invalidate(^Teams);
fn Venue(self, semis: Matches)
-> const `<3>^Venues` Location*;
}
fn Finals(ref t: Tournament,
semis: Matches)
`<4>invalidate(^t.Teams)` {
let l: const Location* = `<2>t.Venue(semis)`;
t.EliminationRound(semis);
ScheduleGame(l, ref t);
}
Field granularity
We could prove this example is safe due to the additional precision of field granularity.
- This example is a retheming of code from Dawn, a WebGPU implementation
🦀 There is a proposed change to the Rust safety model called view types for providing field granularity
- A work-in-progress
Carbon / C++ interop
Allows mixing C++ and Carbon during migration
Interop: Strict Carbon calling C++
Conservative heuristic C++ contract assumed
import Cpp library "<vector>";
fn Run() {
// C++ std::vector<T>
var x: `<1>Cpp.std.vector(i32)` = (1, 20, 300);
// `<2>Pointer into ^x.any`
var p: i32* = &x[0];
// `<3>Any non-const method invalidates`
// iterators from and pointers into ``x``.
x.push_back(4000);
// ❌ Compiler error: use of ``p`` after it was
// invalidated by ``x.PushBack(4000)``.
Core.Print(*p);
}
- Assumes returns can alias anything reachable from parameters, including
*this
unknowneffect: all non-conststd::vectormethods will invalidate all derived pointers and iterators
Interop: Strict Carbon calling C++
Conservative heuristic will have false positives
fn Run() {
// C++ std::vector<T>
var x: Cpp.std.vector(i32) = (1, 20, 300);
// Pointer into ``^x.any``.
var p: `<1>i32* = &x[0]`;
// `<2>x[1] is a non-const method call!`
// so it invalidates ``p``!
var q: `<2>i32* = &x[1]`;
// ❌ Compiler error: use of ``p`` after it was
// invalidated by ``x[1]``.
Core.Print(*p);
}
[]operator can invalidate in other containers, such asabsl::flat_hash_map
- Can’t be more precise without additional information about the C++ API
Interop: Carbon calling C++
Argument aliasing heuristic
“shared XOR mutable” rule for allowed aliasing of reference parameters
void F(`<1>const int& a`, `<1>const int& b`, `<2>int& c`, `<2>int& d`);
aandbareconstand so may overlap
canddare notconstand so must be disjoint from each other and fromaandb
- As if this Carbon function:
void F(const ref a: i32, const ref b: i32,
^ ref c: i32, ^ ref d: i32);
Interop: Carbon calling C++
Data structure aliasing
- C++ classes that can reference external/unowned memory have an additional place set parameter in Carbon
- Includes C++ base classes accessed by a pointer or reference
- Assumption is returned objects could reference anything passed in
Interop: Strict Carbon calling C++
Heuristic is precise for simple APIs
Don’t have to write a wrapper to call C++ functions unless there is something interesting to say about the safety contract (some choice not expressed in the C++ signature)
- Functions that don’t take pointer parameters beyond
this - Functions that don’t return pointers or references
- Or the caller shouldn’t hold onto the return, like with
Cpp.std.cout <<…
- Or the caller shouldn’t hold onto the return, like with
- Or the heuristic is close enough that no wrapper is needed
Interop: Strict Carbon calling C++
Heuristic is sufficient for light usage
- Fewer wrappers means less boilerplate, toil, and friction
Reverse interop: C++ calling Carbon
- Actual argument values of place parameters are erased, and so are not required to call Carbon
- (also needed for separate compilation)
- Carbon assumes C++ code respects the aliasing constraints specified in Carbon signatures
Eliminating undefined behavior
by migrating to strict Carbon
Undefined behavior (UB)
- Fully strict code has no UB
- Permissive code has a subset of the UB of the corresponding C++ code
- Even with no safety annotations
- Some UB is diagnosed (e.g. ODR)
- Some UB becomes erroneous behavior (signed arithmetic overflow)
- Means won’t optimize based on unvalidated assumptions that could introduce UB
- Carbon code always has at most the UB of the corresponding C++ code
- Execution within Carbon, with no C++, only has UB in permissive mode or after the execution passes through an operation marked
unsafe
Undefined behavior (UB)
Mixing modes doesn’t compromise safety
Adding safety annotations to permissive code or switching to strict mode never introduces UB
- May optimize based on safety information, but not in ways that introduce UB if unsafe code compromises safety assumptions
- 🦀 No Rustonomicon saying it is UB to to alias a mutable reference
- Unsafe Rust can be more unsafe than C++ because it introduces new requirements that are not checked
- Means giving up some performance optimization opportunities
Undefined behavior (UB)
Reasonable C++ code doesn’t compromise safety
As long as C++ code follows a set of rules, it won’t compromise Carbon’s safety checks
- Code violating the rules should be recognized as either buggy or dangerous by C++ developers
- Should be reasonable to build a sanitizer to detect violations of the rules
- Like Clang’s upcoming
-fbounds-safety
- Like Clang’s upcoming
- Example:
delete this;is considered dangerous, and Carbon assumes the C++ code won’t do it
Undefined behavior (UB)
Carbon won’t introduce UB based on safety assumptions
- C++ UB, or unreasonable but well-defined C++, may compromise safety checks
- Even when safety checks have been compromised, Carbon code will have less UB than the equivalent C++
Conclusion
In summary
Smooth and incremental transition from C++ to safe Carbon
- Memory Safe
- Compile-time use-after-free checking
- Expressive
- Common C++ patterns made safe without rearchitecting
- Incremental
- Interop and permissive mode
More resources: Safety units
Safety units are how we’ve developed the memory safety design
- Google Drive folder
- Will be distilled into official proposals that update Carbon’s design
Some safety units of interest:
- Catalog of place set expressions and safety annotations: safety unit 40
- Initialization safety: safety unit 26
- Thread safety WIP: examples, safety units 27, 37, 43
This presentation: https://chandlerc.blog/slides/2026-memory-safety-deep-3/
Feedback
Please join us in the #safety channel in Carbon’s Discord
https://docs.carbon-lang.dev/#join-us has instructions for joining the community
- I am
josh11bon Carbon’s Discord and GitHub - I am
Josh Lon rust-lang Zulip
Appendix: Flow-sensitivity
Flow-sensitivity is used in a few places
- Automatic aliasing for locals
- Which places are currently shared across threads
- Which places have been initialized
Gives a precise answer without having to be explicit in the source, but flow-sensitive analysis comes after semantics, so can’t influence overload or impl selection. Only affects validity.
Automatic aliasing for locals
fn F() {
var x: i32 = 1;
var y: i32 = 2;
var p: `<0>i32*` = `<1>&x`;
if (true) {
`<8>var z`: i32 = 3;
`<2>p = &z`;
while (true) `<6>{`
if (G(p)) {
`<3>p = &x`;
} else {
`<4>p = &y`;
}
`<5>if` (H(p)) {
`<7>break`;
}
}
`<8>}`
`<9>J(p)`;
}
`<0>p has type ^*p i32*`, `<1>^*p = ^x`
`<2>^*p = ^z`
`<6>^*p = ^(x, y, z)`
`<3>^*p = ^x`
`<4>^*p = ^y`
`<5>^*p = ^(x, y)`
`<7>^*p = ^(x, y)`
`<8>^*p = ^(x, y), ^z invalidated`
`<9>^*p = ^(x, y)`, ``p`` is still valid
Properties of places
Fixed:
- Single place or multiple?
- Type?
- Overlap with other places?
Flow-sensitive:
- Initialized?
- Can write?
- Shared across threads?
- Guarding mutex is currently acquired?
Addendum
How we got here
This is the third safety model we considered
First approach: Ante’s Rust-like model
- Take Rust and add non-exclusive mutable borrows
- Struggled with transitions between the three modes:
- Exclusive (needed for things that e.g. reallocated)
- Non-exclusive mutable (more flexible when applicable)
- Immutable shared
- Concerns about having too many pointer types
- Lacked expressivity and precision
- Field granularity requires additional mechanisms (view types)
- Doesn’t handle different methods requiring different capabilities from fields
- Expected to work, and so became our backup plan while we explored other options
- The Algebra of Loans in Rust: most promising direction
This is the third safety model we considered
2nd: Safety effects model with flow-sensitive checking
- Inspired by group borrows blog posts (nmsmith, verdagon.dev)
- Very precise in simple cases
- Delays commitment to what capabilities are needed by a type until actually calling the method that needs that capabilities
- Can add more kinds of effects to increase precision
- Example: writes were an effect rather than
constrestricting what the type could do- Less code duplication to be const correct (nim-lang.org)
- Struggles with precision when there is type erasure
- Found potential workarounds, but ends up far down the road of reproducing the body of the function in the signature
FcallsGand so has whatever effectsGhas
This is the third safety model we considered
Final model: Goldilocks hybrid
- Hybrid between the two previous models
- Uses types,
const, and ownership to limit possible effects with type erasure - Uses safety effects and flow-sensitivity sparingly where they are most helpful
- Reference card of effects, not a wall poster
- Fewer pointer types (since never exclusive) and more compatibility between them than the Ante approach
- “
constonly on pointers/references not types” and “preserveconst” reduce the need for code duplication for const correctness
Addendum
const
const
- Means: restricting permission to mutate through this path
- Const in Carbon is on places (and therefore pointers and references), not types
- Const ≠ immutability
- Arises naturally from non-exclusive pointers: if pointer
pcan point toxory, andxis immutable, can’t change throughp, but a change toymight be observed throughp. - Better match for C++
- Arises naturally from non-exclusive pointers: if pointer
- Invalidation requires mutation, can use const to limit permissions, reducing the effects of generic or otherwise type erased code
Immutable borrows instead of expensive copies
- If you don’t mutate an object, a
constreference is equivalent to a copy- Much cheaper for some types
- Carbon defaults to “value” calling convention
- Different behavior for different types
- Copies types where that is cheap
- Or an immutable borrow +
constreference- An error if a copy is needed
- Means expensive copies will be explicit in source
- Good for generics where
Torconst T&will be more efficient depending onT
Immutable borrows
- Rule: something that could overlap an immutable borrow can’t be passed mutably
- Validation that signatures of calls agrees with flow-sensitive state
- Checked in the second “safety effect checking” step that doesn’t affect semantics
- But Carbon’s immutable borrows are not first class
- Only for parameters and locals, not in data structures
- Tracking which places are immutable similar to which places have been shared across threads
- Both are flow-sensitive tracking of status of places
- Difference in triggers (value parameter borrows vs. safety effects)
- Difference in capabilities (no writes vs. no reads or writes)
Preserve const
- “Preserve
const” means:- Function doesn’t mutate through parameter
- Function returns a derived reference
- Caller can figure out if derived reference should be
constbased on what was passed in to the parameter
- Avoids
constand non-constversions of the same function
class C {
var field: i32;
// ``const ref self`` -> doesn't mutate ``self``
// ``^field i32*`` -> returns pointer to ``self.field``
// ``const`` if ``self`` is ``const`` in caller
fn PreservesConst(const ref self) -> ^field i32* {
return &self.field;
}
}