New MC option: smpi/buffering, to control MPI buffering

diff --git a/ChangeLog b/ChangeLog
index 4614f28..b064546 100644 (file)
--- a/ChangeLog
+++ b/ChangeLog
@@ -22,6 +22,7 @@ SMPI:
 
 Model-Checker:
  - Option model-checker/hash was removed. This is always activated now.
 
 Model-Checker:
  - Option model-checker/hash was removed. This is always activated now.

+ - New option smpi/buffering controls the MPI buffering in MC mode.

  - MPI calls now MC_assert() that no MPI_ERR_* code is returned. 
    This is useful to check for MPI compliance.
 
  - MPI calls now MC_assert() that no MPI_ERR_* code is returned. 
    This is useful to check for MPI compliance.
 

diff --git a/docs/source/Configuring_SimGrid.rst b/docs/source/Configuring_SimGrid.rst
index 3a9b16f..0959b78 100644 (file)
--- a/docs/source/Configuring_SimGrid.rst
+++ b/docs/source/Configuring_SimGrid.rst
@@ -140,6 +140,7 @@ Existing Configuration Items
 
 - **For collective operations of SMPI,** please refer to Section :ref:`cfg=smpi/coll-selector`
 - **smpi/async-small-thresh:** :ref:`cfg=smpi/async-small-thresh`
 
 - **For collective operations of SMPI,** please refer to Section :ref:`cfg=smpi/coll-selector`
 - **smpi/async-small-thresh:** :ref:`cfg=smpi/async-small-thresh`

+- **smpi/buffering:** :ref:`cfg=smpi/buffering`

 - **smpi/bw-factor:** :ref:`cfg=smpi/bw-factor`
 - **smpi/coll-selector:** :ref:`cfg=smpi/coll-selector`
 - **smpi/comp-adjustment-file:** :ref:`cfg=smpi/comp-adjustment-file`
 - **smpi/bw-factor:** :ref:`cfg=smpi/bw-factor`
 - **smpi/coll-selector:** :ref:`cfg=smpi/coll-selector`
 - **smpi/comp-adjustment-file:** :ref:`cfg=smpi/comp-adjustment-file`


@@ -484,6 +485,32 @@ be executed using the simgrid-mc wrapper:
 Safety properties are expressed as assertions using the function
 :cpp:func:`void MC_assert(int prop)`.
 
 Safety properties are expressed as assertions using the function
 :cpp:func:`void MC_assert(int prop)`.
 

+.. _cfg=smpi/buffering:
+
+Specifying the MPI buffering behavior
+.....................................
+
+**Option** ``smpi/buffering`` **Default:** zero
+
+Buffering in MPI has a huge impact on the communication semantic. For example,
+standard blocking sends are synchronous calls when the system buffers are full
+while these calls can complete immediately without even requiring a matching
+receive call for small messages sent when the system buffers are empty.
+
+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.
+- 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.
+
+The ``smpi/buffering`` option gives an easier interface to choose between these semantics. It can take two values:
+
+- **zero:** means that buffering should be disabled. Blocking communications are actually blocking.
+- **infty:** means that buffering should be made infinite. Blocking communications are non-blocking.
+

 .. _cfg=model-check/property:
 
 Specifying a liveness property
 .. _cfg=model-check/property:
 
 Specifying a liveness property

diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp
index 6dd2b9f..1ab68c0 100644 (file)
--- a/src/mc/mc_config.cpp
+++ b/src/mc/mc_config.cpp
@@ -9,6 +9,8 @@
 #include "src/mc/mc_safety.hpp"
 #endif
 
 #include "src/mc/mc_safety.hpp"
 #endif
 

+#include <climits>
+

 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_config, mc, "Configuration of the Model Checker");
 
 #if SIMGRID_HAVE_MC
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_config, mc, "Configuration of the Model Checker");
 
 #if SIMGRID_HAVE_MC


@@ -71,6 +73,21 @@ simgrid::config::Flag<bool> _sg_mc_send_determinism{
       _mc_cfg_cb_check("value to enable/disable the detection of send-determinism in the communications schemes");
     }};
 
       _mc_cfg_cb_check("value to enable/disable the detection of send-determinism in the communications schemes");
     }};
 

+static simgrid::config::Flag<std::string> _sg_mc_buffering{
+    "smpi/buffering", "Buffering semantic to use for MPI (only used in MC)", "zero", [](const std::string& value) {
+      try {
+        if (value == "zero")
+          simgrid::config::set_value<int>("smpi/send-is-detached-thresh", 0);
+        else if (value == "infty")
+          simgrid::config::set_value<int>("smpi/send-is-detached-thresh", INT_MAX);
+        else
+          xbt_die("configuration option 'smpi/buffering' can only take 'zero' or 'infty' as a value");
+      } catch (std::out_of_range& e) {
+        /* If the 'smpi/send-is-detached-thresh' does not exist, we are in the MCer process, where this option makes no
+         * sense, so just ignore it */
+      }
+    }};
+

 static simgrid::config::Flag<std::string> _sg_mc_reduce{
     "model-check/reduction", "Specify the kind of exploration reduction (either none or DPOR)", "dpor",
     [](const std::string& value) {
 static simgrid::config::Flag<std::string> _sg_mc_reduce{
     "model-check/reduction", "Specify the kind of exploration reduction (either none or DPOR)", "dpor",
     [](const std::string& value) {