Back to Blog

Tracking Rust's aliasing model can be quadratically expensive if done naively. Learn how we fixed this in Soteria Rust by doing meta garbage collection.

Soteria Rust is a symbolic execution tool for verifying Rust programs; it explores every execution path, catching undefined behaviour, aliasing errors, and more. We recently noticed something odd: a simple loop that increments a variable N times was taking quadratic time in N!

The culprit was our implementation of Tree Borrows , Rust’s latest and most advanced aliasing model. The fix ended up being surprisingly simple: because Soteria is written in OCaml, we can delegate the garbage collection of Tree Borrows’ state to OCaml’s garbage collector. In about 40 lines of code, we went from quadratic to linear time, with up to a 10x speedup!

Let’s look into how we found the issue, and how we fixed it.

Let’s look at the example that made us notice the problem: a simple benchmark in which we take a mutable reference r, read it once (into _old), reset it to zero, and then increment it N times in a loop, asserting that the result is indeed N.

fn loop_incr<const N: u32>(r: &mut u32) {
	let _old = *r;
	*r = 0;
	for _ in 0..N {
		*r += 1;
	}
	assert_eq!(*r, N);
}

Let’s run this with a few different Ns and measure the time:

Quadratic growth, for a linear increment… Hm. Looking at the execution time for N=1000, of the 3.02 seconds, 2.62 seconds (87%) are spent in our Tree Borrows implementation.

Tree Borrows was one of the first things I implemented in Soteria Rust, in ancient times (April 2025). It is designed to give rules for aliasing in unsafe Rust, where the borrow checker cannot help you, providing rules one must follow when manipulating raw pointers. This in turn allows for more optimisations in the compiler, at the cost of more ways to trigger undefined behaviour  (UB).

The important thing to know about Tree Borrows here is that it tracks the relationship between all references (and pointers) taken to a location in memory with a tree. Every reborrow (deriving a reference from another, e.g. with a field access) induces a new node in the tree, and every access to memory (each read or write) requires updating the state of all nodes in the tree.

That state is the heart of the model: each reference is in one of five states, and each access moves it along a state machine. The state machine has changed quite a bit since the original paper, but for the sake of presentation let’s look at the original one:

For instance, &mut T starts in the Reserved state, and &T starts in the Frozen state. The arrows between states are transitions that happen on accesses to memory; if a reference’s state ever reaches the ↯ on the right, it means that the program has UB, and has violated Rust’s aliasing rules. The symbols by the arrows tell us under what condition we can transition from one state to another. R is on reads, W is on writes, and ↓ is for local accesses while ↑ is for foreign accesses.

Because we track references in a tree, an access is local if it happens on that reference, or on a reference that was reborrowed from it (so a child node). An access is foreign otherwise. Looking at the state machine, the only way to reach UB (↯) is thus through a local access (↓); remember this for later.

Adding some debugging to the Tree Borrows access function, we can see that by the end of the loop there is a tree that has 9,010 nodes, and that is being accessed 10,012 times. However, the loop only accesses r: &mut u32 a constant number of times per iteration, so what’s happening?

An important consideration when doing code analysis is that we cannot enable optimisations, because they may rely on the absence of UB, and may erase it. Our tool wants to be able to detect UB, so that’s a no-go. Function inlining? Hides UB. Unused variable elimination? Hides UB. Statement reordering? Hides UB. We have to work with unoptimised code, which is often much less efficient, and lengthier, than optimised code.

To illustrate, this is the code generated by the Rust compiler  for this program, with the optimisation level set to 1:

fn loop_incr<const N: u32>(r: &mut u32) {
	let _old = *r;
	*r = 0;
	for _ in 0..N {
		*r += 1;
	}
	assert_eq!(*r, N);
}

pub fn main() {
	loop_incr::<1000>(&mut 0);
}
example::main::h98dd2dc58b240508:
	ret

The compiler is clever enough to show that this function is a no-op (the assertion never fails), and completely erases it! However, this is only true because the Rust type system promises that the mutable reference is non-null, well-aligned, and points to initialised and writeable memory.

So optimisations are out of the question. Let’s instead look at the MIR without optimisations , Rust’s intermediate language that Soteria Rust runs on. We can see the <Range as Iterator>  calls that the for-loop desugars into (lines 6 and 11 below). These supposedly always get inlined (this is Rust’s zero-cost abstraction promise!), but without optimisations they persist.

