License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2013.127
URN: urn:nbn:de:0030-drops-43665
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4366/
Go to the corresponding LIPIcs Volume Portal

Calin, Georgel ; Derevenetc, Egor ; Majumdar, Rupak ; Meyer, Roland

A Theory of Partitioned Global Address Spaces

pdf-format:
8.pdf (0.7 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{calin_et_al:LIPIcs:2013:4366,
  author =	{Georgel Calin and Egor Derevenetc and Rupak Majumdar and Roland Meyer},
  title =	{{A Theory of Partitioned Global Address Spaces}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{127--139},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-64-4},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{24},
  editor =	{Anil Seth and Nisheeth K. Vishnoi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4366},
  URN =		{urn:nbn:de:0030-drops-43665},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.127},
  annote =	{Keywords: PGAS, SC preservation, Robustness, Semantics, Formal languages}
}

Keywords: PGAS, SC preservation, Robustness, Semantics, Formal languages
Collection: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)
Issue Date: 2013
Date of publication: 10.12.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI