Collective Contracts for Message-Passing Parallel Programs

Procedure contracts are a well-known approach for specifying programs in a modular way. We investigate a new contract theory for collective procedures in parallel message-passing programs. As in the sequential setting, one can verify that a procedure $f$ conforms to its contract using only the contracts, and not the implementations, of the collective procedures called by $f$. We apply this approach to C programs that use the Message Passing Interface (MPI), introducing a new contract language that extends the ANSI/ISO C Specification Language (ACSL). We present contracts for the standard MPI collective functions, as well as many user-defined collective functions. A prototype verification system has been implemented using the CIVL symbolic execution and model checking framework for checking contract satisfaction within small bounds on the number of processes.

@inproceedings{luo-siegel:2024:contracts,
  author = {Ziqing Luo and Stephen F.\ Siegel},
  title = {Collective Contracts for Message-Passing Parallel Programs},
  booktitle={Computer Aided Verification (CAV 2024)},
  volume = 14682,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  address = {Cham},
  editor = {Gurfinkel, Arie and Ganesh, Vijay},
  doi = {10.1007/978-3-031-65630-9_3},
  pages = {44--68},
  year = {2024}
}