From 603a2971cfa9ec8a4fd4493b74c5680956828423 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Tue, 14 May 2019 22:44:41 +0200 Subject: [PATCH] [mc] enable model-check/record by default, and cosmetics --- docs/source/Configuring_SimGrid.rst | 34 ++++++++----------- examples/deprecated/msg/mc/bugged1.tesh | 21 ++++++------ examples/deprecated/msg/mc/bugged2.tesh | 15 ++++---- .../s4u-mc-failing-assert.tesh | 13 +++---- src/mc/ModelChecker.cpp | 8 ++--- src/mc/checker/LivenessChecker.cpp | 8 ++--- src/mc/checker/SafetyChecker.cpp | 3 +- src/mc/mc_config.cpp | 2 +- src/mc/mc_global.cpp | 3 +- .../mc/random-bug/random-bug-report.tesh | 6 ++-- 10 files changed, 56 insertions(+), 57 deletions(-) diff --git a/docs/source/Configuring_SimGrid.rst b/docs/source/Configuring_SimGrid.rst index 682f887883..7a59994c84 100644 --- 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 88d37e763f..2aea4788db 100644 --- 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 1633a7fbce..719ffe2016 100644 --- 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 f35e7b19fa..24e59278de 100644 --- 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 2d6a04b526..8866abb8db 100644 --- 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 5875f8071d..4c5a2ca033 100644 --- 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 LivenessChecker::getTextualTrace() // override diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index 079f3fe827..b37e2d8846 100644 --- 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 e9e4f6655a..ed3220ffad 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -54,7 +54,7 @@ simgrid::config::Flag _sg_mc_timeout{ int _sg_do_model_check = 0; int _sg_mc_max_visited_states = 0; -simgrid::config::Flag _sg_do_model_check_record{"model-check/record", "Record the model-checking paths", false}; +simgrid::config::Flag _sg_do_model_check_record{"model-check/record", "Record the model-checking paths", true}; simgrid::config::Flag _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 0a48a28b20..b2cc82d9cd 100644 --- 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 1fec35e7e1..2cf11154cd 100644 --- 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 -- 2.20.1