X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/dd49f9d0ff63334f76e12446cd8076edef85c508..51e5a45d4be05b7c01d28ce109505cd5e7444e46:/docs/source/Configuring_SimGrid.rst

diff --git a/docs/source/Configuring_SimGrid.rst b/docs/source/Configuring_SimGrid.rst
index 45a12bce01..72d4c516a8 100644
--- a/docs/source/Configuring_SimGrid.rst
+++ b/docs/source/Configuring_SimGrid.rst
@@ -684,16 +684,20 @@ setting for your specific system.
 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:
 
- - **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`
@@ -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.
 
+.. _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)
@@ -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.)
 
-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: