Разработчики инструмента символьного выполнения Soteria Rust заметили, что простой цикл, инкрементирующий переменную N раз, работает за квадратичное от N время. Тормозил модуль Tree Borrows — самая свежая модель алиасинга в Rust. Решение уместилось в 40 строк: поскольку Soteria написан на OCaml, сборку мусора состояния Tree Borrows передали встроенному GC. В результате время стало линейным, а ускорение достигло 10x.
Проблему показал бенчмарк loop_incr, где на N=1000 из 3,02 секунд 87% уходило на Tree Borrows. Модель строит дерево связей ссылок и указателей: каждый реборроу добавляет узел, а каждое чтение или запись обновляет все узлы. В неоптимизированном MIR цикл for разворачивается в вызовы итератора Range, создавая на каждой итерации 9 новых узлов и 10 проходов по дереву — в сумме около 45·N² операций. Однако ветки, оставшиеся от завершённых итераций, становятся недостижимыми: локальный доступ к ним невозможен, а значит, они не могут вызвать неопределённое поведение. Такие узлы можно удалять.
В OCaml объект узла держится по сильной ссылке там, где он нужен интерпретатору, а в дереве хранится слабо — через Weak-множества и Ephemeron. Когда размер дерева превышает порог T, принудительно вызывается полная сборка Gc.major(). Если GC не высвобождает узлы, порог удваивается. Лучший баланс дал T=256: без сборки дерево росло до 9010 узлов, а с GC пилообразно колебалось, не превышая порог. На примере инициализации большого массива LinkedList, взятого из Tokio, время упало с 14,8 до 1,7 секунд — ускорение в 8.7 раз, быстрее аналога, вовсе не отслеживающего Tree Borrows.
В Miri аналогичную очистку реализуют вручную на Rust. Soteria же пользуется тем, что написан на OCaml: идея CTO Саши максимально задействовать хост-язык позволила получить «мета-сборщик мусора» за 40 строк. Если Tree Borrows всё равно тормозит, его можно отключить флагом --ignore-aliasing.