Analysis of May-Happen-in-Parallel in Concurrent Objects

Abstract

Esta tesis presenta un análisis may-happen-in-parallel (puede-ocurrir-en-paralelo) para lenguajes orientados a objetos y basados en objetos concurrentes. En éste modelo de concurrencia, los objetos son la unidad de concurrencia tal que, cuando un método de un objeto o2 es llamado desde una tarea que se ejecuta en un objeto o1, las instrucciones de la tarea concurrente en o1 pueden ejecutarse en paralelo con las de la llamada (asíncrona) en o2, y con los métodos llamados de forma transitiva. El objetivo del análisis MHP es identificar los pares de instrucciones que puede ejecutarse en paralelo en un programa para cualquier ejecución del mismo. Nuestro análisis está definido como un análisis a nivel de método (local) cuya información se puede componer de forma modular para obtener la información al nivel de la aplicación (global). Se ha demostrado la corrección del análisis, es decir, que sobre-aproxima el paralelismo real de los programas de acuerdo con una semántica bien definida. Se ha implementado un prototipo, dando lugar al sistema MayPar, un analizador may-happen-in-parallel que se puede ser útil para depuración, corrección de errores y para incrementar la precisión de otros análisis que infieran propiedades más complejas (por ejemplo, terminación o análisis de recursos). MayPar se ha probado con múltiples ejemplos, entre ellos dos casos de estudio industriales, y se han alcanzado buenas cotas de precisión y rendimiento. [Abstract] This thesis presents a may-happen-in-parallel (MHP) analysis for object-oriented languages based on concurrent objects. In this concurrency model, objects are the concurrency units such that, when a method is invoked on an object o2 from a task executing on object o1, the statements of the current task in o1 may run in parallel with those of the (asynchronous) call on o2, and with those of transitively invoked methods. The goal of the MHP analysis is to identify pairs of statements in the program that may run in parallel in any execution. Our MHP analysis is formalized as a method-level (local) analysis whose information can be modularly composed to obtain application-level (global) information. The analysis has been proven to be sound, that is, it over-approximates the real parallelism according to a well defined semantics. A prototype implementation has been carried out, resulting in the MayPar system, a may-happen-in-parallel analyzer that can be used for debugging and to increase precision of other analyses which infer more complex properties (e.g., termination and resource consumption). MayPar has been tested on several examples, including two industrial cases studies, achieving good precision and performance.