SimGrid MC: Verification Support for a Multi-API Simulation Platform
The original publication is available at www.springerlink.com International audience 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 communic...
Main Authors: | , , |
---|---|
Other Authors: | , , , , , , , , , , , |
Format: | Conference Object |
Language: | English |
Published: |
HAL CCSD
2011
|
Subjects: | |
Online Access: | https://inria.hal.science/inria-00593505 https://inria.hal.science/inria-00593505/document https://inria.hal.science/inria-00593505/file/978-3-642-21461-5_18_Chapter.pdf https://doi.org/10.1007/978-3-642-21461-5_18 |
id |
ftunilorrainehal:oai:HAL:inria-00593505v1 |
---|---|
record_format |
openpolar |
spelling |
ftunilorrainehal:oai:HAL:inria-00593505v1 2023-10-09T21:52:46+02:00 SimGrid MC: Verification Support for a Multi-API Simulation Platform Merz, Stephan Quinson, Martin Rosa, Cristian VERIfication pour les systèmes DIStribués (VERIDIS) Inria Nancy - Grand Est Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS) Algorithms for the Grid (ALGORILLE) INRIA Lorraine Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS) Roberto Bruni Juergen Dingel TC 6 WG 6.1 ANR-08-SEGI-0022,USS-SimGrid,Simulation extrêmement extensible avec SimGrid(2008) Reykjavik, Iceland 2011-06-06 https://inria.hal.science/inria-00593505 https://inria.hal.science/inria-00593505/document https://inria.hal.science/inria-00593505/file/978-3-642-21461-5_18_Chapter.pdf https://doi.org/10.1007/978-3-642-21461-5_18 en eng HAL CCSD Springer info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-642-21461-5_18 inria-00593505 https://inria.hal.science/inria-00593505 https://inria.hal.science/inria-00593505/document https://inria.hal.science/inria-00593505/file/978-3-642-21461-5_18_Chapter.pdf doi:10.1007/978-3-642-21461-5_18 http://creativecommons.org/licenses/by/ info:eu-repo/semantics/OpenAccess Lecture Notes in Computer Science 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE) https://inria.hal.science/inria-00593505 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik, Iceland. pp.274-288, ⟨10.1007/978-3-642-21461-5_18⟩ partial-order reduction distributed systems model checking simulation ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.4: Model checking ACM: I.: Computing Methodologies/I.6: SIMULATION AND MODELING/I.6.7: Simulation Support Systems [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] [INFO.INFO-DC]Computer Science [cs]/Distributed Parallel and Cluster Computing [cs.DC] info:eu-repo/semantics/conferenceObject Conference papers 2011 ftunilorrainehal https://doi.org/10.1007/978-3-642-21461-5_18 2023-09-12T23:25:41Z The original publication is available at www.springerlink.com International audience 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. Conference Object Iceland Université de Lorraine: HAL 274 288 |
institution |
Open Polar |
collection |
Université de Lorraine: HAL |
op_collection_id |
ftunilorrainehal |
language |
English |
topic |
partial-order reduction distributed systems model checking simulation ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.4: Model checking ACM: I.: Computing Methodologies/I.6: SIMULATION AND MODELING/I.6.7: Simulation Support Systems [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] [INFO.INFO-DC]Computer Science [cs]/Distributed Parallel and Cluster Computing [cs.DC] |
spellingShingle |
partial-order reduction distributed systems model checking simulation ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.4: Model checking ACM: I.: Computing Methodologies/I.6: SIMULATION AND MODELING/I.6.7: Simulation Support Systems [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] [INFO.INFO-DC]Computer Science [cs]/Distributed Parallel and Cluster Computing [cs.DC] Merz, Stephan Quinson, Martin Rosa, Cristian SimGrid MC: Verification Support for a Multi-API Simulation Platform |
topic_facet |
partial-order reduction distributed systems model checking simulation ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.4: Model checking ACM: I.: Computing Methodologies/I.6: SIMULATION AND MODELING/I.6.7: Simulation Support Systems [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] [INFO.INFO-DC]Computer Science [cs]/Distributed Parallel and Cluster Computing [cs.DC] |
description |
The original publication is available at www.springerlink.com International audience 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. |
author2 |
VERIfication pour les systèmes DIStribués (VERIDIS) Inria Nancy - Grand Est Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS) Algorithms for the Grid (ALGORILLE) INRIA Lorraine Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS) Roberto Bruni Juergen Dingel TC 6 WG 6.1 ANR-08-SEGI-0022,USS-SimGrid,Simulation extrêmement extensible avec SimGrid(2008) |
format |
Conference Object |
author |
Merz, Stephan Quinson, Martin Rosa, Cristian |
author_facet |
Merz, Stephan Quinson, Martin Rosa, Cristian |
author_sort |
Merz, Stephan |
title |
SimGrid MC: Verification Support for a Multi-API Simulation Platform |
title_short |
SimGrid MC: Verification Support for a Multi-API Simulation Platform |
title_full |
SimGrid MC: Verification Support for a Multi-API Simulation Platform |
title_fullStr |
SimGrid MC: Verification Support for a Multi-API Simulation Platform |
title_full_unstemmed |
SimGrid MC: Verification Support for a Multi-API Simulation Platform |
title_sort |
simgrid mc: verification support for a multi-api simulation platform |
publisher |
HAL CCSD |
publishDate |
2011 |
url |
https://inria.hal.science/inria-00593505 https://inria.hal.science/inria-00593505/document https://inria.hal.science/inria-00593505/file/978-3-642-21461-5_18_Chapter.pdf https://doi.org/10.1007/978-3-642-21461-5_18 |
op_coverage |
Reykjavik, Iceland |
genre |
Iceland |
genre_facet |
Iceland |
op_source |
Lecture Notes in Computer Science 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE) https://inria.hal.science/inria-00593505 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik, Iceland. pp.274-288, ⟨10.1007/978-3-642-21461-5_18⟩ |
op_relation |
info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-642-21461-5_18 inria-00593505 https://inria.hal.science/inria-00593505 https://inria.hal.science/inria-00593505/document https://inria.hal.science/inria-00593505/file/978-3-642-21461-5_18_Chapter.pdf doi:10.1007/978-3-642-21461-5_18 |
op_rights |
http://creativecommons.org/licenses/by/ info:eu-repo/semantics/OpenAccess |
op_doi |
https://doi.org/10.1007/978-3-642-21461-5_18 |
container_start_page |
274 |
op_container_end_page |
288 |
_version_ |
1779315942554075136 |