[mc] enable model-check/record by default, and cosmetics

diff --git a/docs/source/Configuring_SimGrid.rst b/docs/source/Configuring_SimGrid.rst
index 682f887..7a59994 100644 (file)
--- a/docs/source/Configuring_SimGrid.rst
+++ b/docs/source/Configuring_SimGrid.rst
@@ -684,24 +684,21 @@ it could be. For this reason, it is currently disabled by default.
 .. _cfg=model-check/record:
 .. _cfg=model-check/replay:
 
-Record/Replay of Verification
-.............................
+Recording and replaying verifications
+.....................................
 
-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
-under the model-checker. Event the output of the program is difficult to
-interpret. Moreover, the model-checker does not behave nicely with advanced
-debugging tools such as valgrind. For those reason, to identify a trajectory
-in the execution graph with the model-checker and replay this trajcetory and
-without the model-checker black-magic but with more standard tools
-(such as a debugger, valgrind, etc.). For this reason, Simgrid implements an
-experimental record/replay functionnality in order to record a trajectory with
-the model-checker and replay it without the model-checker.
+Debugging the problems reported by the model-checker is challenging: First, the
+application under verification cannot be debugged with gdb because the
+model-checker already traces it. Then, the model-checker may explore several
+execution paths before encountering the issue, making it very difficult to
+understand the outputs. Fortunately, SimGrid provides the execution path leading
+to any reported issue so that you can replay this path out of the model checker,
+enabling the usage of classical debugging tools.
 
 When the model-checker finds an interesting path in the application
 execution graph (where a safety or liveness property is violated), it
 can generate an identifier for this path. To enable this behavious the
-``model-check/record`` must be set to **yes**, which is not the case
+``model-check/record`` must be set to **yes**, which is the case
 by default.
 
 Here is an example of output:
@@ -713,9 +710,9 @@ Here is an example of output:
    [  0.000000] (0:@) *** PROPERTY NOT VALID ***
    [  0.000000] (0:@) **************************
    [  0.000000] (0:@) Counter-example execution trace:
+   [  0.000000] (0:@)   [(1)Tremblay (app)] MC_RANDOM(3)
+   [  0.000000] (0:@)   [(1)Tremblay (app)] MC_RANDOM(4)
    [  0.000000] (0:@) Path = 1/3;1/4
-   [  0.000000] (0:@) [(1)Tremblay (app)] MC_RANDOM(3)
-   [  0.000000] (0:@) [(1)Tremblay (app)] MC_RANDOM(4)
    [  0.000000] (0:@) Expanded states = 27
    [  0.000000] (0:@) Visited states = 68
    [  0.000000] (0:@) Executed transitions = 46
@@ -723,11 +720,8 @@ Here is an example of output:
 This path can then be replayed outside of the model-checker (and even
 in non-MC build of simgrid) by setting the ``model-check/replay`` item
 to the given path. The other options should be the same (but the
-model-checker should be disabled).
-
-The format and meaning of the path may change between different
-releases so the same release of Simgrid should be used for the record
-phase and the replay phase.
+model-checker should be disabled). Note that format and meaning of the
+path may change between different releases.
 
 Configuring the User Code Virtualization
 ----------------------------------------

