From 04d1dd3b085e748d258f896c55ebd3b3a3b9c6c2 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Tue, 26 May 2015 15:31:58 +0200 Subject: [PATCH] [mc][doc] Record/replay and sparse snapshots --- doc/doxygen/options.doc | 91 ++++++++++++++++++++++++++++++++++++++--- 1 file changed, 86 insertions(+), 5 deletions(-) diff --git a/doc/doxygen/options.doc b/doc/doxygen/options.doc index daa8c81712..c2fc2df410 100644 --- a/doc/doxygen/options.doc +++ b/doc/doxygen/options.doc @@ -306,6 +306,7 @@ be executed with the command line argument \verbatim --cfg=model-check:1 \endverbatim + Safety properties are expressed as assertions using the function \verbatim void MC_assert(int prop); @@ -370,20 +371,99 @@ Of course, specifying a reduction technique enables the model-checking so that you don't have to give --cfg=model-check:1 in addition. +\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. Currently each snapshot, will -save a copy of the whole stack and not only of the part which is +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$. -However, when compiled against the model checker, the stacks are not +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: + +
+[  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
+
+ +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. + \section options_virt Configuring the User Process Virtualization \subsection options_virt_factory Selecting the virtualization factory @@ -824,13 +904,14 @@ silently overflow on other parts of the memory. - \c model-check: \ref options_modelchecking - \c model-check/checkpoint: \ref options_modelchecking_steps - \c model-check/communications_determinism: \ref options_modelchecking_comm_determinism +- \c model-check/communications_determinism: \ref options_modelchecking_send_determinism - \c model-check/dot_output: \ref options_modelchecking_dot_output - \c model-check/hash: \ref options_modelchecking_hash - \c model-check/property: \ref options_modelchecking_liveness - \c model-check/max_depth: \ref options_modelchecking_max_depth -- \c model-check/record: \ref options_modelchecking_record +- \c model-check/record: \ref options_modelchecking_recordreplay - \c model-check/reduction: \ref options_modelchecking_reduction -- \c model-check/replay: \ref options_modelchecking_replay +- \c model-check/replay: \ref options_modelchecking_recordreplay - \c model-check/send_determinism: \ref options_modelchecking_sparse_checkpoint - \c model-check/snapshot_fds: \ref options_modelchecking_snapshot_fds - \c model-check/sparse-checkpoint: \ref options_modelchecking_sparse_checkpoint -- 2.20.1