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

Cristian Rosa 1, * Stephan Merz 2 Martin Quinson 1
* Corresponding author
1 ALGORILLE - Algorithms for the Grid
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 VERIDIS - VERIfication pour les systèmes DIStribués
Inria Nancy - Grand Est, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications : UMR7503
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.
Liste complète des métadonnées

Cited literature [11 references]  Display  Hide  Download

https://hal.inria.fr/inria-00532889
Contributor : Martin Quinson <>
Submitted on : Thursday, November 4, 2010 - 4:27:20 PM
Last modification on : Thursday, February 21, 2019 - 2:02:02 PM
Document(s) archivé(s) le : Friday, October 26, 2012 - 2:55:54 PM

File

avocs.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨inria-00532889⟩

Share

Metrics

Record views

474

Files downloads

187