Correct a bug in kademlia

[simgrid.git] / doc / user_guide / doxygen / options.doc

diff --git a/doc/user_guide/doxygen/options.doc b/doc/user_guide/doxygen/options.doc
index c1d2409..1901e91 100644 (file)
--- 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[]) {
 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");
 
 
      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 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.
 
 may speedup the simulation by discarding very small actions, at the
 price of a reduced numerical precision.
 


@@ -234,6 +234,18 @@ the same network card through the \b network/sender_gap item. This
 is still under investigation as of writting, and the default value is
 to wait 0 seconds between emissions (no gap applied).
 
 is still under investigation as of writting, and the default value is
 to wait 0 seconds between emissions (no gap applied).
 

+\subsubsection options_model_network_asyncsend Simulating asyncronous send
+
+(this configuration item is experimental and may change or disapear)
+
+It is possible to specify that messages below a certain size will be sent 
+as soon as the call to MPI_Send is issued, without waiting for the 
+correspondant receive. This threshold can be configured through the 
+\b smpi/async_small_thres item. The default value is 0. This behavior can also be 
+manually set for MSG mailboxes, by setting the receiving mode of the mailbox 
+with a call to \ref MSG_mailbox_set_async . For MSG, all messages sent to this 
+mailbox will have this behavior, so consider using two mailboxes if needed. 
+

 \subsubsection options_pls Configuring packet-level pseudo-models
 
 When using the packet-level pseudo-models, several specific
 \subsubsection options_pls Configuring packet-level pseudo-models
 
 When using the packet-level pseudo-models, several specific


@@ -262,11 +274,70 @@ be executed with the command line argument
 \verbatim
 --cfg=model-check:1
 \endverbatim
 \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
 
 \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:<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
+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 <tt>model-check/checkpoint</tt> 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 <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
+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:<technique>
+\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 <tt>--cfg=model-check:1</tt> in
+addition.
+

 \section options_virt Configuring the User Process Virtualization
 
 \subsection options_virt_factory Selecting the virtualization factory
 \section options_virt Configuring the User Process Virtualization
 
 \subsection options_virt_factory Selecting the virtualization factory


@@ -286,21 +357,19 @@ should be the most effcient one (please report bugs if the
 auto-detection fails for you). They are sorted here from the slowest
 to the most effient:
  - \b thread: very slow factory using full featured threads (either
 auto-detection fails for you). They are sorted here from the slowest
 to the most effient:
  - \b thread: very slow factory using full featured threads (either

-   ptheads or windows native threads)
+   pthreads or windows native threads)

  - \b ucontext: fast factory using System V contexts (or a portability
    layer of our own on top of Windows fibers)
  - \b raw: amazingly fast factory using a context switching mecanism
    of our own, directly implemented in assembly (only available for x86
    and amd64 platforms for now)
 
  - \b ucontext: fast factory using System V contexts (or a portability
    layer of our own on top of Windows fibers)
  - \b raw: amazingly fast factory using a context switching mecanism
    of our own, directly implemented in assembly (only available for x86
    and amd64 platforms for now)
 

-The only reason to change this setting is when the debuging tools get
+The only reason to change this setting is when the debugging tools get

 fooled by the optimized context factories. Threads are the most
 debugging-friendly contextes.
 
 \subsection options_virt_stacksize Adapting the used stack size
 
 fooled by the optimized context factories. Threads are the most
 debugging-friendly contextes.
 
 \subsection options_virt_stacksize Adapting the used stack size
 

-(this only works if you use ucontexts or raw context factories)
-

 Each virtualized used process is executed using a specific system
 stack. The size of this stack has a huge impact on the simulation
 scalability, but its default value is rather large. This is because
 Each virtualized used process is executed using a specific system
 stack. The size of this stack has a huge impact on the simulation
 scalability, but its default value is rather large. This is because


@@ -311,7 +380,9 @@ stacks), leading to segfaults with corrupted stack traces.
 If you want to push the scalability limits of your code, you really
 want to reduce the \b contexts/stack_size item. Its default value
 is 128 (in Kib), while our Chord simulation works with stacks as small
 If you want to push the scalability limits of your code, you really
 want to reduce the \b contexts/stack_size item. Its default value
 is 128 (in Kib), while our Chord simulation works with stacks as small

-as 16 Kib, for example.
+as 16 Kib, for example. For the thread factory, the default value 
+is the one of the system, if it is too large/small, it has to be set 
+with this parameter.

 
 \subsection options_virt_parallel Running user code in parallel
 
 
 \subsection options_virt_parallel Running user code in parallel
 


@@ -389,6 +460,25 @@ smpirun -trace ...
 simulation with --cfg=tracing:1 and --cfg=tracing/smpi:1. Check the
 smpirun's <i>-help</i> parameter for additional tracing options.
 
 simulation with --cfg=tracing:1 and --cfg=tracing/smpi:1. Check the
 smpirun's <i>-help</i> 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.
 \section options_smpi Configuring SMPI
 
 The SMPI interface provides several specific configuration items.


@@ -447,6 +537,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).
 
 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
 \section options_index Index of all existing configuration items
 
 - \c contexts/factory: \ref options_virt_factory


@@ -464,6 +560,11 @@ when \b verbose-exit is set to 0 (it is to 1 by default).
 
 - \c maxmin/precision: \ref options_model_precision
 
 
 - \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
 - \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


@@ -482,6 +583,7 @@ when \b verbose-exit is set to 0 (it is to 1 by default).
 - \c smpi/running_power: \ref options_smpi_bench
 - \c smpi/display_timing: \ref options_smpi_timing
 - \c smpi/cpu_threshold: \ref options_smpi_bench
 - \c smpi/running_power: \ref options_smpi_bench
 - \c smpi/display_timing: \ref options_smpi_timing
 - \c smpi/cpu_threshold: \ref options_smpi_bench

+- \c smpi/async_small_thres: \ref options_model_network_asyncsend

 
 - \c path: \ref options_generic_path
 - \c verbose-exit: \ref options_generic_exit
 
 - \c path: \ref options_generic_path
 - \c verbose-exit: \ref options_generic_exit