diff --git a/examples/deprecated/msg/mc/bugged1.tesh b/examples/deprecated/msg/mc/bugged1.tesh
index 88d37e7..2aea478 100644 (file)
--- a/examples/deprecated/msg/mc/bugged1.tesh
+++ b/examples/deprecated/msg/mc/bugged1.tesh
@@ -21,16 +21,17 @@ $ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged1 "--log=root.fmt:[
 > [  0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
 > [  0.000000] (0:maestro@) **************************
 > [  0.000000] (0:maestro@) Counter-example execution trace:
-> [  0.000000] (0:maestro@) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
-> [  0.000000] (0:maestro@) [(2)HostB (client)] iSend(src=(2)HostB (client), buff=(verbose only), size=(verbose only))
-> [  0.000000] (0:maestro@) [(1)HostA (server)] Wait(comm=(verbose only) [(2)HostB (client)-> (1)HostA (server)])
-> [  0.000000] (0:maestro@) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
-> [  0.000000] (0:maestro@) [(2)HostB (client)] Wait(comm=(verbose only) [(2)HostB (client)-> (1)HostA (server)])
-> [  0.000000] (0:maestro@) [(4)HostD (client)] iSend(src=(4)HostD (client), buff=(verbose only), size=(verbose only))
-> [  0.000000] (0:maestro@) [(1)HostA (server)] Wait(comm=(verbose only) [(4)HostD (client)-> (1)HostA (server)])
-> [  0.000000] (0:maestro@) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
-> [  0.000000] (0:maestro@) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
-> [  0.000000] (0:maestro@) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
+> [  0.000000] (0:maestro@)   [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:maestro@)   [(2)HostB (client)] iSend(src=(2)HostB (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:maestro@)   [(1)HostA (server)] Wait(comm=(verbose only) [(2)HostB (client)-> (1)HostA (server)])
+> [  0.000000] (0:maestro@)   [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:maestro@)   [(2)HostB (client)] Wait(comm=(verbose only) [(2)HostB (client)-> (1)HostA (server)])
+> [  0.000000] (0:maestro@)   [(4)HostD (client)] iSend(src=(4)HostD (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:maestro@)   [(1)HostA (server)] Wait(comm=(verbose only) [(4)HostD (client)-> (1)HostA (server)])
+> [  0.000000] (0:maestro@)   [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:maestro@)   [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:maestro@)   [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
+> [  0.000000] (0:maestro@) Path = 1;2;1;1;2;4;1;1;3;1
 > [  0.000000] (0:maestro@) Expanded states = 22
 > [  0.000000] (0:maestro@) Visited states = 56
 > [  0.000000] (0:maestro@) Executed transitions = 52

diff --git a/examples/deprecated/msg/mc/bugged2.tesh b/examples/deprecated/msg/mc/bugged2.tesh
index 1633a7f..719ffe2 100644 (file)
--- a/examples/deprecated/msg/mc/bugged2.tesh
+++ b/examples/deprecated/msg/mc/bugged2.tesh
@@ -2092,13 +2092,14 @@ $ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged2 "--log=root.fmt:[
 > [  0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
 > [  0.000000] (0:maestro@) **************************
 > [  0.000000] (0:maestro@) Counter-example execution trace:
-> [  0.000000] (0:maestro@) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
-> [  0.000000] (0:maestro@) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
-> [  0.000000] (0:maestro@) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
-> [  0.000000] (0:maestro@) [(3)HostC (client)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
-> [  0.000000] (0:maestro@) [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
-> [  0.000000] (0:maestro@) [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
-> [  0.000000] (0:maestro@) [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
+> [  0.000000] (0:maestro@)   [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:maestro@)   [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:maestro@)   [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
+> [  0.000000] (0:maestro@)   [(3)HostC (client)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
+> [  0.000000] (0:maestro@)   [(1)HostA (server)] iRecv(dst=(1)HostA (server), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:maestro@)   [(3)HostC (client)] iSend(src=(3)HostC (client), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:maestro@)   [(1)HostA (server)] Wait(comm=(verbose only) [(3)HostC (client)-> (1)HostA (server)])
+> [  0.000000] (0:maestro@) Path = 1;3;1;3;1;3;1
 > [  0.000000] (0:maestro@) Expanded states = 1006
 > [  0.000000] (0:maestro@) Visited states = 5319
 > [  0.000000] (0:maestro@) Executed transitions = 4969
\ No newline at end of file

diff --git a/examples/s4u/mc-failing-assert/s4u-mc-failing-assert.tesh b/examples/s4u/mc-failing-assert/s4u-mc-failing-assert.tesh
index f35e7b1..24e5927 100644 (file)
--- a/examples/s4u/mc-failing-assert/s4u-mc-failing-assert.tesh
+++ b/examples/s4u/mc-failing-assert/s4u-mc-failing-assert.tesh
@@ -16,12 +16,13 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-failing-assert ${plat
 > [  0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
 > [  0.000000] (0:maestro@) **************************
 > [  0.000000] (0:maestro@) Counter-example execution trace:
-> [  0.000000] (0:maestro@) [(1)Boivin (server)] iRecv(dst=(1)Boivin (server), buff=(verbose only), size=(verbose only))
-> [  0.000000] (0:maestro@) [(3)Fafard (client2)] iSend(src=(3)Fafard (client2), buff=(verbose only), size=(verbose only))
-> [  0.000000] (0:maestro@) [(1)Boivin (server)] Wait(comm=(verbose only) [(3)Fafard (client2)-> (1)Boivin (server)])
-> [  0.000000] (0:maestro@) [(1)Boivin (server)] iRecv(dst=(1)Boivin (server), buff=(verbose only), size=(verbose only))
-> [  0.000000] (0:maestro@) [(2)Bourassa (client1)] iSend(src=(2)Bourassa (client1), buff=(verbose only), size=(verbose only))
-> [  0.000000] (0:maestro@) [(1)Boivin (server)] Wait(comm=(verbose only) [(2)Bourassa (client1)-> (1)Boivin (server)])
+> [  0.000000] (0:maestro@)   [(1)Boivin (server)] iRecv(dst=(1)Boivin (server), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:maestro@)   [(3)Fafard (client2)] iSend(src=(3)Fafard (client2), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:maestro@)   [(1)Boivin (server)] Wait(comm=(verbose only) [(3)Fafard (client2)-> (1)Boivin (server)])
+> [  0.000000] (0:maestro@)   [(1)Boivin (server)] iRecv(dst=(1)Boivin (server), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:maestro@)   [(2)Bourassa (client1)] iSend(src=(2)Bourassa (client1), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:maestro@)   [(1)Boivin (server)] Wait(comm=(verbose only) [(2)Bourassa (client1)-> (1)Boivin (server)])
+> [  0.000000] (0:maestro@) Path = 1;3;1;1;2;1
 > [  0.000000] (0:maestro@) Expanded states = 18
 > [  0.000000] (0:maestro@) Visited states = 36
 > [  0.000000] (0:maestro@) Executed transitions = 32

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 2d6a04b..8866abb 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -163,9 +163,9 @@ static void MC_report_crash(int status)
   else
     XBT_INFO("No core dump was generated by the system.");
   XBT_INFO("Counter-example execution trace:");
-  simgrid::mc::dumpRecordPath();
   for (auto const& s : mc_model_checker->getChecker()->getTextualTrace())
-    XBT_INFO("%s", s.c_str());
+    XBT_INFO("  %s", s.c_str());
+  simgrid::mc::dumpRecordPath();
   simgrid::mc::session->logState();
   XBT_INFO("Stack trace:");
   mc_model_checker->process().dumpStack();
@@ -177,9 +177,9 @@ static void MC_report_assertion_error()
   XBT_INFO("*** PROPERTY NOT VALID ***");
   XBT_INFO("**************************");
   XBT_INFO("Counter-example execution trace:");
-  simgrid::mc::dumpRecordPath();
   for (auto const& s : mc_model_checker->getChecker()->getTextualTrace())
-    XBT_INFO("%s", s.c_str());
+    XBT_INFO("  %s", s.c_str());
+  simgrid::mc::dumpRecordPath();
   simgrid::mc::session->logState();
 }
 

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 5875f80..4c5a2ca 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -275,12 +275,12 @@ void LivenessChecker::showAcceptanceCycle(std::size_t depth)
   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
   XBT_INFO("|             ACCEPTANCE CYCLE            |");
   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
-  XBT_INFO("Counter-example that violates formula :");
-  simgrid::mc::dumpRecordPath();
+  XBT_INFO("Counter-example that violates formula:");
   for (auto const& s : this->getTextualTrace())
-    XBT_INFO("%s", s.c_str());
+    XBT_INFO("  %s", s.c_str());
+  simgrid::mc::dumpRecordPath();
   simgrid::mc::session->logState();
-  XBT_INFO("Counter-example depth : %zu", depth);
+  XBT_INFO("Counter-example depth: %zu", depth);
 }
 
 std::vector<std::string> LivenessChecker::getTextualTrace() // override

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index 079f3fe..b37e2d8 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -49,7 +49,8 @@ void SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
       XBT_INFO("******************************************");
       XBT_INFO("Counter-example execution trace:");
       for (auto const& s : mc_model_checker->getChecker()->getTextualTrace())
-        XBT_INFO("%s", s.c_str());
+        XBT_INFO("  %s", s.c_str());
+      simgrid::mc::dumpRecordPath();
       simgrid::mc::session->logState();
 
       throw simgrid::mc::TerminationError();

diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp
index e9e4f66..ed3220f 100644 (file)
--- a/src/mc/mc_config.cpp
+++ b/src/mc/mc_config.cpp
@@ -54,7 +54,7 @@ simgrid::config::Flag<bool> _sg_mc_timeout{
 int _sg_do_model_check = 0;
 int _sg_mc_max_visited_states = 0;
 
-simgrid::config::Flag<bool> _sg_do_model_check_record{"model-check/record", "Record the model-checking paths", false};
+simgrid::config::Flag<bool> _sg_do_model_check_record{"model-check/record", "Record the model-checking paths", true};
 
 simgrid::config::Flag<int> _sg_mc_checkpoint{
     "model-check/checkpoint", "Specify the amount of steps between checkpoints during stateful model-checking "

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 0a48a28..b2cc82d 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -106,7 +106,8 @@ void MC_show_deadlock()
   XBT_INFO("**************************");
   XBT_INFO("Counter-example execution trace:");
   for (auto const& s : mc_model_checker->getChecker()->getTextualTrace())
-    XBT_INFO("%s", s.c_str());
+    XBT_INFO("  %s", s.c_str());
+  simgrid::mc::dumpRecordPath();
   simgrid::mc::session->logState();
 }
 

diff --git a/teshsuite/mc/random-bug/random-bug-report.tesh b/teshsuite/mc/random-bug/random-bug-report.tesh
index 1fec35e..2cf1115 100644 (file)
--- a/teshsuite/mc/random-bug/random-bug-report.tesh
+++ b/teshsuite/mc/random-bug/random-bug-report.tesh
@@ -1,14 +1,14 @@
 #!/usr/bin/env tesh
 ! expect return 1
-$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug ${srcdir:=.}/examples/platforms/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=model-check/record:1
+$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug ${srcdir:=.}/examples/platforms/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning
 > [  0.000000] (0:maestro@) Check a safety property. Reduction is: dpor.
 > [  0.000000] (0:maestro@) **************************
 > [  0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
 > [  0.000000] (0:maestro@) **************************
 > [  0.000000] (0:maestro@) Counter-example execution trace:
+> [  0.000000] (0:maestro@)   [(1)Tremblay (app)] MC_RANDOM(3)
+> [  0.000000] (0:maestro@)   [(1)Tremblay (app)] MC_RANDOM(4)
 > [  0.000000] (0:maestro@) Path = 1/3;1/4
-> [  0.000000] (0:maestro@) [(1)Tremblay (app)] MC_RANDOM(3)
-> [  0.000000] (0:maestro@) [(1)Tremblay (app)] MC_RANDOM(4)
 > [  0.000000] (0:maestro@) Expanded states = 27
 > [  0.000000] (0:maestro@) Visited states = 68
 > [  0.000000] (0:maestro@) Executed transitions = 46