Understanding Lua's Garbage Collection -- Towards a Formalized Static Analyzer

TL;DR

This paper formalizes Lua's garbage collection semantics, including finalizers and weak tables, and introduces LuaSafe, a prototype static analyzer to ensure programs' safety from GC-related issues.

Contribution

It provides a mechanized, formal model of Lua's GC, including features not documented, and develops LuaSafe, a static typechecker to prevent GC-related program dangers.

Findings

Mechanized model validated through experimentation

Proved soundness properties of the GC model

LuaSafe effectively typechecks programs for GC safety

Abstract

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.