On the specification and verification of the PCR parallel programming pattern in TLA+
DOI:
https://doi.org/10.19153/cleiej.26.1.6Keywords:
Parallel algorithms, Design patterns, Formal Methods, TLAAbstract
Physical limitations in processor design have made computer industry 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 Yovineproposed a platform-agnostic parallel programming pattern called PCR, that eases writing parallel code. In this thesis, we formalize the PCR pattern in terms of TLA+ —a formal specification language for concurrent systems that is being used at places such
as Intel, Amazon and Microsoft. We seek to provide a formal framework mainly for (1) expressing high level PCR designs and prove their functional correctness in the sense that their parallel computation computes a given mathematical function, and (2) being able to formally relate different PCR designs. In this way, we contribute to the state of the art in formal verification of parallel programs by leveraging TLA+-related tools to proving properties about high-level PCR-based algorithms such as their functional correctness and refinement.
Downloads
Published
Issue
Section
License
Copyright (c) 2023 José Solsona
This work is licensed under a Creative Commons Attribution 4.0 International License.
CLEIej is supported by its home institution, CLEI, and by the contribution of the Latin American and international researchers community, and it does not apply any author charges whatsoever for submitting and publishing. Since its creation in 1998, all contents are made publicly accesibly. The current license being applied is a (CC)-BY license (effective October 2015; between 2011 and 2015 a (CC)-BY-NC license was used).