X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/66a04c68ab4c5135a15505ca5484eb8c4e7cdca6..f8b695bfe0ee01d0295c3e5caddf496e7801918a:/doc/user_guide/doxygen/options.doc diff --git a/doc/user_guide/doxygen/options.doc b/doc/user_guide/doxygen/options.doc index c1d2409338..4fb36d4950 100644 --- a/doc/user_guide/doxygen/options.doc +++ b/doc/user_guide/doxygen/options.doc @@ -46,7 +46,7 @@ currently used in SimGrid. \code extern xbt_cfg_t _surf_cfg_set; int main(int argc, char *argv[]) { - MSG_global_init(&argc, argv); + MSG_init(&argc, argv); xbt_cfg_set_parse(_surf_cfg_set,"Item:Value"); @@ -157,7 +157,7 @@ complicated pattern aiming at following the actual dependencies. The analytical models handle a lot of floating point values. It is possible to change the epsilon used to update and compare them through -the \b maxmin/precision item (default value: 1e-9). Changing it +the \b maxmin/precision item (default value: 0.00001). Changing it may speedup the simulation by discarding very small actions, at the price of a reduced numerical precision. @@ -262,11 +262,70 @@ be executed with the command line argument \verbatim --cfg=model-check:1 \endverbatim -Properties are expressed as assertions using the function +Safety properties are expressed as assertions using the function \verbatim void MC_assert(int prop); \endverbatim +\subsection options_modelchecking_liveness Specifying a liveness property + +If you want to specify liveness properties (beware, that's +experimental), you have to pass them on the command line, specifying +the name of the file containing the property, as formated by the +ltl2ba program. + +\verbatim +--cfg=model-check/property: +\endverbatim + +Of course, specifying a liveness property enables the model-checking +so that you don't have to give --cfg=model-check:1 in +addition. + +\subsection options_modelchecking_steps Going for stateful verification + +By default, the system is backtracked to its initial state to explore +another path instead of backtracking to the exact step before the fork +that we want to explore (this is called stateless verification). This +is done this way because saving intermediate states can rapidly +exhaust the available memory. If you want, you can change the value of +the model-check/checkpoint variable. For example, the +following configuration will ask to take a checkpoint every step. +Beware, this will certainly explode your memory. Larger values are +probably better, make sure to experiment a bit to find the right +setting for your specific system. + +\verbatim +--cfg=model-check/checkpoint:1 +\endverbatim + +Of course, specifying this option enables the model-checking so that +you don't have to give --cfg=model-check:1 in addition. + +\subsection options_modelchecking_reduction Specifying the kind of reduction + +The main issue when using the model-checking is the state space +explosion. To counter that problem, several exploration reduction +techniques can be used. There is unfortunately no silver bullet here, +and the most efficient reduction techniques cannot be applied to any +properties. In particular, the DPOR method cannot be applied on +liveness properties since it may break some cycles in the exploration +that are important to the property validity. + +\verbatim +--cfg=model-check/reduction: +\endverbatim + +For now, this configuration variable can take 2 values: + * none: Do not apply any kind of reduction (mandatory for now for + liveness properties) + * dpor: Apply Dynamic Partial Ordering Reduction. Only valid if you + verify local safety properties. + +Of course, specifying a reduction technique enables the model-checking +so that you don't have to give --cfg=model-check:1 in +addition. + \section options_virt Configuring the User Process Virtualization \subsection options_virt_factory Selecting the virtualization factory @@ -389,6 +448,25 @@ smpirun -trace ... simulation with --cfg=tracing:1 and --cfg=tracing/smpi:1. Check the smpirun's -help parameter for additional tracing options. +Sometimes you might want to put additional information on the trace to +correctly identify them later, or to provide data that can be used to +reproduce an experiment. You have two ways to do that: + +- Add a string on top of the trace file as comment: +\verbatim +--cfg=tracing/comment:my_simulation_identifier +\endverbatim + +- Add the contents of a textual file on top of the trace file as comment: +\verbatim +--cfg=tracing/comment_file:my_file_with_additional_information.txt +\endverbatim + +Please, use these two parameters (for comments) to make reproducible +simulations. For additional details about this and all tracing +options, check See the \ref tracing_tracing_options "Tracing +Configuration Options subsection". + \section options_smpi Configuring SMPI The SMPI interface provides several specific configuration items. @@ -447,6 +525,12 @@ code, but it can reveal troublesome in some cases (such as when the amount of processes becomes really big). This behavior is disabled when \b verbose-exit is set to 0 (it is to 1 by default). + +\section options_log Logging Configuration + +It can be done by using XBT. Go to \ref XBT_log for more details. + + \section options_index Index of all existing configuration items - \c contexts/factory: \ref options_virt_factory @@ -464,6 +548,11 @@ when \b verbose-exit is set to 0 (it is to 1 by default). - \c maxmin/precision: \ref options_model_precision +- \c model-check: \ref options_modelchecking +- \c model-check/property: \ref options_modelchecking_liveness +- \c model-check/checkpoint: \ref options_modelchecking_steps +- \c model-check/reduce: \ref options_modelchecking_reduction + - \c network/bandwidth_factor: \ref options_model_network_coefs - \c network/coordinates: \ref options_model_network_coord - \c network/crosstraffic: \ref options_model_network_crosstraffic