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

Abstract

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.