分代垃圾收集器的验证
Verification of a Generational Garbage Collector
浏览论文内容
中文总结 AI 辅助
本文在Rocq+VST中形式化验证了一个支持可变引用、兼容OCaml数据类型的C语言多代垃圾收集器，其模块化API规范独立于实现细节，并通过验证客户端程序证明了规范的充分性。
中文摘要 AI 辅助
我们使用Rocq+VST形式化验证了一个支持可变引用的多代垃圾收集器，该收集器用C语言编写，并与OCaml数据类型兼容。其精心规范的API支持C程序或CertiRocq（一个从Rocq到C的已验证编译器）生成的程序，其接口与OCaml收集器的接口类似。我们通过验证客户端程序，证明了我们的API规范对于修改器（垃圾收集器的客户端）的充分性。我们的程序和验证是模块化的，因此（1）API规范独立于实现（例如，复制与标记-清除、分代与非分代的选择），并且（2）实现组件（如转发函数）的规范和验证独立于其他组件（例如，关于老年代、多线程或可变引用“记忆集”的设计决策）。
英文摘要
We have formally verified in Rocq+VST a multi-generation collector with support for mutable references, written in C and compatible with OCaml data types. Its carefully specified API supports C programs or CertiRocq (a verified compiler from Rocq to C) is similar to that of OCaml's collector. We have demonstrated the adequacy of our API specification for the mutator (client of the garbage collector) by verifying client programs. Our program and our verification are modular so that (1) the API spec is independent of the implementation (e.g., the choice of copying vs. mark-and-sweep, generational-vs-nongenerational) and (2) the specification and verification of components of the implementation (such as the forwarding function) are independent of other components (e.g., design decisions regarding older generations, multiple threads, or "remembered sets" of mutable references).
发表机构
- Princeton University（普林斯顿大学）
- Shanghai Qi Zhi Institute（上海智源人工智能研究院）
- Heriot-Watt University（赫瑞-瓦特大学）
机构由 AI 辅助整理，请以论文原文为准。
