Verifying MPI Applications with SimGridMC
Verifying MPI Applications with SimGridMC
SimGridMC (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 Order 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.
• Theory of computation → Parallel algorithms, Ultra-large-scale systems, Software verification, [INFO.INFO-SE] Computer Science [cs]/Software Engineering [cs.SE], Dynamic analysis, Software and its engineering → Model checking, Formal software verification
• Theory of computation → Parallel algorithms, Ultra-large-scale systems, Software verification, [INFO.INFO-SE] Computer Science [cs]/Software Engineering [cs.SE], Dynamic analysis, Software and its engineering → Model checking, Formal software verification
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).10 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Top 10% influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Top 10%
Citations provided by BIP!Popularity provided by BIP!