Título : On the specification and verification of the PCR parallel programming pattern in TLA+
Autor(es) : Solsona, José E.
Fecha de publicación : oct-2021
Tipo de publicación: Tesis de maestría
Versión: Publicado
Supervisor(es) : Tasistro, Alvaro
Yovine, Sergio
Publicado por: Universidad ORT Uruguay
Areas del conocimiento : Ciencias Naturales y Exactas
Ciencias de la Computación e Información
Otros descriptores : Algoritmos paralelos
Patrones de diseño
Métodos formales
Resumen : Physical limitations in processor design have made computer industry since 2005 shift from improving the speed of a single processor to increasing the number of processing core units. But the design of software to exploit parallel processing power in a correct and cost-effective way is a challenging task requiring a high degree of expertise. In 2017, Pérez and Yovine proposed a pattern-based formally grounded tool that eases writing parallel code. In particular, the tool is based on a platform-agnostic parallel programming pattern called PCR, which describes computations performed concurrently by communicating Producers, Consumers and Reducers. It combines in a single and composable pattern several concepts like collective operations, stream programming, unbounded iteration and recursion. In this thesis, we formalize the semantics of the PCR pattern in terms of TLA+. In this way, we can leverage TLA$+ related tools to prove properties about high level PCR designs such as their functional correctness and refinements between different PCR designs. TLA+ is a formal specification language for concurrent systems that is being used at places such as Intel, Amazon and Microsoft. We thus contribute to the state of the art in formal refinement of parallel programs from abstract models, especially starting from an alternative characterization of the general PCR pattern, and utilizing the TLA+ framework. A presentation of the work in progress for this thesis was part of the TLA+ Community Event that was held (virtually) in October 2020 as a satellite of the DISC 2020 Conference.
URI / Handle: https://hdl.handle.net/20.500.12381/489
Otros recursos relacionados: https://hdl.handle.net/20.500.12381/488
Financiadores: Agencia Nacional de Investigación e Innovación
Identificador ANII: POS_NAC_2018_1_152201
Nivel de Acceso: Acceso abierto
Licencia CC: Reconocimiento 4.0 Internacional. (CC BY)
Aparece en las colecciones: Publicaciones de ANII

Archivos en este ítem:
archivo  Descripción Tamaño Formato
2021118-MI-182285.pdfDescargar 3.03 MBAdobe PDF

Las obras en REDI están protegidas por licencias Creative Commons.
Por más información sobre los términos de esta publicación, visita: Reconocimiento 4.0 Internacional. (CC BY)