X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/082cedd275c8f6dc3478097595380d3e496c74f6..458eaa0a6abd3e3fc601cbb8146049112aeb4011:/src/mc/SafetyChecker.cpp diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index 442b871eed..9848af70fd 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -33,12 +33,32 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc, namespace simgrid { namespace mc { -static int is_exploration_stack_state(mc_state_t current_state){ +static void MC_show_non_termination(void) +{ + XBT_INFO("******************************************"); + XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***"); + XBT_INFO("******************************************"); + XBT_INFO("Counter-example execution trace:"); + for (auto& s : mc_model_checker->getChecker()->getTextualTrace()) + XBT_INFO("%s", s.c_str()); + MC_print_statistics(mc_stats); +} + +static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2) +{ + simgrid::mc::Snapshot* s1 = state1->system_state.get(); + simgrid::mc::Snapshot* s2 = state2->system_state.get(); + int num1 = state1->num; + int num2 = state2->num; + return snapshot_compare(num1, s1, num2, s2); +} + +static int is_exploration_stack_state(simgrid::mc::State* current_state){ xbt_fifo_item_t item; - mc_state_t stack_state; + simgrid::mc::State* stack_state; for(item = xbt_fifo_get_first_item(mc_stack); item != nullptr; item = xbt_fifo_get_next_item(item)) { - stack_state = (mc_state_t) xbt_fifo_get_item_content(item); + stack_state = (simgrid::mc::State*) xbt_fifo_get_item_content(item); if(snapshot_compare(stack_state, current_state) == 0){ XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num); return 1; @@ -47,30 +67,42 @@ static int is_exploration_stack_state(mc_state_t current_state){ return 0; } -/** - * \brief Initialize the DPOR exploration algorithm - */ -void SafetyChecker::pre() +RecordTrace SafetyChecker::getRecordTrace() // override { - simgrid::mc::visited_states.clear(); + RecordTrace res; - mc_state_t initial_state = MC_state_new(); + xbt_fifo_item_t start = xbt_fifo_get_last_item(mc_stack); + for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) { - XBT_DEBUG("**************************************************"); - XBT_DEBUG("Initial state"); + // Find (pid, value): + simgrid::mc::State* state = (simgrid::mc::State*) xbt_fifo_get_item_content(item); + int value = 0; + smx_simcall_t saved_req = MC_state_get_executed_request(state, &value); + const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); + const int pid = issuer->pid; - /* Wait for requests (schedules processes) */ - mc_model_checker->wait_for_requests(); + res.push_back(RecordTraceElement(pid, value)); + } - /* Get an enabled process and insert it in the interleave set of the initial state */ - for (auto& p : mc_model_checker->process().simix_processes()) - if (simgrid::mc::process_is_enabled(&p.copy)) { - MC_state_interleave_process(initial_state, &p.copy); - if (reductionMode_ != simgrid::mc::ReductionMode::none) - break; - } + return res; +} - xbt_fifo_unshift(mc_stack, initial_state); +std::vector SafetyChecker::getTextualTrace() // override +{ + std::vector trace; + for (xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack); + item; item = xbt_fifo_get_prev_item(item)) { + simgrid::mc::State* state = (simgrid::mc::State*)xbt_fifo_get_item_content(item); + int value; + smx_simcall_t req = MC_state_get_executed_request(state, &value); + if (req) { + char* req_str = simgrid::mc::request_to_string( + req, value, simgrid::mc::RequestType::executed); + trace.push_back(req_str); + xbt_free(req_str); + } + } + return trace; } int SafetyChecker::run() @@ -80,14 +112,16 @@ int SafetyChecker::run() char *req_str = nullptr; int value; smx_simcall_t req = nullptr; - mc_state_t state = nullptr, prev_state = NULL, next_state = NULL; + simgrid::mc::State* state = nullptr; + simgrid::mc::State* prev_state = nullptr; + simgrid::mc::State* next_state = nullptr; xbt_fifo_item_t item = nullptr; std::unique_ptr visited_state = nullptr; while (xbt_fifo_size(mc_stack) > 0) { /* Get current state */ - state = (mc_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); + state = (simgrid::mc::State*)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); XBT_DEBUG("**************************************************"); XBT_DEBUG @@ -176,7 +210,7 @@ int SafetyChecker::run() /* Check for deadlocks */ if (mc_model_checker->checkDeadlock()) { - MC_show_deadlock(nullptr); + MC_show_deadlock(); return SIMGRID_MC_EXIT_DEADLOCK; } @@ -187,14 +221,14 @@ int SafetyChecker::run() executed before it. If it does then add it to the interleave set of the state that executed that previous request. */ - while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) { + while ((state = (simgrid::mc::State*) xbt_fifo_shift(mc_stack))) { if (reductionMode_ == simgrid::mc::ReductionMode::dpor) { req = MC_state_get_internal_request(state); if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK) xbt_die("Mutex is currently not supported with DPOR, " "use --cfg=model-check/reduction:none"); const smx_process_t issuer = MC_smx_simcall_get_issuer(req); - xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) { + xbt_fifo_foreach(mc_stack, item, prev_state, simgrid::mc::State*) { if (reductionMode_ != simgrid::mc::ReductionMode::none && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) { if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) { @@ -251,6 +285,7 @@ int SafetyChecker::run() XBT_INFO("No property violation found."); MC_print_statistics(mc_stats); + initial_global_state = nullptr; return SIMGRID_MC_EXIT_SUCCESS; } @@ -273,10 +308,28 @@ void SafetyChecker::init() /* Create exploration stack */ mc_stack = xbt_fifo_new(); - this->pre(); + simgrid::mc::visited_states.clear(); + + simgrid::mc::State* initial_state = MC_state_new(); + + XBT_DEBUG("**************************************************"); + XBT_DEBUG("Initial state"); + + /* Wait for requests (schedules processes) */ + mc_model_checker->wait_for_requests(); + + /* Get an enabled process and insert it in the interleave set of the initial state */ + for (auto& p : mc_model_checker->process().simix_processes()) + if (simgrid::mc::process_is_enabled(&p.copy)) { + MC_state_interleave_process(initial_state, &p.copy); + if (reductionMode_ != simgrid::mc::ReductionMode::none) + break; + } + + xbt_fifo_unshift(mc_stack, initial_state); /* Save the initial state */ - initial_global_state = xbt_new0(s_mc_global_t, 1); + initial_global_state = std::unique_ptr(new s_mc_global_t()); initial_global_state->snapshot = simgrid::mc::take_snapshot(0); }