10x Speedup: Meta-Garbage-Collection nutzt OCaml-GC für Rust-Verifikation
Meta Garbage Collection: Using OCaml's GC to GC Rust
Soteria Rust, ein symbolisches Ausführungswerkzeug zur Verifikation von Rust-Programmen, litt unter quadratischer Laufzeit bei einfachen Schleifen. Die Ursache war die naive Implementierung des Tree-Borrows-Aliasing-Modells. Die Lösung: Da Soteria in OCaml geschrieben ist, kann die Garbage Collection des Tree-Borrows-Zustands an den OCaml-GC delegiert werden. Mit etwa 40 Zeilen Code wurde die Laufzeit von quadratisch auf linear reduziert – ein Speedup von bis zu 10x. Der Artikel erklärt die Ursache, die mathematischen Details und die Soundness-Argumente für diese Meta-Garbage-Collection.
Mit etwa 40 Zeilen Code reduzierten wir die Laufzeit von quadratisch auf linear – mit einem Speedup von bis zu 10x!