分区全局地址空间理论
计算机科学中的逻辑
2013-07-26 v1 分布式、并行与集群计算
摘要
分区全局地址空间 (PGAS) 是一种用于在集群上开发应用程序的并行编程模型。它提供了一个在集群节点间分区的全局地址空间，并通过 API 在 C、C++ 和 Fortran 等编程语言中得到支持。在本文中，我们为使用 PGAS API 的单指令多数据 (SIMD) 程序的语义提供了一个形式化模型。我们的模型反映了 SHMEM、ARMCI、GASNet、GPI 和 GASPI 等流行现实世界 API 的主要特征。PGAS 的一个关键特征是支持单边通信：节点可以直接读写位于远程节点的内存，而无需与远程侧运行的进程进行显式同步。单边通信通过将进程同步与数据传输解耦来提高性能，但要求程序员对读写之间的适当同步进行推理。作为第二个贡献，我们提出并研究了鲁棒性 (robustness)，这是 PGAS 程序正确同步的一个准则。鲁棒性对应于在 PGAS 计算上定义的合适“发生在前”(happens-before) 关系的无环性。该要求比经典的数据竞争自由更精细，并排除了大多数错误报告。我们的主要结果是一个检查 PGAS 程序鲁棒性的算法。该算法利用了两个见解。首先，利用组合论证我们表明，如果 PGAS 程序不鲁棒，则存在某种正规形式的计算违反了“发生在前”的无环性。直观地说，正规形式计算以有序方式延迟远程访问。随后，我们设计了一种算法来检查循环的正规形式计算。本质上，该算法是对一种新型自动机模型的空性检查，该自动机模型以流式方式接受正规形式计算。总之，我们证明了鲁棒性问题是 PSpace-完全的。
引用
@article{arxiv.1307.6590,
title = {A Theory of Partitioned Global Address Spaces},
author = {Georgel Calin and Egor Derevenetc and Rupak Majumdar and Roland Meyer},
journal= {arXiv preprint arXiv:1307.6590},
year = {2013}
}