DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs

TL;DR

DafnyMPI is a library that enables formal verification of MPI-based parallel programs, ensuring deadlock freedom, termination, and functional correctness without custom concurrency logic.

Contribution

It introduces DafnyMPI, a scalable, verification-friendly library for MPI programs that extends Dafny with concurrent reasoning capabilities and formal guarantees.

Findings

Proves deadlock freedom using formal methods.

Verifies termination and absence of runtime errors.

Demonstrates applicability on PDE numerical solutions.

Abstract

The Message Passing Interface (MPI) is widely used in parallel, high-performance programming, yet writing bug-free software that uses MPI remains difficult. We introduce DafnyMPI, a novel, scalable approach to formally verifying MPI software. DafnyMPI allows proving deadlock freedom, termination, and functional equivalence with simpler sequential implementations. In contrast to existing specialized frameworks, DafnyMPI avoids custom concurrency logics and instead relies on Dafny, a verification-ready programming language used for sequential programs, extending it with concurrent reasoning abilities. DafnyMPI is implemented as a library that enables safe MPI programming by requiring users to specify the communication topology upfront and to verify that calls to communication primitives such as MPI_ISEND and MPI_WAIT meet their preconditions. We formalize DafnyMPI using a core calculus and prove that the preconditions suffice to guarantee deadlock freedom. Functional equivalence is proved via rely-guarantee reasoning over message payloads and a system that guarantees safe use of read and write buffers. Termination and the absence of runtime errors are proved using standard Dafny techniques. To further demonstrate the applicability of DafnyMPI, we verify numerical solutions to three canonical partial differential equations. We believe DafnyMPI demonstrates how to make formal verification viable for a broader class of programs and provides proof engineers with additional tools for software verification of parallel and concurrent systems.