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

Mostrar todas las versiones(2)

Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2021.

Guardado en:
Detalles Bibliográficos
Autor principal: Soldevila Raffa, Mallku Ernesto
Otros Autores: Fridlender, Daniel Edgardo
Formato: publishedVersion doctoralThesis
Lenguaje:Español
Publicado: 2021
Materias:
Semántica operacional
Acceso en línea:http://hdl.handle.net/11086/19301
Aporte de:
Repositorio Digital Universitario (UNC) de Universidad Nacional de Córdoba
id I10-R141-11086-19301
record_format dspace
institution Universidad Nacional de Córdoba
institution_str I-10
repository_str R-141
collection Repositorio Digital Universitario (UNC)
language Español
topic Semántica operacional
spellingShingle Semántica operacional
Soldevila Raffa, Mallku Ernesto
Semántica operacional y su aplicación para el estudio de recolección de basura, en Lua 5.2
topic_facet Semántica operacional
description Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2021.
author2 Fridlender, Daniel Edgardo
author_facet Fridlender, Daniel Edgardo
Soldevila Raffa, Mallku Ernesto
format publishedVersion
doctoralThesis
author Soldevila Raffa, Mallku Ernesto
author_sort Soldevila Raffa, Mallku Ernesto
title Semántica operacional y su aplicación para el estudio de recolección de basura, en Lua 5.2
title_short Semántica operacional y su aplicación para el estudio de recolección de basura, en Lua 5.2
title_full Semántica operacional y su aplicación para el estudio de recolección de basura, en Lua 5.2
title_fullStr Semántica operacional y su aplicación para el estudio de recolección de basura, en Lua 5.2
title_full_unstemmed Semántica operacional y su aplicación para el estudio de recolección de basura, en Lua 5.2
title_sort semántica operacional y su aplicación para el estudio de recolección de basura, en lua 5.2
publishDate 2021
url http://hdl.handle.net/11086/19301
work_keys_str_mv AT soldevilaraffamallkuernesto semanticaoperacionalysuaplicacionparaelestudioderecolecciondebasuraenlua52
_version_ 1782014939629617152
spelling I10-R141-11086-193012023-08-31T13:17:41Z Semántica operacional y su aplicación para el estudio de recolección de basura, en Lua 5.2 Soldevila Raffa, Mallku Ernesto Fridlender, Daniel Edgardo Ziliani, Beta Semántica operacional Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2021. publishedVersion Fil: Soldevila Raffa, Mallku Ernesto. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. 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. publishedVersion Fil: Soldevila Raffa, Mallku Ernesto. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. 2021-08-04T19:39:38Z 2021-08-04T19:39:38Z 2021 doctoralThesis http://hdl.handle.net/11086/19301 spa Atribución-CompartirIgual 4.0 Internacional http://creativecommons.org/licenses/by-sa/4.0/

Ejemplares similares