------------------
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
on Mac OS X yet, so mac users should stick to the docker method for now.
-.. code-block:: shell
+.. 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
+ $ docker image pull simgrid/tuto-mc
+ $ 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:
Let's go with a first example of a bugged program. Once in the container, copy all files from the tutorial into the directory shared
between your host computer and the container.
-.. code-block:: shell
+.. code-block:: console
# From within the container
$ cp -r /source/tuto-mc.git/* /source/tutorial/
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
send their parameter to a given mailbox. A ``server`` receives 3 messages and assumes that the last received message is the number ``3``.
If you compile and run it, it simply works:
-.. code-block:: shell
+.. code-block:: console
$ cmake . && make
(output omitted)
source code and/or the platform file, but this is not a method. Time to start Mc SimGrid, the SimGrid model checker, to exhaustively test
all message orders. For that, you simply launch your simulation as a parameter to the ``simgrid-mc`` binary as you would do with ``valgrind``:
-.. code-block:: shell
+.. code-block:: console
$ simgrid-mc ./ndet-receive-s4u small_platform.xml
(some output ignored)
all possible outcome of the code, the execution is sometimes rewind to explore another possible branch (here: another possible
message ordering). Note also that all times are always 0 in the model checker, since the time is abstracted away in this mode.
- .. code-block:: shell
+ .. code-block:: console
[0.000000] [mc_safety/INFO] Check a safety property. Reduction is: dpor.
[Jupiter:client:(2) 0.000000] [example/INFO] Sending 1
- Then you have the error message, along with a backtrace of the application at the point where the assertion fails. Not all the frames of
the backtrace are useful, and some are omitted here.
- .. code-block:: shell
+ .. code-block:: console
[Tremblay:server:(1) 0.000000] /source/tutorial/ndet-receive-s4u.cpp:27: [root/CRITICAL] Assertion value_got == 3 failed
Backtrace (displayed in actor server):
- First, the error message itself. The ``xbt_assert`` in the code result in an ``abort()`` in the application, that is interpreted as an
application crash by the model-checker.
- .. code-block:: shell
+ .. code-block:: console
[0.000000] [mc_ModelChecker/INFO] **************************
[0.000000] [mc_ModelChecker/INFO] ** CRASH IN THE PROGRAM **
calls we made (put/get) are split in atomic calls (iSend+Wait/iRecv+Wait), and all executions are interleaved. Also, Mc SimGrid
reports the first faulty execution it finds: it may not be the shorter possible one.
- .. code-block:: shell
-
+ .. 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.
- .. code-block:: shell
+ .. code-block:: console
[0.000000] [mc_record/INFO] Path = 1;2;1;1;2;4;1;1;3;1
without ``simgrid-mc``. This is because ``simgrid-mc`` forbids to use a debugger such as gdb or valgrind on the code during the
model-checking. For example, you can trigger the same execution in valgrind as follows:
- .. code-block:: shell
+ .. code-block:: console
$ valgrind ./ndet-receive-s4u small_platform.xml --cfg=model-check/replay:'1;2;1;1;2;4;1;1;3;1'
==402== Memcheck, a memory error detector
==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)
point of the exploration), the visited states (the amount of times we visited another state -- the same state may have been visited
several times) and the amount of transitions.
- .. code-block:: shell
+ .. 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
|br|
You can compile and run it on top of SimGrid as follows.
-.. code-block:: shell
+.. code-block:: console
$ smpicc ndet-receive-mpi.c -o ndet-receive-mpi
$ smpirun -np 4 -platform small_platform.xml ndet-receive-mpi
leading to it. It may not be the case on your machine, as this depends on the iteration order of an unsorted collection. Instead, we
should use Mc SimGrid to exhaustively explore the state space and trigger the bug in all cases.
-.. code-block:: shell
+.. code-block:: console
$ smpirun -wrapper simgrid-mc -np 4 -platform small_platform.xml ndet-receive-mpi
The produced output is then very similar to the one you get with S4U, even if the exact execution path leading to the bug may differs. You
can also trigger a given execution path out of the model-checker, for example to explore it with valgrind.
-.. code-block:: shell
+.. code-block:: console
$ smpirun -wrapper valgrind -np 4 -platform small_platform.xml --cfg=model-check/replay:'1;2;1;1;4;1;1;3;1' ndet-receive-mpi
- 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
issue, you should either update your settings (the security issue was solved in later versions of Linux), or add ``--cap-add
SYS_PTRACE`` to the docker parameters, as hinted by the text.
+Going further
+-------------
+
+This tutorial is not complete yet, as there is nothing on reduction
+techniques nor on liveness properties. For now, the best source of
+information on these topics is `this old tutorial
+<https://simgrid.org/tutorials/simgrid-mc-101.pdf>`_ and `that old
+presentation
+<http://people.irisa.fr/Martin.Quinson/blog/2018/0123/McSimGrid-Boston.pdf>`_.
+
.. |br| raw:: html
<br />
