Tesis:
A General Framework for Static Resource Analysis and Profiling of (Parallel) Programs and an Application to Runtime Checking
- Autor: KLEMEN, Maximiliano
- Título: A General Framework for Static Resource Analysis and Profiling of (Parallel) Programs and an Application to Runtime Checking
- Fecha: 2020
- Materia: Sin materia definida
- Escuela: E.T.S DE INGENIEROS INFORMÁTICOS
- Departamentos: LENGUAJES Y SISTEMAS INFORMATICOS E INGENIERIA DE SOFTWARE
- Acceso electrónico: http://oa.upm.es/66526/
- Director/a 1º: LÓPEZ GARCÍA, Pedro
- Resumen: The goal of static cost analysis is to automatically estimate the resources used by program executions without running the programs with concrete data, as functions of input data sizes and possibly other (environmental) parameters. In this thesis we improve and extend state-of-the-art static cost analysis techniques by developing a novel, general and flexible framework for resource usage analysis that can be easily instantiated to infer a wide range of resources, notions of costs, and approximations, which can deal with different programming languages, platforms and execution models. For some applications, standard resource analyses, which estimate the total resource usage of a program, do not provide the information required. For example, helping developers make resource-related design decisions requires knowing how such total resource usage is distributed over selected parts of a program. The novel, general, and flexible framework developed in this thesis solves this problem, by allowing setting up cost relations that can be instantiated for performing a wide range of resource usage analyses, including both static profiling and the standard notion of cost. We show how to instantiate such framework to perform static profiling of accumulated cost (also parameterized by input data sizes). Such information identifies the parts of the program that have the greatest impact on the total program cost. In addition, parallel computing has become the dominant paradigm in computer architecture, and predicting resource usage on such platforms poses a difficult challenge. We address it by extending and instantiating our general framework for performing resource usage analysis of parallel (logic) programs. Besides cost functions, the analysis also infers other meaningful information to better exploit and assess the potential and actual parallelism of a system. We also develop a novel application of our cost analysis framework: inferring static performance guarantees for programs with run-time checks. Instrumenting programs for performing run-time checking of properties, such as regular shapes, is a common and useful technique that helps programmers detect incorrect program behaviors. However, such run-time checks inevitably introduce run-time overhead (in execution time, memory, energy, etc.). We propose a method that uses static analysis to estimate such overhead. This approach can provide guarantees for all possible execution traces, and allows assessing how the overhead grows as the size of the input, which is a parameter of the estimated cost functions, grows. Our method also extends an existing assertion verification framework to express “admissible” overheads, and statically and automatically checks whether the instrumented program conforms with such specifications. The applicability of our techniques strongly depends on the capabilities of the component in charge of solving (or safely approximating) the cost and size recurrence relations generated during the analysis, which has some limitations. In this thesis we address such a challenge, proposing a novel approach for solving arbitrary, constrained recurrence relations, which extends traditional recurrence solvers. It is a guess and check approach that uses well-known machine learning techniques for the guess stage, and a combination of an SMT-solver and a Computer Algebra System for the check stage. Additionally, we develop a method for solving cost relations involving a maximization operator, which appears when representing complex size and cost relations. Finally, we report on the implementation of the techniques developed in this thesis within the CiaoPP system and their experimental evaluation, obtaining encouraging results. ----------RESUMEN---------- El objetivo del análisis estático de coste es estimar automáticamente los recursos utilizados por los programas sin ejecutarlos con datos concretos, en forma de funciones de los tamaños de las entradas. En esta tesis mejoramos y ampliamos las técnicas de análisis estático de coste actuales, desarrollando un marco novedoso, general y flexible de análisis, 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 análisis de coste estándar no proporcionan la información 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 análisis, incluyendo tanto el perfilado estático como el coste estándar. Mostramos cómo instanciar dicho marco para realizar un perfilado estático del coste acumulado (también paramétrico respecto a tamaños), que identifica las partes del programa que tienen mayor impacto en el coste total. Por otra parte, la computación paralela se lia convertido en el paradigma de arquitectura dominante, y predecir el uso de recursos en dichas plataformas plantea un difícil reto. Para abordarlo, extendemos e instanciamos nuestro marco general para estimar el coste de programas (lógicos) paralelos. Adicionalmente, el análisis infiere información significativa para explotar y evaluar mejor el paralelismo potencial y real de un sistema. También desarrollamos una novedosa aplicación de nuestro análisis de coste: la inferencia estática de garantías de rendimiento para programas que usan la técnica de comprobación de propiedades en tiempo de ejecución. Dicha técnica se usa comúnmente 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 utilizamos nuestro análisis estático para estimar dichas sobrecargas, proporcionando garantías para todas las posibles ejecuciones, además de evaluar cómo crece la sobrecarga en función del tamaño de la entrada. Asimismo, extendemos un marco de verificación de aserciones existente para permitir expresar una sobrecarga admisible, y comprobar estáticamente si el programa instrumentado se ajusta a ella. La aplicabilidad de nuestras técnicas de análisis 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, desarrollamos un método para resolver recurrencias que contienen un operador de maximization, que surgen al representar relaciones complejas de tamaño y coste. Por último, describimos 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.