------------------
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
.. toggle-header::
: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
.. 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.
- 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