- **host/model:** :ref:`options_model_select`
-- **maxmin/precision:** :ref:`cfg=maxmin/precision`
- **maxmin/concurrency-limit:** :ref:`cfg=maxmin/concurrency-limit`
- **model-check:** :ref:`options_modelchecking`
- **storage/max_file_descriptors:** :ref:`cfg=storage/max_file_descriptors`
-- **surf/precision:** :ref:`cfg=surf/precision`
+- **precision/timing:** :ref:`cfg=precision/timing`
+- **precision/work-amount:** :ref:`cfg=precision/work-amount`
- **For collective operations of SMPI,** please refer to Section :ref:`cfg=smpi/coll-selector`
- **smpi/auto-shared-malloc-thresh:** :ref:`cfg=smpi/auto-shared-malloc-thresh`
and slow pattern that follows the actual dependencies.
.. _cfg=bmf/precision:
-.. _cfg=maxmin/precision:
-.. _cfg=surf/precision:
+.. _cfg=precision/timing:
+.. _cfg=precision/work-amount:
Numerical Precision
...................
-**Option** ``maxmin/precision`` **Default:** 1e-5 (in flops or bytes) |br|
-**Option** ``surf/precision`` **Default:** 1e-9 (in seconds) |br|
+**Option** ``precision/timing`` **Default:** 1e-9 (in seconds) |br|
+**Option** ``precision/work-amount`` **Default:** 1e-5 (in flops or bytes) |br|
**Option** ``bmf/precision`` **Default:** 1e-12 (no unit)
The analytical models handle a lot of floating point values. It is
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 'Reno' or
-'Tahoe'.
+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)
In SMPI, this depends on the message size, that is compared against two thresholds:
- if (size < :ref:`smpi/async-small-thresh <cfg=smpi/async-small-thresh>`) then
- MPI_Send returns immediately, even if the corresponding receive has not be issued yet.
-- if (:ref:`smpi/async-small-thresh <cfg=smpi/async-small-thresh>` < size < :ref:`smpi/send-is-detached-thresh <cfg=smpi/send-is-detached-thresh>`) then
- MPI_Send returns as soon as the corresponding receive has been issued. This is known as the eager mode.
+ MPI_Send returns immediately, and the message is sent even if the
+ corresponding receive has not be issued yet. This is known as the eager mode.
+- if (:ref:`smpi/async-small-thresh <cfg=smpi/async-small-thresh>` < size <
+ :ref:`smpi/send-is-detached-thresh <cfg=smpi/send-is-detached-thresh>`) then
+ MPI_Send also returns immediately, but SMPI waits for the corresponding
+ receive to be posted, in order to perform the communication operation.
- if (:ref:`smpi/send-is-detached-thresh <cfg=smpi/send-is-detached-thresh>` < size) then
MPI_Send returns only when the message has actually been sent over the network. This is known as the rendez-vous mode.
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`
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)
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:
