undo changelog modification

[simgrid.git] / docs / source / Configuring_SimGrid.rst

diff --git a/docs/source/Configuring_SimGrid.rst b/docs/source/Configuring_SimGrid.rst
index b0167728db1849917e894fbffcc7cab5816fcdc8..72d4c516a87bf9aa041328275af8bc8f38614f38 100644 (file)
--- a/docs/source/Configuring_SimGrid.rst
+++ b/docs/source/Configuring_SimGrid.rst
@@ -547,12 +547,12 @@ are meant to be detached as well.
 Configuring ns-3
 ^^^^^^^^^^^^^^^^
 
 Configuring ns-3
 ^^^^^^^^^^^^^^^^
 

-**Option** ``ns3/TcpModel`` **Default:** "default" (ns-3 default)
+**Option** ``ns3/NetworkModel`` **Default:** "default" (ns-3 default TCP)

 
 

-When using ns-3, there is an extra item ``ns3/TcpModel``, corresponding
-to the ``ns3::TcpL4Protocol::SocketType`` configuration item in
-ns-3. The only valid values (enforced on the SimGrid side) are
-'default' (no change to the ns-3 configuration), 'NewReno' or 'Cubic'.
+When using ns-3, the item ``ns3/NetworkModel`` can be used to switch between TCP or UDP, and switch the used TCP variante. If
+the item is left unchanged, ns-3 uses the default TCP implementation. With a value of "UDP", ns-3 is set to use UDP instead.
+With the value of either 'NewReno' or 'Cubic', the ``ns3::TcpL4Protocol::SocketType`` configuration item in ns-3 is set to the
+corresponding protocol.

 
 **Option** ``ns3/seed`` **Default:** "" (don't set the seed in ns-3)
 
 
 **Option** ``ns3/seed`` **Default:** "" (don't set the seed in ns-3)
 


@@ -684,16 +684,20 @@ setting for your specific system.
 Specifying the kind of reduction
 ................................
 
 Specifying the kind of reduction
 ................................
 

+**Option** model-check/reduction **Default:** "dpor"
+

 The main issue when using the model-checking is the state space
 explosion. You can activate some reduction technique with
 ``--cfg=model-check/reduction:<technique>``. For now, this
 configuration variable can take 2 values:
 
 The main issue when using the model-checking is the state space
 explosion. You can activate some reduction technique with
 ``--cfg=model-check/reduction:<technique>``. For now, this
 configuration variable can take 2 values:
 

- - **none:** Do not apply any kind of reduction (mandatory for
-   liveness properties, as our current DPOR algorithm breaks cycles)
- - **dpor:** Apply Dynamic Partial Ordering Reduction. Only valid if
-   you verify local safety properties (default value for safety
-   checks).
+ - **none:** Do not apply any kind of reduction (mandatory for liveness properties, as our current DPOR algorithm breaks cycles)
+ - **dpor:** Apply Dynamic Partial Ordering Reduction. Only valid if you verify local safety properties (default value for
+   safety checks).
+ - **sdpor:** Source-set DPOR, as described in "Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction"
+    by Abdulla et al.
+ - **odpor:** Optimal DPOR, as described in "Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction"
+    by Abdulla et al.

 
 Another way to mitigate the state space explosion is to search for
 cycles in the exploration with the :ref:`cfg=model-check/visited`
 
 Another way to mitigate the state space explosion is to search for
 cycles in the exploration with the :ref:`cfg=model-check/visited`


@@ -705,6 +709,27 @@ currently improving its efficiency (both in term of reduction ability
 and computational speed), and future work could make it compatible
 with liveness properties.
 
 and computational speed), and future work could make it compatible
 with liveness properties.
 

+.. _cfg=model-check/strategy:
+
+Guiding strategy
+................
+
+**Option** model-check/strategy **Default:** "none"
+
+Even after the DPOR's reduction, the state space that we have to explore remains huge. SimGrid provides several guiding
+strategies aiming at converging faster toward bugs. By default, none of these strategy is enabled, and SimGrid does a regular
+DFS exploration.
+
+ - **max_match_comm**: Try to minimize the number of in-fly communication by appairing matching send and receive. This tend to
+   produce nicer backtraces, in particular when a user-level ``send`` is broken down internally into a ``send_async`` + ``wait``.
+   This strategy will ensure that the ``wait`` occures as soon as possible, easing the understanding of the user who do not
+   expect her ``send`` to be split.
+ - **min_match_comm**: Try to maximize the number of in-fly communication by not appairing matching send and receive. This is
+   the exact opposite strategy, but it is still useful as it tend to explore first the branches where the risk of deadlock is
+   higher.
+ - **uniform**: this is a boring random strategy where choices are based on a uniform sampling of possible choices.
+   Surprisingly, it gives really really good results.
+

 .. _cfg=model-check/visited:
 
 Size of Cycle Detection Set (state equality reduction)
 .. _cfg=model-check/visited:
 
 Size of Cycle Detection Set (state equality reduction)


@@ -1329,12 +1354,10 @@ existing MPI libraries. The ``smpi/coll-selector`` item can be used to
 select the decision logic either of the OpenMPI or the MPICH libraries. (By
 default SMPI uses naive version of collective operations.)
 
 select the decision logic either of the OpenMPI or the MPICH libraries. (By
 default SMPI uses naive version of collective operations.)
 

-Each collective operation can be manually selected with a
-``smpi/collective_name:algo_name``. Available algorithms are listed in
-:ref:`SMPI_use_colls`.
-
-.. TODO:: All available collective algorithms will be made available
-          via the ``smpirun --help-coll`` command.
+Each collective operation can be manually selected with a ``smpi/collective_name:algo_name``. For example, if you want to use
+the Bruck algorithm for the Alltoall algorithm, you should use ``--cfg=smpi/alltoall:bruck`` on the command-line of smpirun. The
+reference of all available algorithms are listed in :ref:`SMPI_use_colls`, and you can get the full list implemented in your
+version using ``smpirun --help-coll``.

 
 .. _cfg=smpi/barrier-collectives:
 
 
 .. _cfg=smpi/barrier-collectives: