Semántica operacional y su aplicación para el estudio de recolección de basura, en Lua 5.2

Abstract

Lua es un lenguaje de programación imperativo de scripting, que ofrece tipado dinámico, manejo automático de memoria, facilidades para la descripción de datos, y mecanismos de metaprogramación para adaptar el lenguaje a dominios específicos. Es utilizado en proyectos de diversa naturaleza, desde desarrollo de juegos, de manera notable en juegos “AAA”, desarrollo de plugins, firewall de aplicaciones web, y en sistemas embebidos. Gracias al éxito de Lua es posible encontrar diversas implementaciones alternativas y analizadores estáticos. Sin embargo, la naturaleza informal de la especificación del lenguaje implica que quienes desarrollan esas herramientas no pueden proveer garantías formales de corrección para las mismas. En este trabajo presentamos una formalización de la semántica operacional de Lua 5.2, incluyendo recolección de basura (GC) y sus interfaces (finalizadores y tablas débiles; una forma de implementar referencias débiles). Validamos la semántica mediante su mecanización, utilizando PLT Redex, y el testeo de la misma con respecto a la suite de tests del intérprete oficial de Lua. A su vez, utilizamos las facilidades ofrecidas por PLT Redex para la mecanización de sistemas formales y testeo aleatorio de propiedades, para obtener evidencia de la propiedad de progreso de la semántica. Para GC proveemos un framework para razonar formalmente sobre propiedades de cualquier algoritmo de GC basado en un criterio sintáctico. Dentro del framework podemos formalizar y esbozar la demostración de propiedades sobre GC, incluyendo su corrección (sin considerar sus interfaces). La semántica formalizada y su mecanización podrían ayudar a proveer garantías formales de corrección para herramientas que realicen análisis estático de programas Lua, como también en el prototipado de nuevos conceptos de programación y extensiones para Lua.

Lua is a lightweight imperative scripting language, featuring dynamic typing, automatic memory management, data description facilities, and metaprogramming mechanisms to adapt the language to specific domains. It is extensively used in projects ranging from game development, most notably by “AAA” games, plugin development, web application firewalls, and embedded systems. Thanks to Lua’s success,several alternative implementations and static analyzers can be found in the wild. However, the informal nature of the language’s specification means that developers of those tools cannot provide formal guarantees of correctness for them. In this work we present a formalization of Lua 5.2’s operational semantics, including garbage collection (GC) and its interfaces (finalizers and weak tables; a particular implementation of weak references). We validate our model by mechanizing it, using PLT Redex, and testing it against the test suite of the reference interpreter of Lua. Also, we use the features provided by PLT Redex for the mechanization of formal systems and random testing of properties, to gather evidence for the progress property of the semantics. For GC we provide a framework for formal reasoning of properties of any GC algorithm based on a syntactic criterion. Within the given framework we are able to formalize and sketch the proof of several claims about GC, including its correctness (without its interfaces). The formalized semantics and its mechanization could help to provide formal guarantees of correctness for tools that perform static analysis of Lua programs, as well as for the prototyping of new features and extensions to Lua.