so that you don't have to give <tt>--cfg=model-check:1</tt> in
addition.
+\subsection options_modelchecking_visited model-check/visited, Cycle detection
+
+In order to detect cycles, the model-checker needs to check if a new explored
+state is in fact the same state than a previous one. In order to do this,
+the model-checker can take a snapshot of each visited state: this snapshot is
+then used to compare it with subsequent states in the exploration graph.
+
+The \b model-check/visited is the maximum number of states which are stored in
+memory. If the maximum number of snapshotted state is reached some states will
+be removed from the memory and some cycles might be missed.
+
+By default, no state is snapshotted and cycles cannot be detected.
+
+\subsection options_modelchecking_termination, model-check/termination, Non termination detection
+
+The \b model-check/termination configuration item can be used to report if a
+non-termination execution path has been found. This is a path with a cycle
+which means that the program might never terminate.
+
+This only works in safety mode.
+
+This options is disabled by default.
+
+\subsection options_modelchecking_dot_output model-check/dot_output, Dot output
+
+If set, the \b model-check/dot_output configuration item is the name of a file
+in which to write a dot file of the path leading the found property (safety or
+liveness violation) as well as the cycle for liveness properties. This dot file
+can then fed to the graphviz dot tool to generate an corresponding graphical
+representation.
+
+\subsection options_modelchecking_max_depth model-check/max_depth, Depth limit
+
+The \b model-checker/max_depth can set the maximum depth of the exploration
+graph of the model-checker. If this limit is reached, a logging message is
+sent and the results might not be exact.
+
+By default, there is not depth limit.
+
\subsection options_modelchecking_timeout Handling of timeout
By default, the model-checker does not handle timeout conditions: the `wait`
application, the stack will silently overflow on other parts of the
memory.
-\subsection options_recordreplay Record/replay
+\subsection options_modelchecking_hash Hashing of the state (experimental)
+
+Usually most of the time of the model-checker is spent comparing states. This
+process is complicated and consumes a lot of bandwidth and cache.
+In order to speedup the state comparison, the experimental \b model-checker/hash
+configuration item enables the computation of a hash summarizing as much
+information of the state as possible into a single value. This hash can be used
+to avoid most of the comparisons: the costly comparison is then only used when
+the hashes are identical.
+
+Currently most of the state is not included in the hash because the
+implementation was found to be buggy and this options is not as useful as
+it could be. For this reason, it is currently disabled by default.
+
+\subsection options_modelchecking_recordreplay Record/replay (experimental)
As the model-checker keeps jumping at different places in the execution graph,
it is difficult to understand what happens when trying to debug an application
When the code is constituted of numerous consecutive MPI calls, the
previous mechanism feeds the simulation kernel with numerous tiny
computations. The \b smpi/cpu_threshold item becomes handy when this
-impacts badly the simulation performance. It specify a threshold (in
-second) under which the execution chunks are not reported to the
-simulation kernel (default value: 1e-6). Please note that in some
-circonstances, this optimization can hinder the simulation accuracy.
+impacts badly the simulation performance. It specifies a threshold (in
+seconds) below which the execution chunks are not reported to the
+simulation kernel (default value: 1e-6).
+
+
+\note
+ The option smpi/cpu_threshold ignores any computation time spent
+ below this threshold. SMPI does not consider the \a amount of these
+ computations; there is no offset for this. Hence, by using a
+ value that is too low, you may end up with unreliable simulation
+ results.
In some cases, however, one may wish to disable simulation of
application computation. This is the case when SMPI is used not to
\subsection options_smpi_timing smpi/display_timing: Reporting simulation time
+\b Default: 0 (false)
+
Most of the time, you run MPI code through SMPI to compute the time it
would take to run it on a platform that you don't have. But since the
code is run through the \c smpirun script, you don't have any control
The behavior and motivation for this configuration option is identical with \a smpi/test, see
Section \ref options_model_smpi_test for details.
+\subsection options_model_smpi_ois smpi/ois: Inject constant times for asynchronous send operations
+
+This configuration option works exactly as \a smpi/os, see Section \ref options_model_smpi_os.
+Of course, \a smpi/ois is used to account for MPI_Isend instead of MPI_Send.
+
+\subsection options_model_smpi_os smpi/os: Inject constant times for send operations
+
+In several network models such as LogP, send (MPI_Send, MPI_Isend) and receive (MPI_Recv)
+operations incur costs (i.e., they consume CPU time). SMPI can factor these costs in as well, but the
+user has to configure SMPI accordingly as these values may vary by machine.
+This can be done by using smpi/os for MPI_Send operations; for MPI_Isend and
+MPI_Recv, use \a smpi/ois and \a smpi/or, respectively. These work exactly as
+\a smpi/ois.
+
+\a smpi/os can consist of multiple sections; each section takes three values, for example:
+
+\verbatim
+ 1:3:2;10:5:1
+\endverbatim
+
+Here, the sections are divided by ";" (that is, this example contains two sections).
+Furthermore, each section consists of three values.
+
+1. The first value denotes the minimum size for this section to take effect;
+ read it as "if message size is greater than this value (and other section has a larger
+ first value that is also smaller than the message size), use this".
+ In the first section above, this value is "1".
+
+2. The second value is the startup time; this is a constant value that will always
+ be charged, no matter what the size of the message. In the first section above,
+ this value is "3".
+
+3. The third value is the \a per-byte cost. That is, it is charged for every
+ byte of the message (incurring cost messageSize*cost_per_byte)
+ and hence accounts also for larger messages. In the first
+ section of the example above, this value is "2".
+
+Now, SMPI always checks which section it should take for a given message; that is,
+if a message of size 11 is sent with the configuration of the example above, only
+the second section will be used, not the first, as the first value of the second
+section is closer to the message size. Hence, a message of size 11 incurs the
+following cost inside MPI_Send:
+
+\verbatim
+ 5+11*1
+\endverbatim
+
+%As 5 is the startup cost and 1 is the cost per byte.
+
+\note
+ The order of sections can be arbitrary; they will be ordered internally.
+
+\subsection options_model_smpi_or smpi/or: Inject constant times for receive operations
+
+This configuration option works exactly as \a smpi/os, see Section \ref options_model_smpi_os.
+Of course, \a smpi/or is used to account for MPI_Recv instead of MPI_Send.
+
\subsection options_model_smpi_test smpi/test: Inject constant times for calls to MPI_Test
\b Default value: 0.0001
- \c model-check: \ref options_modelchecking
- \c model-check/checkpoint: \ref options_modelchecking_steps
- \c model-check/communications_determinism: \ref options_modelchecking_comm_determinism
-- \c model-check/communications_determinism: \ref options_modelchecking_send_determinism
+- \c model-check/send_determinism: \ref options_modelchecking_comm_determinism
- \c model-check/dot_output: \ref options_modelchecking_dot_output
- \c model-check/hash: \ref options_modelchecking_hash
- \c model-check/property: \ref options_modelchecking_liveness
- \c model-check/reduction: \ref options_modelchecking_reduction
- \c model-check/replay: \ref options_modelchecking_recordreplay
- \c model-check/send_determinism: \ref options_modelchecking_sparse_checkpoint
-- \c model-check/snapshot_fds: \ref options_modelchecking_snapshot_fds
- \c model-check/sparse-checkpoint: \ref options_modelchecking_sparse_checkpoint
- \c model-check/termination: \ref options_modelchecking_termination
- \c model-check/timeout: \ref options_modelchecking_timeout
