On the specification and verification of the PCR parallel programming pattern in TLA+

Abstract

Las limitaciones físicas en el diseño de procesadores han hecho que la industria informática desde 2005 pasara de mejorar la velocidad de un solo procesador a aumentar el número de unidades de proceso. Un diseño de software que explote la potencia de procesamiento paralelo de forma correcta y efectiva es una tarea desafiante que requiere un alto grado de experiencia. En 2017, Pérez y Yovine propusieron una herramienta basada en patrones de diseño para facilitar el desarrollo de software paralelo. En particular, la herramienta está basada en un patrón de programación paralela, agnóstico de la plataforma, denominado PCR, que describe las computaciones realizadas en forma concurrente por Productores, Consumidores y Reductores que se comunican entre sí. Este combina en un único patrón componible varios conceptos como operaciones colectivas, programación basada en flujos, iteración no acotada y recursividad. En la presente tesis se formaliza la semántica del patrón PCR en términos de TLA+. De esta manera, se puede aprovechar las herramientas asociadas a TLA+ para demostrar las propiedades de diseños de PCR de alto nivel, tales como su corrección funcional y refinamientos entre diferentes diseños de PCR. TLA+ es un lenguaje de especificación formal para sistemas concurrentes que se está utilizando en lugares como Intel, Amazon y Microsoft. Se contribuye al estado del arte en los refinamientos de programas paralelos a partir de modelos abstractos, especialmente utilizando una caracterización alternativa del patrón PCR general y el framework TLA+. La investigación que da origen a los resultados presentados en la presente tesis, recibió fondos de la Agencia Nacional de Investigación e Innovación bajo el código POS NAC 2018 1 152201.