Meta Garbage Collection: Using OCaml's GC to GC Rust - Soteria

Back to Blog Meta Garbage Collection: Using OCaml's GC to GC Rust<br>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.

Opale Sjöstedt, Principal Engineer · 20 July 2026<br>RSS<br>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!<br>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 !<br>Let’s look into how we found the issue, and how we fixed it.<br>Finding the Culprit

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.<br>fn loop_incrconst N: u32>(r: &mut u32) {<br>let _old = *r;<br>*r = 0;<br>for _ in 0..N {<br>*r += 1;<br>assert_eq!(*r, N);<br>Let’s run this with a few different Ns and measure the time:<br>0s2s4s6s8s10s12s0500100015002000Nexecution time (s)<br>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.<br>Tree Borrows

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).<br>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.<br>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:

Tree Borrows' state machine<br>by<br>Neven Villani, Johannes Hostert, Derek Dreyer, Ralf Jung

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.<br>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.<br>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.<br>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?<br>Looking at the code

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.<br>To illustrate, this is the code generated by the Rust compiler  for this program, with the optimisation level set to 1:<br>fn loop_incrconst N: u32>(r: &mut u32) {<br>let _old = *r;<br>*r = 0;<br>for _ in 0..N {<br>*r += 1;<br>assert_eq!(*r, N);

pub fn main() {<br>loop_incr::1000>(&mut 0);

example::main::h98dd2dc58b240508:<br>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.<br>So optimisations are out of the...