Mc SimGrid is currently less mature than other parts of the framework, but it improves every month. Please report any question and
issue so that we can further improve it.
+Limits
+^^^^^^
+
+The main limit of Model Checking lies in the huge amount of scenarios to explore. SimGrid tries to explore only non-redundant
+scenarios thanks to classical reduction techniques (such as DPOR and stateful exploration) but the exploration may well never
+finish if you don't carefully adapt your application to this mode.
+
+A classical trap is that the Model Checker can only verify whether your application fits the properties provided, which is
+useless if you have a bug in your property. Remember also that one way for your application to never violate a given assertion
+is to not start at all, because of a stupid bug.
+
+Another limit of this mode is that it does not use the performance models of the simulation mode. Time becomes discrete: You can
+say for example that the application took 42 steps to run, but there is no way to know how much time it took or the number of
+watts that were dissipated.
+
+Finally, the model checker only explores the interleavings of computations and communications. Other factors such as thread
+execution interleaving are not considered by the SimGrid model checker.
+
+The model checker may well miss existing issues, as it computes the possible outcomes *from a given initial situation*. There is
+no way to prove the correctness of your application in full generality with this tool.
+
Getting Mc SimGrid
------------------
It is included in the SimGrid source code, but it is not compiled in by default as it induces a small performance overhead to the
-simulations. It is also not activated in the Debian package, nor in the Java or Python binary distributions. If you just plan to
+simulations. It is also not activated in the Debian package, nor in the Python binary distributions. If you just plan to
experiment with Mc SimGrid, the easiest is to get the corresponding docker image. On the long term, you probably want to install it on
your machine: it works out of the box on Linux, Windows (with WSL2) and FreeBSD. Simply request it from cmake (``cmake
-Denable_model-checking .``) and then compile SimGrid :ref:`as usual <install_src>`. Unfortunately, Mc SimGrid does not work natively
.. code-block:: console
$ docker image pull simgrid/tuto-mc
- $ mkdir ~/tuto-mcsimgrid # or chose another directory to share between your computer and the docker container
- $ docker run -it --rm --name mcsimgrid --volume ~/tuto-mcsimgrid:/source/tutorial simgrid/tuto-mc bash
+ $ mkdir ~/tuto-mcsimgrid # or chose another directory to share between your computer and the docker container
+ $ docker run --user $UID:$GID -it --rm --name mcsimgrid --volume ~/tuto-mcsimgrid:/source/tutorial simgrid/tuto-mc bash
In the container, you have access to the following directories of interest:
if you prefer (see below for details on using the MPI version).
.. toggle-header::
- :header: Code of ``ndet-receive-s4u.cpp``: click here to open it, or `view it online <https://framagit.org/simgrid/tutorial-model-checking/-/blob/main/ndet-receive-s4u.cpp>`_
+ :header: Code of ``ndet-receive-s4u.cpp``: click here to open
+
+ You can also `view it online <https://framagit.org/simgrid/tutorial-model-checking/-/blob/main/ndet-receive-s4u.cpp>`_
.. literalinclude:: tuto_mc/ndet-receive-s4u.cpp
:language: cpp
reports the first faulty execution it finds: it may not be the shorter possible one.
.. code-block:: console
-
+
[0.000000] [mc_ModelChecker/INFO] Counter-example execution trace:
- [0.000000] [mc_ModelChecker/INFO] [(1)Tremblay (server)] iRecv(dst=(1)Tremblay (server), buff=(verbose only), size=(verbose only))
- [0.000000] [mc_ModelChecker/INFO] [(2)Jupiter (client)] iSend(src=(2)Jupiter (client), buff=(verbose only), size=(verbose only))
- [0.000000] [mc_ModelChecker/INFO] [(1)Tremblay (server)] Wait(comm=(verbose only) [(2)Jupiter (client)-> (1)Tremblay (server)])
- [0.000000] [mc_ModelChecker/INFO] [(1)Tremblay (server)] iRecv(dst=(1)Tremblay (server), buff=(verbose only), size=(verbose only))
- [0.000000] [mc_ModelChecker/INFO] [(2)Jupiter (client)] Wait(comm=(verbose only) [(2)Jupiter (client)-> (1)Tremblay (server)])
- [0.000000] [mc_ModelChecker/INFO] [(4)Ginette (client)] iSend(src=(4)Ginette (client), buff=(verbose only), size=(verbose only))
- [0.000000] [mc_ModelChecker/INFO] [(1)Tremblay (server)] Wait(comm=(verbose only) [(4)Ginette (client)-> (1)Tremblay (server)])
- [0.000000] [mc_ModelChecker/INFO] [(1)Tremblay (server)] iRecv(dst=(1)Tremblay (server), buff=(verbose only), size=(verbose only))
- [0.000000] [mc_ModelChecker/INFO] [(3)Bourassa (client)] iSend(src=(3)Bourassa (client), buff=(verbose only), size=(verbose only))
- [0.000000] [mc_ModelChecker/INFO] [(1)Tremblay (server)] Wait(comm=(verbose only) [(3)Bourassa (client)-> (1)Tremblay (server)])
+ [0.000000] [mc_ModelChecker/INFO] 1: iRecv(mbox=0)
+ [0.000000] [mc_ModelChecker/INFO] 2: iSend(mbox=0)
+ [0.000000] [mc_ModelChecker/INFO] 1: WaitComm(from 2 to 1, mbox=0, no timeout)
+ [0.000000] [mc_ModelChecker/INFO] 1: iRecv(mbox=0)
+ [0.000000] [mc_ModelChecker/INFO] 2: WaitComm(from 2 to 1, mbox=0, no timeout)
+ [0.000000] [mc_ModelChecker/INFO] 4: iSend(mbox=0)
+ [0.000000] [mc_ModelChecker/INFO] 1: WaitComm(from 4 to 1, mbox=0, no timeout)
+ [0.000000] [mc_ModelChecker/INFO] 1: iRecv(mbox=0)
+ [0.000000] [mc_ModelChecker/INFO] 3: iSend(mbox=0)
+ [0.000000] [mc_ModelChecker/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
- Then, the execution path is given.
==402== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
==402== Using Valgrind-3.16.1 and LibVEX; rerun with -h for copyright info
==402== Command: ./ndet-receive-s4u small_platform.xml --cfg=model-check/replay:1;2;1;1;2;4;1;1;3;1
- ==402==
+ ==402==
[0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/replay' to '1;2;1;1;2;4;1;1;3;1'
[0.000000] [mc_record/INFO] path=1;2;1;1;2;4;1;1;3;1
[Jupiter:client:(2) 0.000000] [example/INFO] Sending 1
[Jupiter:client:(2) 0.000000] [example/INFO] Sent!
[Tremblay:server:(1) 0.000000] /source/tutorial/ndet-receive-s4u.cpp:27: [root/CRITICAL] Assertion value_got == 3 failed
(some output ignored)
- ==402==
+ ==402==
==402== Process terminating with default action of signal 6 (SIGABRT): dumping core
==402== at 0x550FCE1: raise (raise.c:51)
==402== by 0x54F9536: abort (abort.c:79)
.. code-block:: console
- [0.000000] [mc_safety/INFO] Expanded states = 22
- [0.000000] [mc_safety/INFO] Visited states = 56
- [0.000000] [mc_safety/INFO] Executed transitions = 52
+ [0.000000] [mc_dfs/INFO] DFS exploration ended. 22 unique states visited; 4 backtracks (56 transition replays, 30 states visited overall)
- Finally, the application stack trace is displayed as the model-checker sees it. It should be the same as the one displayed from the
application side, unless you found a bug our tools.
translation of ``ndet-receive-s4u.cpp`` to MPI.
.. toggle-header::
- :header: Code of ``ndet-receive-mpi.c``: click here to open it, or `view it online <https://framagit.org/simgrid/tutorial-model-checking/-/blob/main/ndet-receive-mpi.cpp>`_
+ :header: Code of ``ndet-receive-mpi.c``: click here to open
+
+ You can also `view it online <https://framagit.org/simgrid/tutorial-model-checking/-/blob/main/ndet-receive-mpi.c>`_.
.. literalinclude:: tuto_mc/ndet-receive-mpi.c
:language: cpp
- You should pass some specific flags to the linker when compiling your application: ``-Wl,-znorelro -Wl,-znoseparate-code`` In the
docker, the provided CMakeLists.txt provides them for you when compiling the provided code. ``smpicc`` and friends also add this
parameter automatically.
+- If you get error messages complaining about the Dwarf version used, try adding ``-gdwarf-4`` to you CFLAGS and CXXFLAGS.
+ If you find a situation where this flag is needed in ``smpicc``, please report this issue.
- Also install ``libboost-stacktrace-dev`` to display nice backtraces from the application side (the one from the model-checking side is
available in any case, but it contains less details).
- Mc SimGrid uses the ``ptrace`` system call to spy on the verified application. Some versions of Docker forbid the use of this call by
