El investigador del Instituto IMDEA Software, Maximiliano Klemen, ha defendido de manera exitosa su tesis doctoral sobre: “A General Framework for Static Resource Analysis and Profiling of (Parallel) Programs and an Application to Runtime Checking”, supervisada por el Prof. Pedro López, el pasado día cinco de marzo.
La tesis de Klemen mejora y amplía las técnicas de análisis estático de coste actuales, desarrollando un marco novedoso, general y flexible de analisis, que puede instanciarse para inferir una amplia gama de recursos, nociones de costes y aproximaciones, así como tratar con diferentes lenguajes de programación y modelos de ejecución.
En algunas aplicaciones, los analisis de coste estandar no proporcionan la informacion requerida. Por ejemplo, para ayudar a los desarrolladores a tomar decisiones de diseño, es necesario saber cómo se distribuye el uso total de recursos entre determinadas partes de un programa. El marco novedoso, general y flexible desarrollado en esta tesis resuelve este problema al permitir establecer relaciones de coste que pueden instanciarse para realizar una amplia gama de analisis, incluyendo tanto el perfilado estatico como el coste estandar. Además, muestra cómo instanciar dicho marco para realizar un perfilado estatico del coste acumulado (tambien parametrico respecto a tamaños), que identifica las partes del programa que tienen mayor impacto en el coste total.
Por otra parte, la computacion paralela se ha convertido en el paradigma de arquitectura dominante, y predecir el uso de recursos en dichas plataformas plantea un difıcil reto. Para abordarlo, extiende e instancia su marco general para estimar el coste de programas (logicos) paralelos. Adicionalmente, el analisis infiere informacion útil para explotar y evaluar mejor el paralelismo potencial y real de un sistema.
Klemen también presenta el desarrollo de una novedosa aplicación en su analisis de coste: la inferencia estatica de garantıas de rendimiento para programas que usan la tecnica de comprobacion de propiedades en tiempo de ejecucion. Dicha tecnica se usa comunmente para detectar comportamientos incorrectos en los programas.
Sin embargo, tales comprobaciones introducen sobrecargas en tiempo de ejecución (en términos de tiempo, memoria, energıa, etc.). En esta tesis utiliza su analisis estatico para estimar dichas sobrecargas, proporcionando garantıas para todas las posibles ejecuciones, ademas de evaluar cómo crece la sobrecarga en funcion del tamaño de la entrada. Así mismo, extendemos un marco de verificación de aserciones existente para permitir expresar una sobrecarga admisible, y comprobar est ́aticamente si el programa instrumentado se ajusta a ella.
La aplicabilidad de nuestras t ́ecnicas de an ́alisis depende fuertemente de las capacidades del componente a cargo de resolver o aproximar relaciones de recurrencia, el cual presenta algunas limitaciones. En esta tesis abordamos dicho reto, desarrollando un enfoque novedoso para resolver relaciones arbitrarias de recurrencia con restricciones, extendiendo los resolutores tradicionales. El nuestro es un enfoque basado adivinar y comprobar, usando técnicas de aprendizaje automático para la fase de adivinar, y una combinación de un resolutor SMT y un sistema de álgebra computacional para la etapa de comprobación. Adicionalmente, desarrolla un método para resolver recurrencias que contienen un operador de maximización, que surgen al representar relaciones complejas de tamaño y coste.
Por último, describe la implementación de las técnicas desarrolladas en esta tesis, integradas en el sistema CiaoPP, así como su evaluación experimental, obteniendo resultados prometedores.
