Verifying MPI Applications with SimGridMC
Author/Presenters
Event Type
Workshop
Applications
Correctness
Debugging
Reliability
SIGHPC Workshop
Verification
TimeSunday, November 12th11:21am -
11:38am
Location501
DescriptionSimGridMC (also dubbed Mc SimGrid) is a stateful Model
Checker for MPI applications. It is integrated to
SimGrid, a framework mostly dedicated to predicting the
performance of distributed applications. We describe the
architecture of McSimGrid, and show how it copes with
the state space explosion problem using Dynamic Partial
Or- der Reduction and State Equality algorithms. As case
studies we show how SimGrid can enforce safety and
liveness properties for MPI applications, as well as
global invariants over communication patterns.
