论文标题
了解Lua的垃圾收集 - 朝着形式化的静态分析仪
Understanding Lua's Garbage Collection -- Towards a Formalized Static Analyzer
论文作者
论文摘要
我们为LUA编程语言提供垃圾收集（GC）的语义。感兴趣的是最终化器（类似于对象的语言中的破坏者）和弱表（特定的弱参考实现）。该模型表达了与GC相关的几个方面，这些方面在LUA的文档中未涵盖，但仍会影响程序的可观察行为。我们的模型是机械化的，可以通过实际程序进行测试。我们的长期目标是提供LUA计划的正式静态分析仪，以发现潜在的危险。作为第一步，我们提供了一种原型工具Luasafe，该工具可以打字程序，以确保其行为不受GC的影响。我们的GC模型在实践中通过其机械化和理论上证明了几种合理性能来验证我们的模型。
We provide the semantics of garbage collection (GC) for the Lua programming language. Of interest are the inclusion of finalizers(akin to destructors in object-oriented languages) and weak tables (a particular implementation of weak references). The model expresses several aspects relevant to GC that are not covered in Lua's documentation but that, nevertheless, affect the observable behavior of programs. Our model is mechanized and can be tested with real programs. Our long-term goal is to provide a formalized static analyzer of Lua programs to detect potential dangers. As a first step, we provide a prototype tool, LuaSafe, that typechecks programs to ensure their behavior is not affected by GC. Our model of GC is validated in practice by the experimentation with its mechanization, and in theory by proving several soundness properties.
