Choosing arenas over borrow checking

June 22, 2026

Salt has no lifetime annotations. No 'a, no &'b mut, no Rc<RefCell<T>> escape hatches. The language never asks you to teach a borrow checker about the relative ordering of your objects. Arena allocation, paired with compile-time escape analysis, produces deterministic performance without the annotation burden.

The systems memory trilemma

Every systems language faces a three-way choice about memory management.

Manual memory management (C, C++ with raw pointers). You control every allocation and free. The machine does exactly what you say. The cost is that you must also be right about what you say — every time. Use-after-free, double-free, buffer overrun, null-pointer dereference: CVE after CVE traces to a single free() call that was right 99.9% of the time and wrong on the 0.1% path nobody tested. Performance is maximized; safety is manual and fallible.

Garbage collection (Go, Java, OCaml). You allocate freely. A tracing collector identifies unreachable objects and reclaims them in a periodic pause. The cost is that the pause is unpredictable—and for systems code (a kernel interrupt handler, a network-packet dispatch loop), unpredictability is unacceptable. You cannot take 10 milliseconds to scan the heap when you are holding a spinlock. GC gives safety and programmer productivity at the expense of latency determinism.

Borrow checking (Rust). Compile-time reference tracking ensures that every borrow is valid for its lifetime. No GC pause, no dangling pointer. The cost is annotation ergonomics and code-structure constraints. Rust’s borrow checker is a serious piece of engineering. It also forces you to reason about lifetimes whether or not your problem needs them. And when your data structure doesn’t fit the tree-of-ownership model—graphs, arenas, intrusive lists—you reach for unsafe, Pin, or reference counting, each of which reintroduces some of the costs the borrow checker was meant to eliminate.

The result is a language with the safety properties of Rust, the latency profile of C, and no lifetime annotations on any function signature.

The arena model

An arena is a fixed-size region of memory. Allocation is a single pointer bump: reserve n bytes, advance the bump pointer by n, return the old value. Deallocation is O(1) — reset the bump pointer to the start of the region. There is no free list, no coalescing, no fragmentation.

arena RequestArena : Arena {
    capacity: 64 * 1024;   // 64 KiB per request
}

fn handle_request(arena: &RequestArena, req: &Request) -> Response
{
    let path   = arena.alloc_str(req.path);    // bump-allocated
    let query  = arena.alloc_map();             // hash map in arena memory
    let result = dispatch(path, query);
    arena.reset();                              // O(1): all memory reclaimed
    return result;
}

Every allocation within the request handler is bump-allocated into the arena. When the request completes, a single reset() frees everything. There is no per-object free(), no reference-counting decrement, no garbage-collection pause. The allocator is a single pointer write.

This is not a new idea. Apache used apr_pool_t for this purpose. Region-based allocation appears in the ML Kit and the Cyclone language. What is new is combining it with compile-time guarantees that escape is impossible—without requiring the programmer to write lifetime annotations.

The scope ladder

Salt’s static escape analysis is built on a concept called the scope ladder. Every expression and every block has an associated scope depth: a small integer that encodes how long the value can safely live.

The scope ladder tracks three rules:

Return Rule. A function cannot return a pointer into a local arena. If handle_request tried to return path (which lives only for the duration of the arena), the compiler rejects it. The scope of the arena is a function level; the return value must have function-level scope or higher.

Assignment Rule. A value can be stored only in a container whose scope is at most as deep as the value’s own scope. You cannot put a request-local path into a connection-level cache. The compiler tracks the arena provenance of every pointer and ensures that the destination’s expected lifetime is a subset of the source’s.

Transitivity Rule. If a struct contains a pointer, the pointer’s scope constrains the struct’s scope. A Response that holds a StringView into an arena cannot outlive that arena. Z3 verifies this by translating scope constraints into linear arithmetic formulas that the solver can check in sub-millisecond time.

type StringView = { ptr: *u8, len: u64 };

fn parse_path(arena: &Arena, raw: &[u8]) -> StringView
    requires(raw.len() < arena.capacity)
{
    let slice = arena.alloc_slice(u8, raw.len());
    std::mem::copy(raw, slice);
    return { ptr: &slice[0], len: raw.len() };
    // Scope check: StringView.ptr = Arena scope, this is fn scope.
    // Return scope must be >= Arena scope. OK.
}

fn bad_return(arena: &Arena) -> StringView
{
    let local_buf: [u8; 64] = [0; 64];
    return { ptr: &local_buf[0], len: 64 };
    // ERROR: local_buf is stack-local (depth 2),
    // but return type expects at least arena scope (depth 1).
}

The scope ladder is not a new invention. It is region analysis, known since Tofte and Talpin’s work in the 1990s. What makes it practical in Salt is that the programmer never writes a scope annotation. The compiler infers scopes from the arena declaration and the structure of the code. The rules are enforced silently. When you violate them, the error message names the value, the scope it requires, and the scope it would escape into.

What it catches in practice

Three classes of bugs are eliminated at compile time.

Return escape. A common mistake in arena-based prototypes is returning a pointer into an arena that is about to be reset. The scope ladder catches this automatically:

fn process_connection(conn: &Connection) -> Response
{
    let arena = Arena::with_capacity(64 * 1024);
    let req   = arena.alloc(Request);
    parse(&arena, conn.buffer, req);
    let resp  = build_response(req);
    arena.reset();
    return resp;
    // If resp contained a pointer into arena, the compiler rejects it.
}

