A Simple Model of Communication APIs ­ - Application to Dynamic Partial-order Reduction

Cristian Rosa 1, * Stephan Merz 2 Martin Quinson 1
* Auteur correspondant
1 ALGORILLE - Algorithms for the Grid
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : We are interested in the verification, using model checking, of distributed programs that communicate asynchronously over standard communication APIs such as MPI. This is feasible only if the set of executions that the model checker explores is aggressively reduced to a subset of representative executions, using techniques such as dynamic partial-order reduction. We propose a small set of core primitives in terms of which such APIs can be defined and formally specify these primitives in TLA+ . From this specification we derive theorems about the (in)dependence of invocations of the primitives, and use them in a DPOR-based verifier that runs within SimGrid, a simulation framework for distributed programming. Our preliminary experimental results indicate that we obtain good reductions, even though complex network operations are implemented in terms of the core communication primitives.
Type de document :
Communication dans un congrès
10th International Workshop on Automated Verification of Critical Systems - AVOCS 2010, Sep 2010, Düsseldorf, Germany. 2010
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00532889
Contributeur : Martin Quinson <>
Soumis le : jeudi 4 novembre 2010 - 16:27:20
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 14:55:54

Fichier

avocs.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00532889, version 1

Collections

Citation

Cristian Rosa, Stephan Merz, Martin Quinson. A Simple Model of Communication APIs ­ - Application to Dynamic Partial-order Reduction. 10th International Workshop on Automated Verification of Critical Systems - AVOCS 2010, Sep 2010, Düsseldorf, Germany. 2010. 〈inria-00532889〉

Partager

Métriques

Consultations de la notice

446

Téléchargements de fichiers

178