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

Loading...
Thumbnail Image
Date
2021
Authors
Solsona Giossa, José Eduardo
Publisher
Universidad ORT Uruguay
DOI
ISSN
ISBN
URI
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.
En
Thesis note
Desarrollo de Tesis (Master). Universidad ORT Uruguay, Facultad de Ingeniería
Thesis degree name
Master en Ingeniería
352 p. tbls., diagrs., grafs.
Notes
Incluye bibliografía y anexos.
Subject
PROYECTOS-MI, DESARROLLO DE SOFTWARE, ALGORITMO PARALELO, SOFTWARE-DESARROLLO, MÉTODOS FORMALES, TLA+, DISEÑO DE PATRONES
Type
Trabajo final de carrera
Access the full text
Citation
Solsona Giossa, J. E. (2021). On the specification and verification of the PCR parallel programming pattern in TLA+ (Desarrollo de Tesis). Universidad ORT Uruguay, Facultad de Ingeniería.
Rights license