VSS Challenge Problem: Verifying the Correctness of AllReduce Algorithms in the MPICH Implementation of MPI
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.
Authors
- Paul Hovland (ORCID: https://orcid.org/0000-0002-0907-2567)
Institutions
- Argonne National Laboratory (US)
Publication Details
- Journal
- Electronic Proceedings in Theoretical Computer Science
- Published
- 2025-10-14
- DOI
- https://doi.org/10.4204/eptcs.432.10
- Primary Topic
- Parallel Computing and Optimization Techniques
- Type
- article
- Field-Weighted Citation Impact
- 0.00
Funders
- U.S. Department of Energy
- Office of Science
- Advanced Scientific Computing Research