SimGrid MC: Verification Support for a Multi-API Simulation Platform

Stephan Merz; Martin Quinson; Cristian Rosa

inria-00593505, version 1

SimGrid MC: Verification Support for a Multi-API Simulation Platform

Stephan Merz () ^1, 2, Martin Quinson ()^a^, 3, Cristian Rosa () ³

31st IFIP International Conference on Formal Techniques for Networked and Distributed Systems 6722 (2011) 274-288

Résumé : SimGrid MC is a stateless model checker for distributed systems that is part of the SimGrid Simulation Framework. It verifies implementations of distributed algorithms, written in C and using any of several communication APIs provided by the simulator. Because the model checker is fully integrated in the simulator that programmers use to validate their implementations, they gain powerful verification capabilities without having to adapt their code. We describe the architecture of SimGrid MC, and show how it copes with the state space explosion problem. In particular, we argue that a generic Dynamic Partial Order Reductions algorithm is effective for handling the different communication APIs that are provided by SimGrid. As a case study, we verify an implementation of Chord, where SimGrid MC helped us discover an intricate bug in a matter of seconds.

a – Université Henri Poincaré - Nancy I
1 : VERIDIS (INRIA Nancy - Grand Est / LORIA)
Université de Lorraine – CNRS : UMR7503 – INRIA
2 : MOSEL (LORIA)
INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
3 : ALGORILLE (INRIA Lorraine - LORIA)
INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)

inria-00593505, version 1
http://hal.inria.fr/inria-00593505
oai:hal.inria.fr:inria-00593505
Contributeur : Stephan Merz <>
Soumis le : Lundi 16 Mai 2011, 12:33:57
Dernière modification le : Mardi 13 Décembre 2011, 16:40:47

Voir la fiche détaillée

Documents associés

DOI : 10.1007/978-3-642-21461-5_18

Exporter

Bibtex EndNote TEI RefWorks

%F inria-00593505, version 1
%0 Conference Proceedings
%U http://hal.inria.fr/inria-00593505
%2 INFO:INFO_LO;INFO:INFO_DC
%T SimGrid MC: Verification Support for a Multi-API Simulation Platform
%A Merz, Stephan
%A Quinson, Martin
%A Rosa, Cristian
%+ VERIDIS - INRIA Nancy - Grand Est / LORIA , MOSEL - LORIA , ALGORILLE - INRIA Lorraine - LORIA
%X SimGrid MC is a stateless model checker for distributed systems that is part of the SimGrid Simulation Framework. It verifies implementations of distributed algorithms, written in C and using any of several communication APIs provided by the simulator. Because the model checker is fully integrated in the simulator that programmers use to validate their implementations, they gain powerful verification capabilities without having to adapt their code. We describe the architecture of SimGrid MC, and show how it copes with the state space explosion problem. In particular, we argue that a generic Dynamic Partial Order Reductions algorithm is effective for handling the different communication APIs that are provided by SimGrid. As a case study, we verify an implementation of Chord, where SimGrid MC helped us discover an intricate bug in a matter of seconds.
%2 D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.4: Model checking, I.: Computing Methodologies/I.6: SIMULATION AND MODELING/I.6.7: Simulation Support Systems
%G Anglais
%8 2011-06-00
%2 internationale
%B 31st IFIP International Conference on Formal Techniques for Networked and Distributed Systems
%2 Reykjavik
%2 Islande
%8 2011-06-06
%8 2011-06-09
%E Roberto Bruni and Juergen Dingel
%I Springer
%2 Proceedings of Formal Techniques for Distributed Systems Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011, and 30th IFIP WG 6.1 International Conference - FORTE 2011
%V 6722
%N Lecture Notes in Computer Science
%P 274-288
%R 10.1007/978-3-642-21461-5_18
%K model checking; simulation; distributed systems; partial-order reduction
%Z The original publication is available at www.springerlink.com
%2 7645

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Communications avec actes</head>
<biblStruct type="inproceedings" xml:id="inria-00593505"><analytic>
<author><persName><forename>Stephan</forename><surname>Merz</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Nancy - Grand Est / LORIA</orgName>
<orgName type="team">VERIDIS</orgName>
<country>FR</country>
<orgName type="institution">Université de Lorraine</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">INRIA</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">LORIA</orgName>
<orgName type="team">MOSEL</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Martin</forename><surname>Quinson</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA</orgName>
<orgName type="team">ALGORILLE</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Cristian</forename><surname>Rosa</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA</orgName>
<orgName type="team">ALGORILLE</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<title type="main" level="a">SimGrid MC: Verification Support for a Multi-API Simulation Platform</title></analytic><monogr><meeting>31st IFIP International Conference on Formal Techniques for Networked and Distributed Systems</meeting><imprint><publisher>Springer</publisher><pubPlace><settlement>Reykjavik</settlement><country>Islande</country></pubPlace><biblScope type="publicationDate">2011-06-00</biblScope><biblScope type="vol">6722</biblScope><biblScope type="pp">274-288</biblScope></imprint></monogr><idno type="doi">10.1007/978-3-642-21461-5_18</idno><idno type="HALid">http://hal.inria.fr/inria-00593505</idno></biblStruct>
</listBibl>
</listBibl>