The Partitioned Global Address Space (PGAS) execution model is a promising alternative model to MPI. PGAS implementations offer several programmability advantages over their MPI counterparts while
preserving the appeal of high-performance communication libraries. Among existing PGAS instances, Chapel and Unified Parallel-C (UPC) are some of the leading implementations. Unfortunately, despite multiple advances, anomaly detection support for PGAS programs, both at the language level and library level, has been largely ignored.

In this work, we propose new static analyses to detect various distributed, multi-locale anomalies in Chapel and UPC programs. We leverage constraint formulae to model Chapel/UPC semantics together with anomaly-specific constraints that encapsulate triggering conditions of the anomaly. Generated models are then checked with Z3 SMT solver to decide the existence of anomalies. While our implementation targets Chapel, the underlying approach generalizes to other PGAS languages, as we illustrate through a construct mapping to UPC. We demonstrate the effectiveness of our analyses on well-known scientific operators and communication patterns, comparing against native Chapel analyses and MPI debugging tools targeting lowered Chapel code. We further validate our approach with an evaluation on UPC programs.