De cuadrático a lineal: cómo Soteria Rust usa el GC de OCaml para recolectar basura en Rust

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

Soteria Rust, una herramienta de ejecución simbólica para verificar programas Rust, sufría un rendimiento cuadrático en bucles simples. El problema estaba en su implementación de Tree Borrows, un modelo de aliasing avanzado. Al analizar el código, descubrieron que los nodos del árbol crecían innecesariamente debido a las reborrows implícitas en las llamadas a métodos. La solución fue sencilla: dado que Soteria está escrita en OCaml, delegaron la recolección de basura de los nodos inalcanzables al GC de OCaml. Con solo 40 líneas de código, lograron una aceleración de hasta 10x, pasando de tiempo cuadrático a lineal.