-/*! \page options Simgrid options and configurations
+/*! \page options Step 2: Configure SimGrid
A number of options can be given at runtime to change the default
SimGrid behavior. For a complete list of all configuration options
here may not be available in your simulators, depending on the
@ref install_src_config "compile-time options" that you used.
+\tableofcontents
+
\section options_using Passing configuration options to the simulators
There is several way to pass configuration options to the simulators.
- \b LV08 (default one): Realistic network analytic model
(slow-start modeled by multiplying latency by 10.4, bandwidth by
.92; bottleneck sharing uses a payload of S=8775 for evaluating RTT)
- - \b Constant: Simplistic network model where all communication
+ - \anchor options_model_select_network_constant \b Constant: Simplistic network model where all communication
take a constant time (one second). This model provides the lowest
realism, but is (marginally) faster.
- \b SMPI: Realistic network model specifically tailored for HPC
\subsubsection options_model_network_coord Coordinated-based network models
When you want to use network coordinates, as it happens when you use
-an \<AS\> in your platform file with \c Vivaldi as a routing, you must
+an \<AS\> in your platform file with \c Vivaldi as a routing (see also
+Section \ref pf_routing_model_vivaldi "Vivaldi Routing Model"), you must
set the \b network/coordinates to \c yes so that all mandatory
initialization are done in the simulator.
\section options_modelchecking Configuring the Model-Checking
-To enable the experimental SimGrid model-checking support the program should
-be executed with the command line argument
+To enable the SimGrid model-checking support the program should
+be executed using the simgrid-mc wrapper:
\verbatim
---cfg=model-check:1
+simgrid-mc ./my_program
\endverbatim
Safety properties are expressed as assertions using the function
--cfg=model-check/property:<filename>
\endverbatim
-Of course, specifying a liveness property enables the model-checking
-so that you don't have to give <tt>--cfg=model-check:1</tt> in
-addition.
-
\subsection options_modelchecking_steps Going for stateful verification
By default, the system is backtracked to its initial state to explore
--cfg=model-check/checkpoint:1
\endverbatim
-Of course, specifying this option enables the model-checking so that
-you don't have to give <tt>--cfg=model-check:1</tt> in addition.
-
\subsection options_modelchecking_reduction Specifying the kind of reduction
The main issue when using the model-checking is the state space
* 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 <tt>--cfg=model-check:1</tt> in
-addition.
-
\subsection options_modelchecking_visited model-check/visited, Cycle detection
In order to detect cycles, the model-checker needs to check if a new explored
To disable the benchmarking/simulation of computation in the simulated
application, the variable \b
-smpi/simulation_computation should be set to no
+smpi/simulate_computation should be set to no
\subsection options_model_smpi_bw_factor smpi/bw_factor: Bandwidth factors
- \c smpi/privatize_global_variables: \ref options_smpi_global
- \c smpi/running_power: \ref options_smpi_bench
- \c smpi/send_is_detached_thresh: \ref options_model_smpi_detached
-- \c smpi/simulation_computation: \ref options_smpi_bench
+- \c smpi/simulate_computation: \ref options_smpi_bench
- \c smpi/test: \ref options_model_smpi_test
- \c smpi/use_shared_malloc: \ref options_model_smpi_use_shared_malloc
- \c smpi/wtime: \ref options_model_smpi_wtime