Store escape. Storing an arena pointer into a longer-lived data structure:

type CacheEntry = { key: StringView, value: StringView };

fn cache_insert_bad(cache: &Cache, arena: &Arena, k: &[u8], v: &[u8])
{
    let key   = arena.alloc_str(k);
    let value = arena.alloc_str(v);
    cache.insert({ key, value });
    // ERROR: Cache lives longer than this arena.
    // Store escape: arena-scoped pointer into long-lived container.
}

Use-after-reset. The Z3 epoch tracker catches reads across a reset() boundary in debug builds. By the time you run your test suite, you know exactly which pointer was read from a freed region, and which reset() made it stale.

Together, these three checks eliminate the entire category of use-after-free bugs for arena-allocated memory. No runtime tooling needed. No Valgrind, no ASAN, no Miri. The compiler and the solver prove it before the program executes one instruction.

When arenas do not work

Arenas are not a universal memory solution. Two patterns require a different approach.

Arbitrary graph structures with independent lifetimes. An arena is a region; all objects in it share the same lifetime. If you have a graph where nodes are created and destroyed independently—a scene graph in a game, a DOM tree in a browser—one arena per node defeats the purpose (you might as well use malloc), and one arena for everything means you never reclaim memory until the graph is destroyed entirely. For these cases, Salt provides separate per-component allocators. The component that owns the graph manages its own arena hierarchy. If a graph needs fine-grained deallocation, you can use a freelist allocator wrapped in a #[may_dangle] contract that asserts the freed node is no longer referenced.

Long-lived caches that span request boundaries. A connection pool or a DNS cache lives for the duration of the process. Storing arena-allocated data in these caches is a store-escape violation by design. The answer is a separate, GC-like collector for the cache region—but with a key difference: the collector is scoped to the cache and runs only when the cache is accessed, never during latency-sensitive code paths. Salt provides a gc::Region type for this purpose, with explicit mark-or-sweep boundaries and Z3 contracts that prove no pointer from the cache region escapes into request-handling code.

type DnsCache {
    arena: gc::Region,
    entries: HashMap<String, IpAddr>,
}

fn lookup(cache: &DnsCache, host: &[u8]) -> Option<IpAddr>
    ensures(result.is_none() || result.is_some())
{
    return cache.entries.get(host).copied();
    // IpAddr is Copy; no pointer escapes the cache region.
}

For the remaining cases, Salt offers unsafe blocks with Z3 contracts. The contract formalizes the safety invariant; the programmer attests it; Z3 checks that the invariant is not violated by the code within the block. This is the same mechanism as in the zero-cost safety post, applied to memory management rather than array bounds.

Comparison with Rust

Rust’s borrow checker proves that every reference is valid. Salt’s arena model proves that every arena-allocated pointer is valid for the lifetime of its region. The two approaches provide equivalent safety for the common case. The difference is where the complexity lives.

In Rust, you write lifetime annotations on function signatures, struct definitions, and impl blocks. The compiler checks that your annotations are consistent with the code. When the annotations are wrong, you get an error with a detailed explanation—and a suggestion for the fix. This works, and it works well. But it requires that you think about lifetimes all the time, even when your data has a simple, region-shaped lifetime.

In Salt, you write no lifetime annotations. The compiler infers scopes from the arena declaration and the function body. The scope ladder enforces the same constraints that Rust’s borrow checker enforces, but without the syntax. The trade is that Salt’s model works best when your allocation pattern is arena-shaped: allocate in bulk, free in bulk. When it is not arena-shaped, you need a separate mechanism.

Rust can do arena allocation too, using crates like bumpalo or typed-arena. But Rust’s borrow checker does not understand arenas natively. Using bumpalo in Rust means working with lifetime parameters that thread through every function that touches arena memory. The arena is not a first-class concept; it is a library that the borrow checker treats as opaque. In Salt, the arena is part of the type system. The compiler knows what an arena is, knows when a pointer came from one, and knows when a reset() would invalidate a reference.

Rust is the right language for projects that need the full power of individual-lifetime tracking across diverse allocation patterns. Salt is the right language for projects that work in request-response or frame-at-a-time patterns—servers, kernels, game engines, network stacks—where allocation is batch-shaped and the annotation burden of individual lifetimes would be pure overhead.

What this taught

Building the scope ladder forced a rethink of memory safety. The goal was eliminating lifetime annotations. The result is a system that is not only annotation-free but also catches bugs that Rust’s borrow checker does not: use-after-reset across reset() boundaries (tracked by epoch), store-escape into arbitrarily nested containers (tracked by transitive scope propagation), and cross-region pointer leaks (tracked by Z3).

The lesson is not that lifetime annotations are bad. The lesson is that matching the memory model to the allocation pattern—region-shaped allocation gets a region-shaped safety model, tree-shaped allocation gets a borrow checker, and graph-shaped allocation gets a separate collector—produces a language where each pattern pays only for what it needs.

Salt is open source. The compiler is written in Rust and produces native arm64 and x86-64 binaries through MLIR and LLVM.

git clone https://github.com/bneb/lattice.git
cd lattice
make build              # Build the compiler
make test               # Run the test suite
cat docs/tutorial/arena.salt  # See arena allocation in action

The tutorial walks through building a request handler with arena allocation from scratch. The benchmark methodology compares bump allocation against malloc/free across request sizes. Everything is at github.com/bneb/lattice.