2026-07-21T09:37:41Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4366 2024-03-06T10:34:57Z ddc:004 open_access

A Theory of Partitioned Global Address Spaces Calin, Georgel Derevenetc, Egor Majumdar, Rupak Meyer, Roland PGAS SC preservation Robustness Semantics Formal languages Partitioned global address space (PGAS) is a parallel programming model for the development of high-performance applications on clusters. It provides a global address space partitioned among the cluster nodes, and is supported in programming languages like C, C++, and Fortran by means of APIs. Our first contribution is a formal model for the semantics of single program, multiple data programs that use PGAS APIs. Our model reflects the main features of popular real-world APIs such as SHMEM, ARMCI, GASNet, GPI, and 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 synchronizations between reads and writes. As a second contribution, we propose 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. Our main technical result is an algorithm for checking robustness of PGAS programs. The algorithm makes use of two insights. We first 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. We then 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 streaming fashion. Altogether, we prove that the robustness problem is PSPACE complete. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Georgel Calin and Egor Derevenetc and Rupak Majumdar and Roland Meyer 2013 Is Part Of LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2013.127 urn:nbn:de:0030-drops-43665 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.127 eng https://creativecommons.org/licenses/by/3.0/legalcode