+\subsection options_modelchecking_comm_determinism Communication determinism
+
+The \b model-check/communications_determinism and
+\b model-check/send_determinism items can be used to select the communication
+determinism mode of the model-checker which checks determinism properties of
+the communications of an application.
+
+\subsection options_modelchecking_sparse_checkpoint Per page checkpoints
+
+When the model-checker is configured to take a snapshot of each explored state
+(with the \b model-checker/visited item), the memory consumption can rapidly
+reach GiB ou Tib of memory. However, for many workloads, the memory does not
+change much between different snapshots and taking a complete copy of each
+snapshot is a waste of memory.
+
+The \b model-check/sparse-checkpoint option item can be set to \b yes in order
+to avoid making a complete copy of each snapshot: instead, each snapshot will be
+decomposed in blocks which will be stored separately.
+If multiple snapshots share the same block (or if the same block
+is used in the same snapshot), the same copy of the block will be shared leading
+to a reduction of the memory footprint.
+
+For many applications, this option considerably reduces the memory consumption.
+In somes cases, the model-checker might be slightly slower because of the time
+taken to manage the metadata about the blocks. In other cases however, this
+snapshotting strategy will be much faster by reducing the cache consumption.
+When the memory consumption is important, by avoiding to hit the swap or
+reducing the swap usage, this option might be much faster than the basic
+snapshotting strategy.
+
+This option is currently disabled by default.
+
+\subsection options_mc_perf Performance considerations for the model checker
+
+The size of the stacks can have a huge impact on the memory
+consumption when using model-checking. By default, each snapshot will
+save a copy of the whole stacks and not only of the part which is
+really meaningful: you should expect the contribution of the memory
+consumption of the snapshots to be \f$ \mbox{number of processes}
+\times \mbox{stack size} \times \mbox{number of states} \f$.
+
+The \b model-check/sparse-checkpoint can be used to reduce the memory
+consumption by trying to share memory between the different snapshots.
+
+When compiled against the model checker, the stacks are not
+protected with guards: if the stack size is too small for your
+application, the stack will silently overflow on other parts of the
+memory.
+
+\subsection options_recordreplay Record/replay
+
+As the model-checker keeps jumping at different places in the execution graph,
+it is difficult to understand what happens when trying to debug an application
+under the model-checker. Event the output of the program is difficult to
+interpret. Moreover, the model-checker does not behave nicely with advanced
+debugging tools such as valgrind. For those reason, to identify a trajectory
+in the execution graph with the model-checker and replay this trajcetory and
+without the model-checker black-magic but with more standard tools
+(such as a debugger, valgrind, etc.). For this reason, Simgrid implements an
+experimental record/replay functionnality in order to record a trajectory with
+the model-checker and replay it without the model-checker.
+
+When the model-checker finds an interesting path in the application execution
+graph (where a safety or liveness property is violated), it can generate an
+identifier for this path. In order to enable this behavious the
+\b model-check/record must be set to \b yes. By default, this behaviour is not
+enabled.
+
+This is an example of output:
+
+<pre>
+[ 0.000000] (0:@) Check a safety property
+[ 0.000000] (0:@) **************************
+[ 0.000000] (0:@) *** PROPERTY NOT VALID ***
+[ 0.000000] (0:@) **************************
+[ 0.000000] (0:@) Counter-example execution trace:
+[ 0.000000] (0:@) Path = 1/3;1/4
+[ 0.000000] (0:@) [(1)Tremblay (app)] MC_RANDOM(3)
+[ 0.000000] (0:@) [(1)Tremblay (app)] MC_RANDOM(4)
+[ 0.000000] (0:@) Expanded states = 27
+[ 0.000000] (0:@) Visited states = 68
+[ 0.000000] (0:@) Executed transitions = 46
+</pre>
+
+This path can then be replayed outside of the model-checker (and even in
+non-MC build of simgrid) by setting the \b model-check/replay item to the given
+path. The other options should be the same (but the model-checker should
+be disabled).
+
+The format and meaning of the path may change between different releases so
+the same release of Simgrid should be used for the record phase and the replay
+phase.
+