Lobsters | 📄 原文链接 | 2026-07-22 collected

元垃圾回收：用 OCaml 的 GC 回收 Rust 的借用状态树

source: soteria-tools.com — 2026-07-20

概述

Soteria Rust 是一个用 OCaml 编写的 Rust 符号执行验证工具。开发团队发现一个简单的循环递增基准测试在 N 增大时呈二次方时间增长——罪魁祸首是 Tree Borrows 实现的状态树节点未清理。修复方案惊人地简洁：因为 Soteria 本身用 OCaml 编写，可以直接委托 OCaml 的 GC 回收 Tree Borrows 的状态数据。约 40 行代码，从 O(n2) 降至 O(n)，获得高达 10 倍加速。文章详细展示了 Tree Borrows 的状态机和未优化 Rust 代码的膨胀问题。

核心要点

  • Soteria Rust 的 Tree Borrows 实现中，状态树节点未释放导致 N=1000 时树有 9010 个节点，遍历开销呈二次方增长。
  • 修复方案：利用 OCaml 的 GC 自动回收 Tree Borrows 状态数据——约 40 行代码从 O(n2) 降至 O(n)。
  • Tree Borrows 是 Rust 最新的 别名分析模型，每个 reborrow 创建新节点，每次内存访问需更新所有节点状态。
  • 关键约束：符号执行工具不能启用编译器优化——函数内联、死代码消除等优化会 隐藏 UB。

金句

In about 40 lines of code, we went from quadratic to linear time, with up to a 10x speedup!
back to Lobsters