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

Summary

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: 0s2s4s6s8s10s12s0500100015002000Nexecution time (s) 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 ...