VSS Challenge Problem: Verifying the Correctness of AllReduce Algorithms in the MPICH Implementation of MPI
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909847611506688 |
|---|---|
| author | Hovland, Paul D. |
| author_facet | Hovland, Paul D. |
| contents | We describe a challenge problem for verification based on the MPICH implementation of MPI. The MPICH implementation includes several algorithms for allreduce, all of which should be functionally equivalent to reduce followed by broadcast. We created standalone versions of three algorithms and verified two of them using CIVL. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_13413 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | VSS Challenge Problem: Verifying the Correctness of AllReduce Algorithms in the MPICH Implementation of MPI Hovland, Paul D. Logic in Computer Science Distributed, Parallel, and Cluster Computing D.2.4; D.1.3 We describe a challenge problem for verification based on the MPICH implementation of MPI. The MPICH implementation includes several algorithms for allreduce, all of which should be functionally equivalent to reduce followed by broadcast. We created standalone versions of three algorithms and verified two of them using CIVL. |
| title | VSS Challenge Problem: Verifying the Correctness of AllReduce Algorithms in the MPICH Implementation of MPI |
| topic | Logic in Computer Science Distributed, Parallel, and Cluster Computing D.2.4; D.1.3 |
| url | https://arxiv.org/abs/2510.13413 |