On the specification and verification of the PCR parallel programming pattern in TLA+
DOI:
https://doi.org/10.36561/ING.24.8Keywords:
Parallel algorithms, Design patterns, Formal Methods, TLAAbstract
Physical limitations in processor design have made the 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 Yovine proposed a platform-agnostic parallel programming pattern called PCR, that eases writing parallel code. In this work, 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
References
Asanovic, K. et al; A view of the parallel computing landscape, Commun. ACM, 2009. 52(10) : p. 56–67.
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.
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.
Cousineau, D. et al.; TLA+ Proofs, FM 2012: Formal Methods, 2012. 7436 : p. 147–154.
Kuppe, M. et al; The TLA+ Toolbox, ArXiv, 2019. p. 50–62.
Lamport, L.; The pluscal algorithm language, Theoretical Aspects of Computing-ICTAC, 2009. 5684 : p. 36–60.
