Model-checker:
- Remove option 'model-check/record': Paths are recorded in any cases now.
+ - Remove option 'model-check/sparse-checkpoint': Checkpoints are now
+ always sparse. That's an immense gain in memory, and can even be
+ faster because of cache effects. So there is no need to clutter the
+ code to allow the user to go for the unefficient mode.
Fixed bugs (FG=FramaGit; GH=GitHub):
- FG#1: Broken link in error messages
- **model-check/reduction:** :ref:`cfg=model-check/reduction`
- **model-check/replay:** :ref:`cfg=model-check/replay`
- **model-check/send-determinism:** :ref:`cfg=model-check/send-determinism`
-- **model-check/sparse-checkpoint:** :ref:`cfg=model-check/sparse-checkpoint`
- **model-check/termination:** :ref:`cfg=model-check/termination`
- **model-check/timeout:** :ref:`cfg=model-check/timeout`
- **model-check/visited:** :ref:`cfg=model-check/visited`
communication determinism mode of the model-checker which checks
determinism properties of the communications of an application.
-.. _cfg=model-check/sparse-checkpoint:
-
-Incremental Checkpoints
-.......................
-
-When the model-checker is configured to take a snapshot of each
-explored state (with the ``model-checker/visited`` item), the memory
-consumption can rapidly reach GiB ou Tib of memory. However, for many
-workloads, the memory does not change much between different snapshots
-and taking a complete copy of each snapshot is a waste of memory.
-
-The ``model-check/sparse-checkpoint`` option item can be set to
-**yes** to avoid making a complete copy of each snapshot. Instead,
-each snapshot will be decomposed in blocks which will be stored
-separately. If multiple snapshots share the same block (or if the
-same block is used in the same snapshot), the same copy of the block
-will be shared leading to a reduction of the memory footprint.
-
-For many applications, this option considerably reduces the memory
-consumption. In somes cases, the model-checker might be slightly
-slower because of the time taken to manage the metadata about the
-blocks. In other cases however, this snapshotting strategy will be
-much faster by reducing the cache consumption. When the memory
-consumption is important, by avoiding to hit the swap or reducing the
-swap usage, this option might be much faster than the basic
-snapshotting strategy.
-
-This option is currently disabled by default.
-
Verification Performance Considerations
.......................................
consumption of the snapshots to be @f$ @mbox{number of processes}
@times @mbox{stack size} @times @mbox{number of states} @f$.
-The ``model-check/sparse-checkpoint`` can be used to reduce the memory
-consumption by trying to share memory between the different snapshots.
-
When compiled against the model checker, the stacks are not
protected with guards: if the stack size is too small for your
application, the stack will silently overflow on other parts of the
ADD_TESH_FACTORIES(mc-bugged2 "ucontext;raw" --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged2.tesh)
IF(HAVE_UCONTEXT_CONTEXTS AND SIMGRID_PROCESSOR_x86_64) # liveness model-checking works only on 64bits (for now ...)
ADD_TESH(mc-bugged1-liveness-ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged1_liveness.tesh)
- ADD_TESH(mc-bugged1-liveness-ucontext-sparse --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged1_liveness_sparse.tesh)
ADD_TESH(mc-bugged1-liveness-visited-ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged1_liveness_visited.tesh)
- ADD_TESH(mc-bugged1-liveness-visited-ucontext-sparse --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged1_liveness_visited_sparse.tesh)
IF(HAVE_C_STACK_CLEANER)
# This test checks if the stack cleaner is making a difference:
ADD_TEST(mc-bugged1-liveness-stack-cleaner ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc/bugged1_liveness_stack_cleaner ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc/ ${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc/)
+++ /dev/null
-#!/usr/bin/env tesh
-
-! expect return 2
-! timeout 20
-! output ignore
-$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../../platforms/small_platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack-size:256 --cfg=model-check/sparse-checkpoint:yes --cfg=model-check/property:promela_bugged1_liveness
-> [ 0.000000] (0:maestro@) Check the liveness property promela_bugged1_liveness
-> [ 0.000000] (2:client@Boivin) Ask the request
-> [ 0.000000] (3:client@Fafard) Ask the request
-> [ 0.000000] (2:client@Boivin) Propositions changed : r=1, cs=0
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (3:client@Fafard) 2 got the answer. Sleep a bit and release it
-> [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle
-> [ 0.000000] (3:client@Fafard) Ask the request
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (0:maestro@) Pair 22 already reached (equal to pair 10) !
-> [ 0.000000] (0:maestro@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
-> [ 0.000000] (0:maestro@) | ACCEPTANCE CYCLE |
-> [ 0.000000] (0:maestro@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
-> [ 0.000000] (0:maestro@) Counter-example that violates formula :
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(3)Fafard (client)] iRecv(dst=(3)Fafard (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (3)Fafard (client)])
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(3)Fafard (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (3)Fafard (client)])
-> [ 0.000000] (0:maestro@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) Expanded pairs = 22
-> [ 0.000000] (0:maestro@) Visited pairs = 20
-> [ 0.000000] (0:maestro@) Executed transitions = 20
-> [ 0.000000] (0:maestro@) Counter-example depth : 21
+++ /dev/null
-#!/usr/bin/env tesh
-
-! expect return 2
-! timeout 20
-! output ignore
-$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../../platforms/small_platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack-size:256 --cfg=model-check/sparse-checkpoint:yes --cfg=model-check/property:promela_bugged1_liveness
-> [ 0.000000] (0:maestro@) Check the liveness property promela_bugged1_liveness
-> [ 0.000000] (2:client@Boivin) Ask the request
-> [ 0.000000] (3:client@Fafard) Ask the request
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
-> [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle
-> [ 0.000000] (2:client@Boivin) Ask the request
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
-> [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle
-> [ 0.000000] (2:client@Boivin) Ask the request
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
-> [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle
-> [ 0.000000] (2:client@Boivin) Ask the request
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
-> [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle
-> [ 0.000000] (2:client@Boivin) Ask the request
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (1:coordinator@Tremblay) CS already used. Queue the request.
-> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
-> [ 0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1)
-> [ 0.000000] (2:client@Boivin) Ask the request
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
-> [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle
-> [ 0.000000] (2:client@Boivin) Ask the request
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (1:coordinator@Tremblay) CS already used. Queue the request.
-> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
-> [ 0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1)
-> [ 0.000000] (2:client@Boivin) Ask the request
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
-> [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle
-> [ 0.000000] (2:client@Boivin) Ask the request
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (1:coordinator@Tremblay) CS already used. Queue the request.
-> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
-> [ 0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1)
-> [ 0.000000] (2:client@Boivin) Ask the request
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
-> [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle
-> [ 0.000000] (2:client@Boivin) Ask the request
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (1:coordinator@Tremblay) CS already used. Queue the request.
-> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
-> [ 0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1)
-> [ 0.000000] (2:client@Boivin) Ask the request
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
-> [ 0.000000] (3:client@Fafard) Propositions changed : r=1, cs=0
-> [ 0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1)
-> [ 0.000000] (2:client@Boivin) Ask the request
-> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it
-> [ 0.000000] (0:maestro@) Pair 58 already reached (equal to pair 46) !
-> [ 0.000000] (0:maestro@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
-> [ 0.000000] (0:maestro@) | ACCEPTANCE CYCLE |
-> [ 0.000000] (0:maestro@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
-> [ 0.000000] (0:maestro@) Counter-example that violates formula :
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)])
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)])
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)])
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)])
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)])
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)])
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] Wait(comm=(verbose only) [(2)Boivin (client)-> (1)Tremblay (coordinator)])
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] iRecv(dst=(2)Boivin (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)])
-> [ 0.000000] (0:maestro@) [(1)Tremblay (coordinator)] iRecv(dst=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)])
-> [ 0.000000] (0:maestro@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only))
-> [ 0.000000] (0:maestro@) Expanded pairs = 58
-> [ 0.000000] (0:maestro@) Visited pairs = 202
-> [ 0.000000] (0:maestro@) Executed transitions = 208
-> [ 0.000000] (0:maestro@) Counter-example depth : 51
\ No newline at end of file
"compromises between speed and memory consumption.",
0, [](int) { _mc_cfg_cb_check("checkpointing value"); }};
-simgrid::config::Flag<bool> _sg_mc_sparse_checkpoint{"model-check/sparse-checkpoint", "Use sparse per-page snapshots.",
- false, [](bool) { _mc_cfg_cb_check("checkpointing value"); }};
-
simgrid::config::Flag<std::string> _sg_mc_property_file{
"model-check/property", "Name of the file containing the property, as formatted by the ltl2ba program.", "",
[](const std::string&) { _mc_cfg_cb_check("property"); }};
extern "C" XBT_PUBLIC int _sg_do_model_check;
extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_record_path;
extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_checkpoint;
-extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_sparse_checkpoint;
extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_property_file;
extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_comms_determinism;
extern XBT_PUBLIC simgrid::config::Flag<bool> _sg_mc_send_determinism;
namespace simgrid {
namespace mc {
-RegionDense::RegionDense(RegionType region_type, void* start_addr, void* permanent_addr, size_t size)
- : RegionSnapshot(region_type, start_addr, permanent_addr, size)
-{
- flat_data_ = Buffer::malloc(size);
-
- mc_model_checker->process().read_bytes(flat_data_.get(), size, remote(permanent_addr));
-
- storage_type_ = StorageType::Flat;
- page_numbers_.clear();
-
- XBT_DEBUG("New region : type : %s, data : %p (real addr %p), size : %zu",
- (region_type == RegionType::Heap ? "Heap" : (region_type == RegionType::Data ? "Data" : "?")),
- flat_data().get(), permanent_addr, size);
-}
-
/** @brief Take a snapshot of a given region
*
* @param type
*/
RegionSnapshot* region(RegionType type, void* start_addr, void* permanent_addr, size_t size)
{
- if (_sg_mc_sparse_checkpoint)
return new RegionSparse(type, start_addr, permanent_addr, size);
- else
- return new RegionDense(type, start_addr, permanent_addr, size);
}
RegionSparse::RegionSparse(RegionType region_type, void* start_addr, void* permanent_addr, size_t size)
xbt_assert((((uintptr_t)permanent_addr) & (xbt_pagesize - 1)) == 0,
"Permanent address not at the beginning of a page");
- storage_type_ = StorageType::Chunked;
- flat_data_.clear();
-
page_numbers_ =
ChunkedData(mc_model_checker->page_store(), *process, RemotePtr<void>(permanent_addr), mmu::chunk_count(size));
}
*/
void RegionSnapshot::restore()
{
- switch (storage_type()) {
- case simgrid::mc::StorageType::Flat:
- mc_model_checker->process().write_bytes(flat_data().get(), size(), permanent_address());
- break;
-
- case simgrid::mc::StorageType::Chunked:
xbt_assert(((permanent_address().address()) & (xbt_pagesize - 1)) == 0, "Not at the beginning of a page");
xbt_assert(simgrid::mc::mmu::chunk_count(size()) == page_data().page_count());
const void* source_page = page_data().page(i);
mc_model_checker->process().write_bytes(source_page, xbt_pagesize, remote(target_page));
}
-
- break;
-
- default: // includes StorageType::NoData
- xbt_die("Storage type not supported");
- break;
- }
}
} // namespace mc
enum class RegionType { Unknown = 0, Heap = 1, Data = 2 };
-enum class StorageType { NoData = 0, Flat = 1, Chunked = 2 };
-
-class Buffer {
-private:
- void* data_ = nullptr;
- std::size_t size_;
-
- explicit Buffer(std::size_t size) : size_(size) { data_ = ::operator new(size_); }
-
- Buffer(void* data, std::size_t size) : data_(data), size_(size) {}
-
-public:
- Buffer() = default;
- void clear() noexcept
- {
- ::operator delete(data_);
- data_ = nullptr;
- size_ = 0;
- }
-
- ~Buffer() noexcept { clear(); }
-
- static Buffer malloc(std::size_t size) { return Buffer(size); }
-
- // No copy
- Buffer(Buffer const& buffer) = delete;
- Buffer& operator=(Buffer const& buffer) = delete;
-
- // Move
- Buffer(Buffer&& that) noexcept : data_(that.data_), size_(that.size_)
- {
- that.data_ = nullptr;
- that.size_ = 0;
- }
- Buffer& operator=(Buffer&& that) noexcept
- {
- clear();
- data_ = that.data_;
- size_ = that.size_;
- that.data_ = nullptr;
- that.size_ = 0;
- return *this;
- }
-
- void* get() { return data_; }
- const void* get() const { return data_; }
- std::size_t size() const { return size_; }
-};
-
/** A copy/snapshot of a given memory region
*
* Different types of region snapshot storage types exist:
protected:
RegionType region_type_ = UnknownRegion;
- StorageType storage_type_ = StorageType::NoData;
simgrid::mc::ObjectInformation* object_info_ = nullptr;
/** @brief Virtual address of the region in the simulated process */
* */
void* permanent_addr_ = nullptr;
- Buffer flat_data_;
ChunkedData page_numbers_;
public:
RegionSnapshot& operator=(RegionSnapshot const&) = delete;
RegionSnapshot(RegionSnapshot&& that)
: region_type_(that.region_type_)
- , storage_type_(that.storage_type_)
, object_info_(that.object_info_)
, start_addr_(that.start_addr_)
, size_(that.size_)
, permanent_addr_(that.permanent_addr_)
- , flat_data_(std::move(that.flat_data_))
, page_numbers_(std::move(that.page_numbers_))
{
that.clear();
RegionSnapshot& operator=(RegionSnapshot&& that)
{
region_type_ = that.region_type_;
- storage_type_ = that.storage_type_;
object_info_ = that.object_info_;
start_addr_ = that.start_addr_;
size_ = that.size_;
permanent_addr_ = that.permanent_addr_;
- flat_data_ = std::move(that.flat_data_);
page_numbers_ = std::move(that.page_numbers_);
that.clear();
return *this;
void clear()
{
region_type_ = UnknownRegion;
- storage_type_ = StorageType::NoData;
page_numbers_.clear();
- flat_data_.clear();
object_info_ = nullptr;
start_addr_ = nullptr;
size_ = 0;
void clear_data()
{
- storage_type_ = StorageType::NoData;
- flat_data_.clear();
page_numbers_.clear();
}
- const Buffer& flat_data() const { return flat_data_; }
- Buffer& flat_data() { return flat_data_; }
-
ChunkedData const& page_data() const { return page_numbers_; }
simgrid::mc::ObjectInformation* object_info() const { return object_info_; }
RemotePtr<void> end() const { return remote((char*)start_addr_ + size_); }
RemotePtr<void> permanent_address() const { return remote(permanent_addr_); }
std::size_t size() const { return size_; }
- StorageType storage_type() const { return storage_type_; }
RegionType region_type() const { return region_type_; }
bool contain(RemotePtr<void> p) const { return p >= start() && p < end(); }
void restore();
};
-class RegionDense : public RegionSnapshot {
-public:
- RegionDense(RegionType type, void* start_addr, void* data_addr, std::size_t size);
-};
class RegionSparse : public RegionSnapshot {
public:
RegionSparse(RegionType type, void* start_addr, void* data_addr, std::size_t size);
// Read each page:
while (simgrid::mc::mmu::split((std::uintptr_t)addr).first != page_end) {
- void* snapshot_addr = mc_translate_address_region_chunked((uintptr_t)addr, region);
+ void* snapshot_addr = mc_translate_address_region((uintptr_t)addr, region);
void* next_page = (void*)simgrid::mc::mmu::join(simgrid::mc::mmu::split((std::uintptr_t)addr).first + 1, 0);
size_t readable = (char*)next_page - (char*)addr;
memcpy(dest, snapshot_addr, readable);
}
// Read the end:
- void* snapshot_addr = mc_translate_address_region_chunked((uintptr_t)addr, region);
+ void* snapshot_addr = mc_translate_address_region((uintptr_t)addr, region);
memcpy(dest, snapshot_addr, size);
return target;
// Using alloca() for large allocations may trigger stack overflow:
// use malloc if the buffer is too big.
bool stack_alloc = size < 64;
- void* buffer1a = nullptr;
- void* buffer2a = nullptr;
- if (region1 != nullptr && region1->storage_type() != simgrid::mc::StorageType::Flat)
- buffer1a = stack_alloc ? alloca(size) : ::operator new(size);
- if (region2 != nullptr && region2->storage_type() != simgrid::mc::StorageType::Flat)
- buffer2a = stack_alloc ? alloca(size) : ::operator new(size);
+ void* buffer1a = stack_alloc ? alloca(size) : ::operator new(size);
+ void* buffer2a = stack_alloc ? alloca(size) : ::operator new(size);
const void* buffer1 = MC_region_read(region1, buffer1a, addr1, size);
const void* buffer2 = MC_region_read(region2, buffer2a, addr2, size);
int res;
// ***** Snapshot region
-static XBT_ALWAYS_INLINE void* mc_translate_address_region_chunked(uintptr_t addr, simgrid::mc::RegionSnapshot* region)
+static XBT_ALWAYS_INLINE void* mc_translate_address_region(uintptr_t addr, simgrid::mc::RegionSnapshot* region)
{
auto split = simgrid::mc::mmu::split(addr - region->start().address());
auto pageno = split.first;
return (char*)snapshot_page + offset;
}
-static XBT_ALWAYS_INLINE void* mc_translate_address_region(uintptr_t addr, simgrid::mc::RegionSnapshot* region)
-{
- switch (region->storage_type()) {
- case simgrid::mc::StorageType::Flat: {
- uintptr_t offset = (uintptr_t)addr - (uintptr_t)region->start().address();
- return (void*)((uintptr_t)region->flat_data().get() + offset);
- }
- case simgrid::mc::StorageType::Chunked:
- return mc_translate_address_region_chunked(addr, region);
- default: // includes StorageType::NoData
- xbt_die("Storage type not supported");
- }
-}
-
// ***** MC Snapshot
/** Ignored data
{
xbt_assert(region);
- std::uintptr_t offset = (std::uintptr_t)addr - (std::uintptr_t)region->start().address();
-
xbt_assert(region->contain(simgrid::mc::remote(addr)), "Trying to read out of the region boundary.");
- switch (region->storage_type()) {
- case simgrid::mc::StorageType::Flat:
- return (char*)region->flat_data().get() + offset;
-
- case simgrid::mc::StorageType::Chunked: {
// Last byte of the region:
void* end = (char*)addr + size - 1;
if (simgrid::mc::mmu::same_chunk((std::uintptr_t)addr, (std::uintptr_t)end)) {
// The memory is contained in a single page:
- return mc_translate_address_region_chunked((uintptr_t)addr, region);
+ return mc_translate_address_region((uintptr_t)addr, region);
}
// Otherwise, the memory spans several pages:
return MC_region_read_fragmented(region, target, addr, size);
- }
-
- default:
- xbt_die("StorageType::NoData not supported");
- }
}
static XBT_ALWAYS_INLINE void* MC_region_read_pointer(simgrid::mc::RegionSnapshot* region, const void* addr)
class snap_test_helper {
public:
static void init_memory(void* mem, size_t size);
- static void Init(bool sparse_ckpt);
+ static void Init();
typedef struct {
size_t size;
void* src;
}
static std::default_random_engine rnd_engine;
- static bool sparse_checkpoint;
static std::unique_ptr<simgrid::mc::RemoteClient> process;
};
// static member variables init.
std::default_random_engine snap_test_helper::rnd_engine;
-bool snap_test_helper::sparse_checkpoint = 0;
std::unique_ptr<simgrid::mc::RemoteClient> snap_test_helper::process = nullptr;
void snap_test_helper::init_memory(void* mem, size_t size)
}
}
-void snap_test_helper::Init(bool sparse_ckpt)
+void snap_test_helper::Init()
{
- _sg_mc_sparse_checkpoint = sparse_ckpt;
REQUIRE(xbt_pagesize == getpagesize());
REQUIRE(1 << xbt_pagebits == xbt_pagesize);
TEST_CASE("MC::Snapshot: A copy/snapshot of a given memory region", "MC::Snapshot")
{
- auto sparse = GENERATE(false, true);
- if (sparse) {
- INFO("Sparse snapshot (using pages)");
- } else {
- INFO("Flat snapshot (no pages)");
- }
+ INFO("Sparse snapshot (using pages)");
- snap_test_helper::Init(sparse);
+ snap_test_helper::Init();
INFO("Read whole region");
snap_test_helper::read_whole_region();
