VSS挑战问题：验证MPI的MPICH实现中AllReduce算法的正确性
计算机科学中的逻辑
2025-10-16 v1 分布式、并行与集群计算
摘要
我们描述了一个基于MPI的MPICH实现的验证挑战问题。MPICH实现包括几种用于allreduce的算法，所有这些算法在功能上都应等价于先进行reduce再进行broadcast。我们创建了三种算法的独立版本，并使用CIVL验证了其中两种。
引用
@article{arxiv.2510.13413,
title = {VSS Challenge Problem: Verifying the Correctness of AllReduce Algorithms in the MPICH Implementation of MPI},
author = {Paul D. Hovland},
journal= {arXiv preprint arXiv:2510.13413},
year = {2025}
}
备注
In Proceedings VSS 2025, arXiv:2510.12314