A Simple Model of Communication APIs ­ - Application to Dynamic Partial-order Reduction - Archive ouverte HAL Access content directly
Conference Papers Year : 2010

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

(1) , (2) , (1)
1
2
Cristian Rosa
  • Function : Correspondent author
  • PersonId : 859830

Connectez-vous pour contacter l'auteur
Stephan Merz
Martin Quinson

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.
Fichier principal
Vignette du fichier
avocs.pdf (177.29 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00532889 , version 1 (04-11-2010)

Identifiers

  • HAL Id : inria-00532889 , version 1

Cite

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⟩
242 View
117 Download

Share

Gmail Facebook Twitter LinkedIn More