A Theory of Partitioned Global Address Spaces

Partitioned global address space (PGAS) is a parallel programming model for the development of high-performance software for clusters. It provides with a global address space made up of the memories of multiple cluster nodes. This programming model is supported by several PGAS APIs: SHMEM, ARMCI, GASNet, GPI, GASPI.

A key feature of PGAS is the support for one-sided communication: a node may directly read and write the memory located at a remote node, without explicit synchronization with the processes running on the remote side. One-sided communication increases performance by decoupling process synchronization from data transfer, but requires the programmer to reason about appropriate synchronization between reads and writes.

In the talk I will define and investigate robustness, a criterion for correct synchronization of PGAS programs. Robustness corresponds to acyclicity of a suitable happens-before relation defined on PGAS computations. The requirement is finer than classical data race freedom and rules out most false error reports.

I will present a novel algorithm for checking robustness of PGAS programs. The algorithm makes use of two insights. First, we show that, if a PGAS program is not robust, then there are computations in a certain normal form that violate happens-before acyclicity. Intuitively, normal-form computations delay remote accesses in an ordered way. Then, we devise an algorithm that checks for cyclic normal-form computations. Essentially, the algorithm is an emptiness check for a novel automaton model that accepts normal-form computations in a streaming fashion. Altogether, we prove that the robustness checking problem is PSPACE-complete.

The talk presents joint work with Georgel Calin, Rupak Majumdar, and Roland Meyer.