Sobre la especificación y verificación del patrón de programación paralela PCR en TLA+

José E. Solsona

doi:10.36561/ING.24.8

Autores/as

José E. Solsona Universidad ORT Uruguay https://orcid.org/0000-0001-8626-9569

DOI:

https://doi.org/10.36561/ING.24.8

Palabras clave:

Algoritmos paralelos, Patrones de diseño, Métodos formales, TLA

Resumen

Limitaciones físicas en el diseño de microprocesadores han hecho que la industria de computadoras pase de mejorar la velocidad de un solo procesador a aumentar el número de unidades centrales de procesamiento. Pero el diseño de software para explotar la potencia de procesamiento paralelo de manera correcta y efectiva es una tarea desafiante que requiere un alto grado de experiencia. En 2017, Pérez y Yovine propusieron un patrón de programación paralela agnóstico de plataforma llamado PCR, que facilita la escritura de código paralelo. En este trabajo, formalizamos el patrón PCR en términos de TLA+ - un lenguaje de especificación formal para sistemas concurrentes que se está utilizando en lugares como Intel, Amazon y Microsoft. Buscamos proporcionar un marco formal principalmente para (1) expresar diseños PCR de alto nivel y probar su corrección funcional en el sentido de que su computación paralela calcula una función matemática dada, y (2) poder relacionar formalmente diferentes diseños PCR. De esta manera, contribuimos al estado del arte en la verificación formal de programas paralelos aprovechando las herramientas asociadas a TLA+ para probar propiedades sobre algoritmos PCR de alto nivel, como su corrección funcional y refinamiento.

Descargas

Los datos de descargas todavía no están disponibles.

Citas

Asanovic, K. et al; A view of the parallel computing landscape, Commun. ACM, 2009. 52(10) : p. 56–67. DOI: https://doi.org/10.1145/1562764.1562783

Pérez, G. y Yovine, S.; Formal specification and implementation of an automated pattern-based parallel-code generation framework, STTT, 2017. 21(2) : p. 183–202. DOI: https://doi.org/10.1007/s10009-017-0465-2

Lamport, L.; Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, 2002, Addison-Wesley Longman Publishing.

Yu, Y. et al; Model Checking TLA+ Specifications, Correct Hardware Design and Verification Methods, 1999. 1703 : p. 54–66. DOI: https://doi.org/10.1007/3-540-48153-2_6

Cousineau, D. et al.; TLA+ Proofs, FM 2012: Formal Methods, 2012. 7436 : p. 147–154. DOI: https://doi.org/10.1007/978-3-642-32759-9_14

Kuppe, M. et al; The TLA+ Toolbox, ArXiv, 2019. p. 50–62. DOI: https://doi.org/10.4204/EPTCS.310.6

Lamport, L.; The pluscal algorithm language, Theoretical Aspects of Computing-ICTAC, 2009. 5684 : p. 36–60. DOI: https://doi.org/10.1007/978-3-642-03466-4_2