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

Cristian Rosa, Stephan Merz, and 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.

© Europ. Assoc. Software Science and Technology 2010

Available as: PDF

Reference

@InProceedings{rosa:simple,
  author =       {Cristian Rosa and Stephan Merz and Martin Quinson},
  title =        {A Simple Model of Communication APIs - Application to Dynamic Partial-order Reduction},
  booktitle = {10th Intl. Workshop Automated Verification of Critical Systems (AVoCS 2010)},
  pages =     {15},
  year =      2010,
  editor =    {Jens Bendisposto and Michael Leuschel and Markus Roggenbach},
  volume =    35,
  series =    {Elec. Comm. Europ. Assoc. Software Science and Technology (ECEASST 35)},
  address =   {D{\"u}sseldorf, Germany},
  publisher = {ECEASST},
}