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

• Main Authors: Merz, Stephan, Quinson, Martin, Rosa, Cristian
• Other Authors: 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
• Language: English
• Published: HAL CCSD 2011
• Subjects: 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]; Iceland
• 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

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.