TLA+ specification of PCR parallel programming pattern

Abstract

Programming correct parallel software in a cost-effective way is a challenging task requiring a high degree of expertise. The PCR pattern aims at expressing computations consisting of a producer consuming input data items and generating for each of them, a data set to be consumed by several consumers working in parallel. Their outputs are finally aggregated back into a single result by a reducer. PCR emphasize the independence between different computations in order to expose all opportunities for parallelism. Here, we formalize the semantics of PCR in terms of TLA+. In this way, we can leverage TLA+ related tools to prove properties.