docs/source/Tutorial_Model-checking.rst

   1 .. _usecase_modelchecking:
   2
   3 Formal Verification and Model-checking
   4 ======================================
   5
   6 SimGrid can not only predict the performance of your application, but also assess its correctness through formal methods. Mc SimGrid is
   7 a full-featured model-checker that is embedded in the SimGrid framework. It can be used to formally verify safety
   8 properties on codes running on top of SimGrid, be it :ref:`simple algorithms <usecase_simalgo>` or :ref:`full MPI applications
   9 <usecase_smpi>`.
  10
  11 Primer on formal methods
  12 ------------------------
  13
  14 Formal methods are techniques leveraging mathematics to test and assess systems. They are routinely used to assess computer hardware,
  15 transportation systems or any other complex engineering process. Among these methods, model-checking is a technique to automatically
  16 prove that a given model verifies a given property by systematically checking all states of the model. The property and model are
  17 written in a mathematical language and fed to an automated tool called model checker. When the model does not verify the property, the
  18 model checker gives a counter-example that can be used to refine and improve the model. Conversely, if no counter-example can be found
  19 after an exhaustive exploration of the model, we know that the property holds for the model. It may also happen that the model is too
  20 large to be exhaustively explored, in which case the model-checker is not conclusive. Model checkers rely on so-called reduction
  21 techniques (based on symmetries and equivalence) to efficiently explore the system state.
  22
  23 Dynamic verification applies similar ideas to programs, without requiring a mathematical model of the system. Instead, the program
  24 itself is used as a model to verify against a property. Along these lines, Mc SimGrid is a stateful model checker: it does not leverage
  25 static analysis nor symbolic execution. Instead, the program is simply executed through all possible outcomes. On indecision points, a
  26 system checkpoint is taken, the first branch is executed exhaustively, and then the system is roll back to that point to explore the
  27 other branch.
  28
  29 Mc SimGrid targets distributed applications that interact through message passing or through synchronization mechanisms (mutex,
  30 barrier, etc). Since it does not explicitly observe memory accesses, Mc SimGrid cannot automatically detect race conditions in
  31 multithreaded programs. It can however be used to detect misuses of the synchronization functions, such as the ones resulting in
  32 deadlocks.
  33
  34 Mc SimGrid can be used to verify classical `safety properties <https://en.wikipedia.org/wiki/Linear_time_property>`_, but
  35 also `communication determinism <https://hal.inria.fr/hal-01953167/document>`_, a property that allows more efficient solutions toward
  36 fault-tolerance. It can alleviate the state space explosion problem through `Dynamic Partial Ordering Reduction (DPOR)
  37 <https://en.wikipedia.org/wiki/Partial_order_reduction>`_ and `state equality <https://hal.inria.fr/hal-01900120/document>`_. Note that
  38 Mc SimGrid is currently less mature than other parts of the framework, but it improves every month. Please report any question and
  39 issue so that we can further improve it.
  40
  41 Limits
  42 ^^^^^^
  43
  44 The main limit of Model Checking lies in the huge amount of scenarios to explore. SimGrid tries to explore only non-redundant
  45 scenarios thanks to classical reduction techniques (such as DPOR and stateful exploration) but the exploration may well never
  46 finish if you don't carefully adapt your application to this mode.
  47
  48 A classical trap is that the Model Checker can only verify whether your application fits the properties provided, which is
  49 useless if you have a bug in your property. Remember also that one way for your application to never violate a given assertion
  50 is to not start at all, because of a stupid bug.
  51
  52 Another limit of this mode is that it does not use the performance models of the simulation mode. Time becomes discrete: You can
  53 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
  54 watts that were dissipated.
  55
  56 Finally, the model checker only explores the interleavings of computations and communications. Other factors such as thread
  57 execution interleaving are not considered by the SimGrid model checker.
  58
  59 The model checker may well miss existing issues, as it computes the possible outcomes *from a given initial situation*. There is
  60 no way to prove the correctness of your application in full generality with this tool.
  61
  62 Getting Mc SimGrid
  63 ------------------
  64
  65 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
  66 simulations. It is also not activated in the Debian package, nor in the Python binary distributions. If you just plan to
  67 experiment with Mc SimGrid, the easiest is to get the corresponding docker image. On the long term, you probably want to install it on
  68 your machine: it works out of the box on Linux, Windows (with WSL2) and FreeBSD. Simply request it from cmake (``cmake
  69 -Denable_model-checking .``) and then compile SimGrid :ref:`as usual <install_src>`. Unfortunately, Mc SimGrid does not work natively
  70 on Mac OS X yet, so mac users should stick to the docker method for now.
  71
  72 .. code-block:: console
  73
  74    $ docker image pull simgrid/tuto-mc
  75    $ mkdir ~/tuto-mcsimgrid # or chose another directory to share between your computer and the docker container
  76    $ docker run --user $UID:$GID -it --rm --name mcsimgrid --volume ~/tuto-mcsimgrid:/source/tutorial simgrid/tuto-mc bash
  77
  78 In the container, you have access to the following directories of interest:
  79
  80 - ``/source/tutorial``: A view to the ``~/tuto-mcsimgrid`` directory on your disk, out of the container.
  81   Edit the files you want from your computer and save them in ``~/tuto-mcsimgrid``;
  82   Compile and use them immediately within the container in ``/source/tutorial``.
  83 - ``/source/tuto-mc.git``: Files provided with this tutorial.
  84 - ``/source/simgrid.git``: Source code of SimGrid, pre-configured in MC mode. The framework is also installed in ``/usr``
  85   so the source code is only provided for your information.
  86
  87 Lab1: non-deterministic receive
  88 -------------------------------
  89
  90 Motivational example
  91 ^^^^^^^^^^^^^^^^^^^^
  92
  93 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
  94 between your host computer and the container.
  95
  96 .. code-block:: console
  97
  98   # From within the container
  99   $ cp -r /source/tuto-mc.git/* /source/tutorial/
 100   $ cd /source/tutorial/
 101
 102 Several files should have appeared in the ``~/tuto-mcsimgrid`` directory of your computer.
 103 This tutorial uses `ndet-receive-s4u.cpp <https://framagit.org/simgrid/tutorial-model-checking/-/blob/main/ndet-receive-s4u.cpp>`_,
 104 that uses the :ref:`S4U interface <S4U_doc>` of SimGrid, but we provide a
 105 `MPI version <https://framagit.org/simgrid/tutorial-model-checking/-/blob/main/ndet-receive-mpi.cpp>`_
 106 if you prefer (see below for details on using the MPI version).
 107
 108 .. toggle-header::
 109    :header: Code of ``ndet-receive-s4u.cpp``: click here to open
 110
 111    You can also `view it online <https://framagit.org/simgrid/tutorial-model-checking/-/blob/main/ndet-receive-s4u.cpp>`_
 112
 113    .. literalinclude:: tuto_mc/ndet-receive-s4u.cpp
 114       :language: cpp
 115
 116 |br|
 117 The provided code is rather simple: Three ``client`` are launched with an integer from ``1, 2, 3`` as a parameter. These actors simply
 118 send their parameter to a given mailbox. A ``server`` receives 3 messages and assumes that the last received message is the number ``3``.
 119 If you compile and run it, it simply works:
 120
 121 .. code-block:: console
 122
 123    $ cmake . && make
 124    (output omitted)
 125    $ ./ndet-receive-s4u small_platform.xml
 126    [Jupiter:client:(2) 0.000000] [example/INFO] Sending 1
 127    [Bourassa:client:(3) 0.000000] [example/INFO] Sending 2
 128    [Ginette:client:(4) 0.000000] [example/INFO] Sending 3
 129    [Jupiter:client:(2) 0.020516] [example/INFO] Sent!
 130    [Bourassa:client:(3) 0.047027] [example/INFO] Sent!
 131    [Ginette:client:(4) 0.064651] [example/INFO] Sent!
 132    [Tremblay:server:(1) 0.064651] [example/INFO] OK
 133
 134 Running and understanding Mc SimGrid
 135 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 136
 137 If you think of it, that's weird that this code works: all the messages are sent at the exact same time (t=0), so there is no reason for
 138 the message ``3`` to arrive last. Depending on the link speed, any order should be possible. To trigger the bug, you could fiddle with the
 139 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
 140 all message orders. For that, you simply launch your simulation as a parameter to the ``simgrid-mc`` binary as you would do with ``valgrind``:
 141
 142 .. code-block:: console
 143
 144    $ simgrid-mc ./ndet-receive-s4u small_platform.xml
 145    (some output ignored)
 146    [Tremblay:server:(1) 0.000000] (...) Assertion value_got == 3 failed
 147    (more output ignored)
 148
 149 If it fails with the error ``[root/CRITICAL] Could not wait for the model-checker.``, you need to explicitly add the PTRACE capability to
 150 your docker. Restart your docker with the additional parameter ``--cap-add SYS_PTRACE``.
 151
 152 At the end, it works: Mc SimGrid successfully triggers the bug. But the produced output is somewhat long and hairy. Don't worry, we will
 153 now read it together. It can be split in several parts:
 154
 155 - First, you have some information coming from the application.
 156
 157   - On top, you see the output of the application, but somewhat stuttering. This is exactly what happens: since Mc SimGrid is exploring
 158     all possible outcome of the code, the execution is sometimes rewind to explore another possible branch (here: another possible
 159     message ordering). Note also that all times are always 0 in the model checker, since the time is abstracted away in this mode.
 160
 161     .. code-block:: console
 162
 163        [0.000000] [mc_safety/INFO] Check a safety property. Reduction is: dpor.
 164        [Jupiter:client:(2) 0.000000] [example/INFO] Sending 1
 165        [Bourassa:client:(3) 0.000000] [example/INFO] Sending 2
 166        [Ginette:client:(4) 0.000000] [example/INFO] Sending 3
 167        [Jupiter:client:(2) 0.000000] [example/INFO] Sent!
 168        [Bourassa:client:(3) 0.000000] [example/INFO] Sent!
 169        [Tremblay:server:(1) 0.000000] [example/INFO] OK
 170        [Ginette:client:(4) 0.000000] [example/INFO] Sent!
 171        [Jupiter:client:(2) 0.000000] [example/INFO] Sent!
 172        [Bourassa:client:(3) 0.000000] [example/INFO] Sent!
 173        [Jupiter:client:(2) 0.000000] [example/INFO] Sent!
 174        [Bourassa:client:(3) 0.000000] [example/INFO] Sent!
 175        [Tremblay:server:(1) 0.000000] [example/INFO] OK
 176        [Ginette:client:(4) 0.000000] [example/INFO] Sent!
 177        [Jupiter:client:(2) 0.000000] [example/INFO] Sent!
 178        [Bourassa:client:(3) 0.000000] [example/INFO] Sent!
 179        [Jupiter:client:(2) 0.000000] [example/INFO] Sent!
 180
 181   - 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
 182     the backtrace are useful, and some are omitted here.
 183
 184     .. code-block:: console
 185
 186        [Tremblay:server:(1) 0.000000] /source/tutorial/ndet-receive-s4u.cpp:27: [root/CRITICAL] Assertion value_got == 3 failed
 187        Backtrace (displayed in actor server):
 188          ->  0# xbt_backtrace_display_current at /source/simgrid.git/src/xbt/backtrace.cpp:30
 189          ->  1# server() at /source/tutorial/ndet-receive-s4u.cpp:27
 190
 191 -  After that comes a lot of information from the model-checker.
 192
 193   - First, the error message itself. The ``xbt_assert`` in the code result in an ``abort()`` in the application, that is interpreted as an
 194     application crash by the model-checker.
 195
 196     .. code-block:: console
 197
 198        [0.000000] [mc_ModelChecker/INFO] **************************
 199        [0.000000] [mc_ModelChecker/INFO] ** CRASH IN THE PROGRAM **
 200        [0.000000] [mc_ModelChecker/INFO] **************************
 201        [0.000000] [mc_ModelChecker/INFO] From signal: Aborted
 202        [0.000000] [mc_ModelChecker/INFO] A core dump was generated by the system.
 203
 204   - An execution trace is then given, listing all the actions that led to that faulty execution. This is not easy to read, because the API
 205     calls we made (put/get) are split in atomic calls (iSend+Wait/iRecv+Wait), and all executions are interleaved. Also, Mc SimGrid
 206     reports the first faulty execution it finds: it may not be the shorter possible one.
 207
 208     .. code-block:: console
 209
 210        [0.000000] [mc_ModelChecker/INFO] Counter-example execution trace:
 211        [0.000000] [mc_ModelChecker/INFO]   1: iRecv(mbox=0)
 212        [0.000000] [mc_ModelChecker/INFO]   2: iSend(mbox=0)
 213        [0.000000] [mc_ModelChecker/INFO]   1: WaitComm(from 2 to 1, mbox=0, no timeout)
 214        [0.000000] [mc_ModelChecker/INFO]   1: iRecv(mbox=0)
 215        [0.000000] [mc_ModelChecker/INFO]   2: WaitComm(from 2 to 1, mbox=0, no timeout)
 216        [0.000000] [mc_ModelChecker/INFO]   4: iSend(mbox=0)
 217        [0.000000] [mc_ModelChecker/INFO]   1: WaitComm(from 4 to 1, mbox=0, no timeout)
 218        [0.000000] [mc_ModelChecker/INFO]   1: iRecv(mbox=0)
 219        [0.000000] [mc_ModelChecker/INFO]   3: iSend(mbox=0)
 220        [0.000000] [mc_ModelChecker/INFO]   1: WaitComm(from 3 to 1, mbox=0, no timeout)
 221
 222   - Then, the execution path is given.
 223
 224     .. code-block:: console
 225
 226        [0.000000] [mc_record/INFO] Path = 1;2;1;1;2;4;1;1;3;1
 227
 228     This is the magical string (here: ``1;2;1;1;2;4;1;1;3;1``) that you should pass to your simulator to follow the same execution path
 229     without ``simgrid-mc``. This is because ``simgrid-mc`` forbids to use a debugger such as gdb or valgrind on the code during the
 230     model-checking. For example, you can trigger the same execution in valgrind as follows:
 231
 232     .. code-block:: console
 233
 234        $ valgrind ./ndet-receive-s4u small_platform.xml --cfg=model-check/replay:'1;2;1;1;2;4;1;1;3;1'
 235        ==402== Memcheck, a memory error detector
 236        ==402== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
 237        ==402== Using Valgrind-3.16.1 and LibVEX; rerun with -h for copyright info
 238        ==402== Command: ./ndet-receive-s4u small_platform.xml --cfg=model-check/replay:1;2;1;1;2;4;1;1;3;1
 239        ==402==
 240        [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/replay' to '1;2;1;1;2;4;1;1;3;1'
 241        [0.000000] [mc_record/INFO] path=1;2;1;1;2;4;1;1;3;1
 242        [Jupiter:client:(2) 0.000000] [example/INFO] Sending 1
 243        [Bourassa:client:(3) 0.000000] [example/INFO] Sending 2
 244        [Ginette:client:(4) 0.000000] [example/INFO] Sending 3
 245        [Jupiter:client:(2) 0.000000] [example/INFO] Sent!
 246        [Tremblay:server:(1) 0.000000] /source/tutorial/ndet-receive-s4u.cpp:27: [root/CRITICAL] Assertion value_got == 3 failed
 247        (some output ignored)
 248        ==402==
 249        ==402== Process terminating with default action of signal 6 (SIGABRT): dumping core
 250        ==402==    at 0x550FCE1: raise (raise.c:51)
 251        ==402==    by 0x54F9536: abort (abort.c:79)
 252        ==402==    by 0x10C696: server() (ndet-receive-s4u.cpp:27)
 253        (more valgrind output ignored)
 254
 255   - Then, Mc SimGrid displays some statistics about the amount of expanded states (the unique states in which your program was at a given
 256     point of the exploration), the visited states (the amount of times we visited another state -- the same state may have been visited
 257     several times) and the amount of transitions.
 258
 259     .. code-block:: console
 260
 261        [0.000000] [mc_dfs/INFO] DFS exploration ended. 22 unique states visited; 4 backtracks (56 transition replays, 30 states visited overall)
 262
 263   - Finally, the application stack trace is displayed as the model-checker sees it. It should be the same as the one displayed from the
 264     application side, unless you found a bug our tools.
 265
 266 Using MPI instead of S4U
 267 ^^^^^^^^^^^^^^^^^^^^^^^^
 268
 269 If you prefer, you can use MPI instead of the SimGrid-specific interface. Inspect the provided ``ndet-receive-mpi.c`` file: that's just a
 270 translation of ``ndet-receive-s4u.cpp`` to MPI.
 271
 272 .. toggle-header::
 273    :header: Code of ``ndet-receive-mpi.c``: click here to open
 274
 275    You can also `view it online <https://framagit.org/simgrid/tutorial-model-checking/-/blob/main/ndet-receive-mpi.c>`_.
 276
 277    .. literalinclude:: tuto_mc/ndet-receive-mpi.c
 278       :language: cpp
 279
 280 |br|
 281 You can compile and run it on top of SimGrid as follows.
 282
 283 .. code-block:: console
 284
 285    $ smpicc ndet-receive-mpi.c -o ndet-receive-mpi
 286    $ smpirun -np 4 -platform small_platform.xml ndet-receive-mpi
 287
 288 Interestingly enough, the bug is triggered on my machine even without Mc SimGrid, because the simulator happens to use the execution path
 289 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
 290 should use Mc SimGrid to exhaustively explore the state space and trigger the bug in all cases.
 291
 292 .. code-block:: console
 293
 294    $ smpirun -wrapper simgrid-mc -np 4 -platform small_platform.xml ndet-receive-mpi
 295
 296 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
 297 can also trigger a given execution path out of the model-checker, for example to explore it with valgrind.
 298
 299 .. code-block:: console
 300
 301    $ 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
 302
 303 Under the hood
 304 ^^^^^^^^^^^^^^
 305
 306 If you want to run such analysis on your own code, out of the provided docker, there is some steps that you should take.
 307
 308 - SimGrid should naturally :ref:`be compiled <install_src>` with model-checking support. This requires a full set of dependencies
 309   (documented on the :ref:`relevant page <install_src>`) and should not be activated by default as there is a small performance penalty for
 310   codes using a SimGrid with MC enabled (even if you don't activate the model-checking at run time).
 311 - Also install ``libboost-stacktrace-dev`` to display nice backtraces from the application side (the one from the model-checking side is
 312   available in any case, but it contains less details).
 313 - Mc SimGrid uses the ``ptrace`` system call to spy on the verified application. Some versions of Docker forbid the use of this call by
 314   default for security reason (it could be used to escape the docker containment with older versions of Linux). If you encounter this
 315   issue, you should either update your settings (the security issue was solved in later versions of Linux), or add ``--cap-add
 316   SYS_PTRACE`` to the docker parameters, as hinted by the text.
 317
 318 Going further
 319 -------------
 320
 321 This tutorial is not complete yet, as there is nothing on reduction
 322 techniques. For now, the best source of
 323 information on these topics is `this old tutorial
 324 <https://simgrid.org/tutorials/simgrid-mc-101.pdf>`_ and `that old
 325 presentation
 326 <http://people.irisa.fr/Martin.Quinson/blog/2018/0123/McSimGrid-Boston.pdf>`_. But be warned that these source of
 327 information are very old: the liveness verification was removed in v3.35, even if these docs still mention it.
 328
 329 .. |br| raw:: html
 330
 331    <br />