From ebb85bd0b304300f7556e5077d294baa717ddb79 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Tue, 2 Jun 2015 15:02:27 +0200 Subject: [PATCH] [mc] exit() instead of abort() in normal operation --- buildtools/Cmake/DefinePackages.cmake | 1 + examples/msg/mc/bugged1.tesh | 2 +- examples/msg/mc/bugged1_liveness.tesh | 2 +- examples/msg/mc/bugged1_liveness_sparse.tesh | 2 +- examples/msg/mc/bugged1_liveness_visited.tesh | 2 +- .../mc/bugged1_liveness_visited_sparse.tesh | 2 +- examples/msg/mc/bugged2.tesh | 2 +- src/mc/mc_comm_determinism.cpp | 5 ++-- src/mc/mc_exit.h | 13 ++++++++++ src/mc/mc_liveness.cpp | 3 ++- src/mc/mc_safety.cpp | 25 ++++++++++--------- src/mc/mc_server.cpp | 3 ++- src/mc/mc_server.h | 3 ++- teshsuite/mc/replay/random_bug.tesh | 2 +- 14 files changed, 43 insertions(+), 24 deletions(-) create mode 100644 src/mc/mc_exit.h diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake index ea972cb9a2..c4eb5fdb1f 100644 --- a/buildtools/Cmake/DefinePackages.cmake +++ b/buildtools/Cmake/DefinePackages.cmake @@ -653,6 +653,7 @@ set(MC_SRC src/mc/mc_smx.cpp src/mc/mc_xbt.hpp src/mc/mc_xbt.cpp + src/mc/mc_exit.h ) set(MC_SIMGRID_MC_SRC diff --git a/examples/msg/mc/bugged1.tesh b/examples/msg/mc/bugged1.tesh index b8a1ca278e..8e13b8257b 100644 --- a/examples/msg/mc/bugged1.tesh +++ b/examples/msg/mc/bugged1.tesh @@ -1,6 +1,6 @@ #! ./tesh -! expect signal SIGABRT +! expect return 1 ! timeout 20 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack_size:256 > [ 0.000000] (0:@) Check a safety property diff --git a/examples/msg/mc/bugged1_liveness.tesh b/examples/msg/mc/bugged1_liveness.tesh index 5cb0cf00eb..9f0b7adf0e 100644 --- a/examples/msg/mc/bugged1_liveness.tesh +++ b/examples/msg/mc/bugged1_liveness.tesh @@ -1,6 +1,6 @@ #! ./tesh -! expect signal SIGABRT +! expect return 2 ! timeout 20 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 --cfg=model-check/property:promela_bugged1_liveness > [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness diff --git a/examples/msg/mc/bugged1_liveness_sparse.tesh b/examples/msg/mc/bugged1_liveness_sparse.tesh index 72d4e722e1..bc96e3bc67 100644 --- a/examples/msg/mc/bugged1_liveness_sparse.tesh +++ b/examples/msg/mc/bugged1_liveness_sparse.tesh @@ -1,6 +1,6 @@ #! ./tesh -! expect signal SIGABRT +! expect return 2 ! timeout 60 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--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:@) Check the liveness property promela_bugged1_liveness diff --git a/examples/msg/mc/bugged1_liveness_visited.tesh b/examples/msg/mc/bugged1_liveness_visited.tesh index daaa02eff4..fd040b4a0a 100644 --- a/examples/msg/mc/bugged1_liveness_visited.tesh +++ b/examples/msg/mc/bugged1_liveness_visited.tesh @@ -1,6 +1,6 @@ #! ./tesh -! expect signal SIGABRT +! expect return 2 ! timeout 90 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--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/property:promela_bugged1_liveness > [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness diff --git a/examples/msg/mc/bugged1_liveness_visited_sparse.tesh b/examples/msg/mc/bugged1_liveness_visited_sparse.tesh index 77e64a4128..9fe46b02d7 100644 --- a/examples/msg/mc/bugged1_liveness_visited_sparse.tesh +++ b/examples/msg/mc/bugged1_liveness_visited_sparse.tesh @@ -1,6 +1,6 @@ #! ./tesh -! expect signal SIGABRT +! expect return 2 ! timeout 90 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--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:@) Check the liveness property promela_bugged1_liveness diff --git a/examples/msg/mc/bugged2.tesh b/examples/msg/mc/bugged2.tesh index cadf32f2ab..4449cbe72d 100644 --- a/examples/msg/mc/bugged2.tesh +++ b/examples/msg/mc/bugged2.tesh @@ -1,6 +1,6 @@ #! ./tesh -! expect signal SIGABRT +! expect return 1 ! timeout 20 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged2 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack_size:256 > [ 0.000000] (0:@) Check a safety property diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/mc_comm_determinism.cpp index 41a5918a3b..a30cd61b02 100644 --- a/src/mc/mc_comm_determinism.cpp +++ b/src/mc/mc_comm_determinism.cpp @@ -12,6 +12,7 @@ #include "mc_record.h" #include "mc_smx.h" #include "mc_client.h" +#include "mc_exit.h" using simgrid::mc::remote; @@ -144,7 +145,7 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int xbt_free(initial_global_state->send_diff); initial_global_state->send_diff = NULL; MC_print_statistics(mc_stats); - xbt_abort(); + exit(SIMGRID_EXIT_NON_DETERMINISM); }else if(_sg_mc_comms_determinism && (!initial_global_state->send_deterministic && !initial_global_state->recv_deterministic)) { XBT_INFO("****************************************************"); XBT_INFO("***** Non-deterministic communications pattern *****"); @@ -156,7 +157,7 @@ static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int xbt_free(initial_global_state->recv_diff); initial_global_state->recv_diff = NULL; MC_print_statistics(mc_stats); - xbt_abort(); + exit(SIMGRID_EXIT_NON_DETERMINISM); } } } diff --git a/src/mc/mc_exit.h b/src/mc/mc_exit.h new file mode 100644 index 0000000000..0b17cacad4 --- /dev/null +++ b/src/mc/mc_exit.h @@ -0,0 +1,13 @@ +#ifndef SIMGRID_MC_EXIT_HPP +#define SIMGRID_MC_EXIT_HPP + +#define SIMGRID_EXIT_SUCCESS 0 +#define SIMGRID_EXIT_SAFETY 1 +#define SIMGRID_EXIT_LIVENESS 2 +#define SIMGRID_EXIT_DEADLOCK 3 +#define SIMGRID_EXIT_NON_TERMINATION 4 +#define SIMGRID_EXIT_NON_DETERMINISM 5 + +#define SIMGRID_ERROR 63 + +#endif diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp index 927692d5b9..953f1383e5 100644 --- a/src/mc/mc_liveness.cpp +++ b/src/mc/mc_liveness.cpp @@ -18,6 +18,7 @@ #include "mc_client.h" #include "mc_replay.h" #include "mc_safety.h" +#include "mc_exit.h" extern "C" { @@ -251,7 +252,7 @@ static void MC_modelcheck_liveness_main(void) MC_dump_stack_liveness(mc_stack); MC_print_statistics(mc_stats); XBT_INFO("Counter-example depth : %d", counter_example_depth); - xbt_abort(); + exit(SIMGRID_EXIT_LIVENESS); } } diff --git a/src/mc/mc_safety.cpp b/src/mc/mc_safety.cpp index d5fd9bacfe..f4ff0b77da 100644 --- a/src/mc/mc_safety.cpp +++ b/src/mc/mc_safety.cpp @@ -13,6 +13,7 @@ #include "mc_record.h" #include "mc_smx.h" #include "mc_client.h" +#include "mc_exit.h" #include "xbt/mmalloc/mmprivate.h" @@ -21,6 +22,8 @@ extern "C" { XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc, "Logging specific to MC safety verification "); +} + static int is_exploration_stack_state(mc_state_t current_state){ xbt_fifo_item_t item; @@ -35,6 +38,8 @@ static int is_exploration_stack_state(mc_state_t current_state){ return 0; } +static void MC_modelcheck_safety_init(void); + /** * \brief Initialize the DPOR exploration algorithm */ @@ -68,8 +73,10 @@ static void MC_pre_modelcheck_safety() /** \brief Model-check the application using a DFS exploration * with DPOR (Dynamic Partial Order Reductions) */ -static void MC_modelcheck_safety_main(void) +void MC_modelcheck_safety(void) { + MC_modelcheck_safety_init(); + char *req_str = NULL; int value; smx_simcall_t req = NULL; @@ -119,7 +126,7 @@ static void MC_modelcheck_safety_main(void) if(_sg_mc_termination && is_exploration_stack_state(next_state)){ MC_show_non_termination(); - return; + exit(SIMGRID_EXIT_NON_TERMINATION); } if ((visited_state = is_visited_state(next_state)) == NULL) { @@ -179,7 +186,7 @@ static void MC_modelcheck_safety_main(void) /* Check for deadlocks */ if (MC_deadlock_check()) { MC_show_deadlock(NULL); - return; + exit(SIMGRID_EXIT_DEADLOCK); } /* Traverse the stack backwards until a state with a non empty interleave @@ -246,12 +253,13 @@ static void MC_modelcheck_safety_main(void) } } } + XBT_INFO("No property violation found."); MC_print_statistics(mc_stats); - return; + exit(SIMGRID_EXIT_SUCCESS); } -void MC_modelcheck_safety(void) +static void MC_modelcheck_safety_init(void) { if(_sg_mc_termination) mc_reduce_kind = e_mc_reduce_none; @@ -276,11 +284,4 @@ void MC_modelcheck_safety(void) /* Save the initial state */ initial_global_state = xbt_new0(s_mc_global_t, 1); initial_global_state->snapshot = MC_take_snapshot(0); - - MC_modelcheck_safety_main(); - - xbt_abort(); - //MC_exit(); -} - } diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp index 2c8342424b..ba809845b8 100644 --- a/src/mc/mc_server.cpp +++ b/src/mc/mc_server.cpp @@ -21,6 +21,7 @@ #include "mc_private.h" #include "mc_ignore.h" #include "mcer_ignore.h" +#include "mc_exit.h" using simgrid::mc::remote; @@ -238,7 +239,7 @@ bool s_mc_server::handle_events() case MC_MESSAGE_ASSERTION_FAILED: MC_report_assertion_error(); - xbt_abort(); + ::exit(SIMGRID_EXIT_SAFETY); break; default: diff --git a/src/mc/mc_server.h b/src/mc/mc_server.h index a6fc2f8c50..e1ed05d705 100644 --- a/src/mc/mc_server.h +++ b/src/mc/mc_server.h @@ -18,10 +18,11 @@ #include #include "mc_process.h" +#include "mc_exit.h" SG_BEGIN_DECL() -#define MC_SERVER_ERROR 127 +#define MC_SERVER_ERROR SIMGRID_ERROR typedef struct s_mc_server s_mc_server_t, *mc_server_t; diff --git a/teshsuite/mc/replay/random_bug.tesh b/teshsuite/mc/replay/random_bug.tesh index 59e995b3e0..c418e24167 100644 --- a/teshsuite/mc/replay/random_bug.tesh +++ b/teshsuite/mc/replay/random_bug.tesh @@ -1,5 +1,5 @@ #!/usr/bin/env tesh -!expect signal SIGABRT +! expect return 1 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random_bug ${srcdir:=.}/../../../examples/platforms/small_platform.xml ${srcdir:=.}/random_bug.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=model-check:1 --cfg=model-check/record:1 > [ 0.000000] (0:@) Check a safety property > [ 0.000000] (0:@) ************************** -- 2.20.1