VSS Challenge Problem: Verifying the Correctness of AllReduce Algorithms in the MPICH Implementation of MPI

TL;DR

The paper addresses verifying the correctness of multiple MPICH allreduce algorithms by proving their equivalence to a reduce-plus-broadcast baseline. It uses standalone algorithm variants combined with wrapper layers and CIVL-based formal verification to establish equivalence for recursive doubling and reduce_scatter-allgather under builtin operator and datatype assumptions, while acknowledging limitations for nonblocking cases. The authors report successful proofs within constrained input sizes and process counts and discuss the restrictions and potential extensions needed to handle more general (non-builtin) cases. This work provides a practical methodology for formally validating MPI collectives in major libraries, contributing to reliability and portability of parallel software.

Abstract

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.