GoKawiilTracking 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 N s and measure the time:
0s 2s 4s 6s 8s 10s 12s 0 500 1000 1500 2000 N execution 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).
... continue reading