@inproceedings{burak_spmd_2024,
  title = {{{SPMD IR}}: {{Unifying SPMD}} And\ {{Multi-value IR Showcased}} For\ {{Static Verification}} Of\ {{Collectives}}},
  booktitle = {Recent {{Advances}} in the {{Message Passing Interface}}: 31st {{European MPI Users}}' {{Group Meeting}}, {{EuroMPI}} 2024, {{Perth}}, {{WA}}, {{Australia}}, {{September}} 25--27, 2024, {{Proceedings}}},
  author = {Burak, Semih and Ivanov, Ivan R. and Domke, Jens and M{\"u}ller, Matthias},
  year = {2024},
  pages = {3--20},
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg},
  doi = {10.1007/978-3-031-73370-3_1},
  abstract = {To effectively utilize modern HPC clusters, inter-node communication and related single program, multiple data (SPMD) parallel programming models such as mpi are inevitable. Current tools and compilers that employ analyses of SPMD models often have the limitation of only supporting one model or implementing the necessary abstraction internally. This makes the analysis and effort for the abstraction neither reusable nor the tool extensible to other models without extensive changes to the tool itself.This work proposes an spmd ir as part of a multi-layer program representation and accompanying compiler passes to explicitly express the results of abstraction and multi-value analysis. The spmd ir makes the executing processes of operations explicit and differentiates between static and dynamic cases. It is implemented as a prototype in the mlirllvm infrastructure and is comprised of the spmd dialect and two compiler passes, supporting mpi, shmem, and nccl, including hybrid cases.To evaluate the proposed IR, verification of collective communication was chosen as a use case. For that, this work reimplements and extends parcoach's static approach on the spmd ir and assesses it by an expanded micro-benchmark suite in mpi, shmem, and nccl. Achieving similar detection accuracy, the evaluation shows that the spmd ir's level of abstraction is strong enough for parcoach's analyses and generic enough for increased extensibility. The prototype also constitutes the first collectives verification of shmem, nccl, and their combinations (with mpi).},
  isbn = {978-3-031-73369-7},
  keywords = {Correctness,MLIR,MPI,NCCL,Parallel IR,SHMEM,Static Analysis}
}