1 
fn loop_incr(_1: &mut u32) -> () {
2 
	bb0: {
3 
		_2 = copy (*_1);
4 
		(*_1) = const 0_u32;
5 
		_4 = std::ops::Range::<u32> { start: const 0_u32, end: const N };
6 
		_3 = <std::ops::Range<u32> as IntoIterator>::into_iter(move _4) -> [return: bb2, unwind continue];
7 
	}
8
9 
	bb2: {
10 
		_7 = &mut _3;
11 
		_6 = <std::ops::Range<u32> as Iterator>::next(copy _7) -> [return: bb3, unwind continue];
12 
	}
13
14 
	...
15 
}

This gives us a hint as to what is actually happening: this overgrown tree isn’t caused by r, but by the Range object being iterated over.

On each iteration, the tree grows by A nodes, and is accessed B times. This means in total there are roughly A * B * N² node accesses, which is quadratic in N! If you want the exact numbers, expand the details below; it turns out the 9,010 nodes and 10,012 accesses we measured earlier are unfortunately exactly what we expect to see.

The Boring Details and Maths

New nodes are created on reborrows, which happen implicitly in 1. function calls, 2. before method calls on the receiver (this is autoref ), and 3. on field accesses. If we dig deeper, we find the following reborrows in the stack:

Every function call to <Range as Iterator>::next thus adds 9 nodes to the tree at the range’s location, which is called N + 1 times. Adding the root node to the tree, this gives us 9 * (N + 1) + 1 = 9N + 10 nodes by the end of the function, which matches the 9,010 nodes we saw for N=1000.

Looking at the code, we also see:

  • the initial borrow of the Range accesses the tree twice, as it has two fields – so 2 tree accesses total
  • each call to next does 10 accesses to the tree when it returns Some(_), and 8 otherwise – 2 + 10N + 8, for the N iterations and the final None return
  • the tree gets accessed two last times when the Range goes out of scope – 2 + 10N + 8 + 2 = 10N + 12

For N=1000, this gives us 10,012 accesses to the tree, which matches what we saw earlier too!

This explains the quadratic growth. The tree grows by A=9 nodes per iteration, and is accessed B=10 times per iteration. So for N iterations, we have 1/2 * 9 * 10 * N² = 45N² node accesses, which is quadratic in N (the 1/2 is because the tree grows linearly, so it is half-grown on average.)

So we should track these 9,010 nodes, but that seems like a lot of work. Can we avoid this? Luckily, the answer is yes! Sort of. In the best cases. And the justification is back in the state machine of Tree Borrows.

If we look more closely at the structure of the tree in our code example, we have something that looks like this, which matches the calculations we did earlier:

Structure of the Tree Borrows tree

Structure of the Tree Borrows tree

The important thing to notice is that each branch created by each iteration is independent; those references are created from the root, which is the variable storing the Range object.

As we saw earlier, the only way for a node to reach UB is a local access. But once an iteration is done, its branch is unreachable: no live references point to it, so nothing can perform a local access on it. Those nodes can thus never contribute to UB, and we can safely drop them from the tree once we know they aren’t reachable!

Extra soundness justifications

For those familiar with Tree Borrows, I brushed over some details here. So here are the last few justifications to show this is sound!

  • UB can actually be reached through foreign accesses when a reference is protected, which happens on function entry (it is unprotected at function exit). Garbage collecting a protected node could thus cause us to miss UB!

    Luckily for us, our interpreter keeps these references in a variable throughout the scope of the function to be able to release the protectors. This means we keep a strong reference to them, and they can’t be GCed.

  • What if some intermediate node gets GCed, but its children are still reachable? Then a local access would also be possible, and we would miss UB!

    Fortunately, due to the way the state machine is structured and reborrows work, we know a child is always at least as close to UB as its parent. Any UB the parent would cause, the child would cause too. Getting rid of the parent is thus safe, as it can’t cause more UB than the child.

    The way we organise the data structure to enable intermediate nodes to be GCed is that the tree is represented as a weak map from nodes to a set of weak nodes, which are all of that node’s ancestors, not just its parent. If an intermediate node is GCed, all its descendants lose it as an ancestor, but they still hold every other ancestor directly, so local/foreign relationships remain intact.

  • What about symbolic execution? Couldn’t this GC mechanism erase references that aren’t reachable in one execution branch from another branch? This system introduces mutability to state that is shared across parallel execution branches!

    Again, this is naturally avoided by how our interpreter works. We always hold references to the state before a branching point, so if the Tree Borrows node is reachable in the other execution branch, that reference to the state would stop it from being GCed in a branch for which it is unreachable.

    This is technically suboptimal, as it means some branches may need to keep track of references they don’t need, but it is sound and in practice we haven’t seen any issues with this.

A solution would be to implement a garbage collector in our interpreter, which traverses the heap we’re tracking and looks for which tree nodes are still reachable, clearing all the nodes that aren’t. This is however costly, as the heap can grow very large. Traversing it entirely, keeping track of encountered nodes, and then clearing those nodes is a lot of work.

