DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
summary
DafnyMPI is a pure Dafny library that verifies MPI programs by requiring a statically declared communication topology and unique message tags so preconditions on MPI_ISEND/MPI_WAIT suffice to guarantee deadlock freedom via tag ordering. The work proves deadlock freedom in a core calculus, uses rely‑guarantee for payloads and buffer safety, verifies three canonical PDE solvers (convection, advection, diffusion) showing speedups when compiled to Python, and ships artifacts evaluated — functional.
AI-written summary · about
chapters (8)
- 0:00DafnyMPI and MPI basics
- 3:55DafnyMPI library goals
- 7:50Communication topology enforcement
- 9:35Deadlock freedom proof
- 15:14Verified PDE solvers
- 17:47Verification overhead analysis
- 19:53Contributions and future work
- 20:14Q&A
related talks
44mCAN WE FREE CONCURRENT PROGRAMMING FROM THE MONADIC STYLE
16mAutomated Verification of Parametric Channel-Based Process Communication
54mDesigning for Concurrency Using Message Passing in C++
14mMultiparty GV: Functional Multiparty Session Types with Certified Deadlock Fre...
01h 01mThe Future of Concurrency and Parallelism
21mMechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Libr
28mAutomated Correctness Analysis for core.async
55mJava PathFinder: going to Mars without bugs and deadlocks