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 ae3a1fe8fe25bc4bf09d214990c5a0bb5c6a23da..72d4c516a87bf9aa041328275af8bc8f38614f38 100644 (file)
--- a/docs/source/Configuring_SimGrid.rst
+++ b/docs/source/Configuring_SimGrid.rst
@@ -117,7 +117,6 @@ Existing Configuration Items
 - **model-check/replay:** :ref:`cfg=model-check/replay`
 - **model-check/send-determinism:** :ref:`cfg=model-check/send-determinism`
 - **model-check/setenv:** :ref:`cfg=model-check/setenv`
-- **model-check/sleep-set:** :ref:`cfg=model-check/sleep-set`
 - **model-check/termination:** :ref:`cfg=model-check/termination`
 - **model-check/timeout:** :ref:`cfg=model-check/timeout`
 - **model-check/visited:** :ref:`cfg=model-check/visited`
@@ -685,6 +684,8 @@ 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
@@ -708,13 +709,26 @@ 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/sleep-set:
+.. _cfg=model-check/strategy:
 
-Sleep sets
-..........
+Guiding strategy
+................
 
-The performance of the DPOR algorithm is greatly improved by using sleep sets, but if you want, you can still disable it with
-this option.
+**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: