------------------
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
$ 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 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
.. 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:: 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
