Parameterized Verification of Deterministic MPI Programs
2026-07-20 • Programming Languages
Programming LanguagesLogic in Computer Science
AI summaryⓘ
The authors study how to check if a message passing program works correctly when the number of processes can change and each process has a unique ID. They ask users to provide some information about how many messages are sent between processes, when messages happen in order, and specific details about each message. Using this, they turn the program into one that runs step-by-step in sequence, which is easier to verify with existing tools. They implemented this method as an extension to Frama-C/Wp to help verify C programs using MPI communication.
message passingparameterized verificationprocess IDsend/receivehappens-beforeFrama-CMPIsequentializationprogram verification
Authors
Stephen F. Siegel
Abstract
We consider the problem of verifying a message passing program in which the number of processes is a parameter NP and each process knows its unique ID. Processes communicate using send and receive commands which specify a single destination or source. To verify the program, the user provides functions specifying the number of messages sent from process i to process j, the level of each communication event in the happens-before hierarchy, and a fact that holds for the k-th message sent from i to j. These are used to transform the program to a parameterized sequential program which can be verified using any techniques appropriate for such programs. We realize this approach in an extension to Frama-C/Wp to verify C/MPI programs.