Analysis Techniques for Concurrent Programming Languages
Salvador Tamarit Muñoz · 2013
Concurrent languages are increasingly present in our society, both in new technologies and in the systems used on a daily basis.Moreover, given the current systems distribution and their internal architecture, one can expect that this remains so in the coming years.In this context, the development of tools to support the implementation of concurrent programs becomes essential.Futhermore, the behavior of concurrent systems is particularly difficult to analyse, so that any tool that helps in this task, even if in a limited way, will be very useful.For example, one can find tools for debugging, analysis, testing, optimisation, or simplification of programs, which are widely used by programmers nowadays.The purpose of this thesis is to introduce, through various concurrent programming languages, some analysis techniques that can help to improve the experience of the software development and release for concurrent models.This thesis introduces both static (approximating all possible executions) and dynamic (considering a specific execution) analysis.The topics considered here differ enough from each other to be fully independent.Nevertheless, they have a common link: they can be used to analyse properties of a concurrent programming language.All the analyses presented here have been formally defined and their correctness have been proved, ensuring that the results will have the reliability degree which is needed for some systems (for instance, for critical systems).It also includes a description of the software tools that implement the different ideas proposed.This gives the work a usefulness well beyond the theoretical aspect, allowing us to put it in practice and to test the different analyses with real-world examples.v All the ideas here presented are, by themselves, approaches that can be applied in many current contexts and problems.Moreover, individually they serve as a starting point for other derived analysis, as well as for the adaptation to other languages of the same family.This gives an added value to this work, a fact confirmed by some later works that are already benefiting from the results obtained in this thesis.vi Resumen Los lenguajes concurrentes están cada día más presentes en nuestra sociedad, tanto en las nuevas tecnologías como en los sistemas utilizados de manera cotidiana.Más aún, dada la actual distribución de los sistemas y su arquitectura interna, cabe esperar que este hecho siga siendo una realidad en los próximos años.En este contexto, el desarrollo de herramientas de apoyo a la implementación de programas concurrentes se vuelve esencial.Además, el comportamiento de los sistemas concurrentes es especialmente difícil de analizar, por lo que cualquier herramienta que ayude en esta tarea, aún cuando sea limitada, será de gran utilidad.Por ejemplo, podemos encontrar herramientas para la depuración, análisis, comprobación, optimización, o simplificación de programas.Muchas de ellas son ampliamente utilizadas por los programadores hoy en día.El propósito de esta tesis es introducir, a través de diferentes lenguajes de programación concurrentes, técnicas de análisis que puedan ayudar a mejorar la experiencia del desarrollo y publicación de software para modelos concurrentes.En esta tesis se introducen tanto análisis estáticos (aproximando todas las posibles ejecuciones) como dinámicos (considerando una ejecución en concreto).Los trabajos aquí propuestos difieren lo suficiente entre sí para constituir ideas totalmente independientes, pero manteniendo un nexo común: el hecho de ser un análisis para un lenguaje de programación concurrente.Todos los análisis presentados han sido definidos formalmente y se ha probado su corrección, asegurando que los resultados obtenidos tendrán el grado de fiabilidad necesario en sistemas que lo requieran, como por ejemplo, en sistemas críticos.Además, se incluye la descripción de las herramientas software que implementan las diferentes ideas propuestas.Esto le da al trabajo una utilidad más allá del marco teórico, permitiendo poner en práctica y probar con ejemplos reales los diferentes análisis.vii Todas las ideas aquí presentadas constituyen, por sí mismas, propuestas aplicables en multitud de contextos y problemas actuales.Además, individualmente sirven de punto de partida para otros análisis derivados, así como para la adaptación a otros lenguajes de la misma familia.Esto le da un valor añadido a este trabajo, como bien atestiguan algunos trabajos posteriores que ya se están beneficiando de los resultados obtenidos en esta tesis.viii Resum Els llenguatges concurrents estan cada dia més presents en la nostra societat, tant a les noves tecnologies com en els sistemes utilitzats de manera quotidiana.Encara més, donada l'actual distribució dels sistemes i la seva arquitectura interna, cal esperar que aquest fet segueixi sent una realitat en els propers anys.En aquest context, el desenvolupament d'eines de suport a la implementació de programes concurrents es torna essencial.A més, el comportament dels sistemes concurrents és especialment difícil d'analitzar, pel que qualsevol eina que ajudi en aquesta tasca, tot i que sigui limitada, serà de gran utilitat.Per exemple, podem trobar eines per a la depuració, anàlisi, comprovació, optimització, o simplificació de programes.Moltes d'elles són àmpliament utilitzades pels programadors avui en dia.El propòsit d'aquesta tesi és introduir, a través de diferents llenguatges de programació concurrents, tècniques d'anàlisi que puguin ajudar a millorar l'experiència del desenvolupament i publicació de software per a models concurrents.En aquesta tesi s'introdueixen tant anàlisis estàtics (aproximant totes les possibles execucions) com dinàmics (considerant una execució en concret).Els treballs aquí proposats difereixen prou entre si per constituir idees totalment independents, però mantenint un nexe comú: el fet de ser un anàlisi per a un llenguatge de programació concurrent.Tots els anàlisis presentats han estat definits formalment i s'ha provat la seva correcció, assegurant que els resultats obtinguts tindran el grau de fiabilitat necessari en sistemes que ho requereixin, com per exemple, en sistemes crítics.A més, s'inclou la descripció de les eines software que implementen les diferents idees propostes.Això li dóna al treball una utilitat més enllà del marc teòric, permetent posar en pràctica i provar amb exemples reals els diferents anàlisis.ix Totes les idees aquí presentades constitueixen, per si mateixes, propostes aplicables en multitud de contextos i problemes actuals.A més, individualment serveixen com a punt de partida per a altres anàlisis derivats, així com per a l'adaptació a altres llenguatges de la mateixa família.Això li dóna un valor afegit a aquest treball, com bé testifiquen alguns treballs posteriors que ja s'estan beneficiant dels resultats obtinguts en aquesta tesi.x