Verifying MPI Applications with SimGridMC

The Anh Pham 1 Thierry Jéron 2 Martin Quinson 1
1 MYRIADS - Design and Implementation of Autonomous Distributed Systems
Inria Rennes – Bretagne Atlantique , IRISA_D1 - SYSTÈMES LARGE ÉCHELLE
2 SUMO - SUpervision of large MOdular and distributed systems
Inria Rennes – Bretagne Atlantique , IRISA_D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : 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.
Type de document :
Communication dans un congrès
Correctness 2017 - First International Workshop on Software Correctness for HPC Applications, Nov 2017, Denver, United States. 〈10.1145/3145344.3145345〉
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01632421
Contributeur : Thierry Jéron <>
Soumis le : vendredi 10 novembre 2017 - 10:46:23
Dernière modification le : jeudi 15 novembre 2018 - 11:58:59
Document(s) archivé(s) le : dimanche 11 février 2018 - 12:33:43

Fichier

McSimGrid-correctness17.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

The Anh Pham, Thierry Jéron, Martin Quinson. Verifying MPI Applications with SimGridMC. Correctness 2017 - First International Workshop on Software Correctness for HPC Applications, Nov 2017, Denver, United States. 〈10.1145/3145344.3145345〉. 〈hal-01632421〉

Partager

Métriques

Consultations de la notice

438

Téléchargements de fichiers

122