Luckily for us, Soteria Rust is written in OCaml, which comes with its own garbage collector. What if we just re-used that?

Doing this is surprisingly easy! We need to ensure two things:

  1. The OCaml object for a node is held strongly wherever its Rust reference is still in use, so that a node whose reference is live can never be collected. This is already the case.
  2. Our implementation of Tree Borrows holds its nodes weakly: the GC should not consider nodes that are in the tree as impeding garbage collection, since we want them to be collected and removed. To do this, we use a mix of Weak sets  and Ephemeron , two data structures provided by OCaml that hold weak references to their elements.

That’s it! Let’s run it again.

The execution time is now… slower? And the line chart is escaping the graph.

What is happening is that the OCaml garbage collector  runs only periodically, rather than constantly. In our case, Soteria Rust doesn’t allocate much memory, so the garbage collector doesn’t run often. In this example, the garbage collector seems to never run, and we instead have to pay the cost of weak references, which are a bit more expensive to access than strong ones.

Let’s take matters into our own hands. We can’t run the GC constantly, as that would be too costly. We also want to make sure we don’t invoke it when it’s unlikely to be worth it; reborrowing a reference when the tree is small is not a problem.

Furthermore, the OCaml GC is done in two phases: a minor collection, which is fast and collects only the “young” values, and a major collection, which is slower and collects all values. The minor collection is not enough for us, as it will not collect the nodes in the tree that are no longer reachable, so we must force major collections instead, with Gc.major () .

We will run the GC when the tree exceeds size T, a separate parameter for us to play with. We also need to be cautious of cases where the tree grows past size T but the GC doesn’t free any nodes (because all references are held): we don’t want all subsequent accesses to be slowed down by a GC run. Instead, we’ll implement a “backoff” mechanism, where the GC failing to free any nodes will set the next T to 2T.

Let’s run this again; first with T=10, which is the theoretically optimal value for this example, given at most 10 nodes are reachable at any time. We also try it with T=32, 64, 128, 256, 512 to see how it behaves with less frequent GC runs.

Fantastic! The GC is now running, and we have a linear execution time again. Unsurprisingly, T=10 is actually far from optimal, as doing a GC run every 10 nodes is too costly. The best value seems to be T=256, which strikes a good balance between keeping the tree relatively small, and not running the GC too often. For N=1000, the execution time is now 0.54 seconds, which is a 5.6x speedup over the original 3.02 seconds. At N=2000, the speedup is 10.6x! Most importantly, our execution time is now linear in N, rather than quadratic.

We can also look at the improvement directly, by measuring the size of the Range’s tree after each of the 10,012 accesses. Without collection, the tree only ever grows, ending at the 9,010 nodes we predicted earlier. With T=256, we get a sawtooth pattern, growing until the threshold T is reached, where the GC runs and most nodes are collected.

Running this change across other benchmarks, we get mostly positive results; some benchmarks end up being slower, due to the cost of using weak references rather than just having straightforward strong references, but most benchmarks are faster. Importantly, this change avoids quadratic growth in relatively common patterns, so it’s a win!1

An example of performance improvement is on the code below. This snippet was taken from Tokio’s initialisation code , where we were facing some performance issues. We bumped the size of the array from the original 64 to 1024, to stress test it. This benchmark used to take 14.8 seconds; for comparison, a similar (unnamed) tool in this domain takes 15.4 seconds, without tracking Tree Borrows. After this change, it takes 1.7 seconds: an 8.7x speedup!

let arr: [LinkedList<u32>; 1024] = std::array::from_fn(|_| LinkedList {
	head: None,
	tail: None,
	_marker: PhantomData,
});

Varying the size of the array, we get the following results:

Doing garbage collection of Tree Borrows trees is not a new idea; Miri already does it , along with some other tricks  to improve performance. However, in Miri the GC must be implemented manually, since Rust is the host language. Using OCaml enables us to do it much more easily; this change was only about 40 lines of code, and is a neat form of meta garbage collection.

One of the strengths of Soteria Rust, and how we architect code in Soteria, is that we fully leverage the host language. This is one of the key design decisions Sacha, our CTO, took for the Soteria library. We have a shallow OCaml embedding and don’t provide or enforce a unique intermediate language, so the interpreter is highly customisable. It’s what allows us to solve this problem in 40 lines, instead of reimplementing a garbage collector ourselves! It’s always worth knowing your host language well enough to hand it the hard parts.

If you want to learn more about Soteria Rust, check out the documentation and the getting started guide!

1. If Tree Borrows still proves to be prohibitively slow, users can disable it with --ignore-aliasing. ↩


Stay updated

Subscribe to get updates on new features and releases.
This is a very low volume mailing list!