/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
+#include "mc_state.h"
+#include "mc_request.h"
+#include "mc_safety.h"
#include "mc_private.h"
+#include "mc_record.h"
#include "xbt/mmalloc/mmprivate.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
"Logging specific to MC safety verification ");
-xbt_dict_t first_enabled_state;
+static int is_exploration_stack_state(mc_state_t current_state){
+
+ xbt_fifo_item_t item;
+ mc_state_t stack_state;
+ for(item = xbt_fifo_get_first_item(mc_stack); item != NULL; item = xbt_fifo_get_next_item(item)) {
+ stack_state = (mc_state_t) 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;
+ }
+ }
+ return 0;
+}
/**
* \brief Initialize the DPOR exploration algorithm
MC_SET_MC_HEAP;
if (_sg_mc_visited > 0)
- visited_states =
- xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
-
- if (mc_reduce_kind == e_mc_reduce_dpor)
- first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
+ visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
initial_state = MC_state_new();
/* Wait for requests (schedules processes) */
MC_wait_for_requests();
- if (_sg_mc_visited > 0) {
- MC_ignore_heap(simix_global->process_to_run->data, 0);
- MC_ignore_heap(simix_global->process_that_ran->data, 0);
- }
-
MC_SET_MC_HEAP;
/* Get an enabled process and insert it in the interleave set of the initial state */
xbt_fifo_unshift(mc_stack, initial_state);
- if (mc_reduce_kind == e_mc_reduce_dpor) {
- /* To ensure the soundness of DPOR, we have to keep a list of
- processes which are still enabled at each step of the exploration.
- If max depth is reached, we interleave them in the state in which they have
- been enabled for the first time. */
- xbt_swag_foreach(process, simix_global->process_list) {
- if (MC_process_is_enabled(process)) {
- char *key = bprintf("%lu", process->pid);
- char *data = bprintf("%d", xbt_fifo_size(mc_stack));
- xbt_dict_set(first_enabled_state, key, data, NULL);
- xbt_free(key);
- }
- }
- }
-
if (!mc_mem_set)
MC_SET_STD_HEAP;
}
char *req_str = NULL;
int value;
smx_simcall_t req = NULL, prev_req = NULL;
- mc_state_t state = NULL, prev_state = NULL, next_state =
- NULL, restored_state = NULL;
+ mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
smx_process_t process = NULL;
xbt_fifo_item_t item = NULL;
- mc_state_t state_test = NULL;
- int pos;
- int visited_state = -1;
- int enabled = 0;
+ mc_visited_state_t visited_state = NULL;
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 = (mc_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
XBT_DEBUG("**************************************************");
XBT_DEBUG
- ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
+ ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
xbt_fifo_size(mc_stack), state, state->num,
- MC_state_interleave_size(state), user_max_depth_reached,
- xbt_dict_size(first_enabled_state));
+ MC_state_interleave_size(state), user_max_depth_reached);
/* Update statistics */
mc_stats->visited_states++;
/* If there are processes to interleave and the maximum depth has not been reached
then perform one step of the exploration algorithm */
if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
- && (req = MC_state_get_request(state, &value)) && visited_state == -1) {
+ && (req = MC_state_get_request(state, &value)) && visited_state == NULL) {
- /* Debug information */
- if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
- req_str = MC_request_to_string(req, value);
- XBT_DEBUG("Execute: %s", req_str);
- xbt_free(req_str);
- }
+ char* req_str = MC_request_to_string(req, value);
+ XBT_DEBUG("Execute: %s", req_str);
+ xbt_free(req_str);
- MC_SET_MC_HEAP;
- if (dot_output != NULL)
+ if (dot_output != NULL) {
+ MC_SET_MC_HEAP;
req_str = MC_request_get_dot_output(req, value);
- MC_SET_STD_HEAP;
+ MC_SET_STD_HEAP;
+ }
MC_state_set_executed_request(state, req, value);
mc_stats->executed_transitions++;
- if (mc_reduce_kind == e_mc_reduce_dpor) {
- MC_SET_MC_HEAP;
- char *key = bprintf("%lu", req->issuer->pid);
- xbt_dict_remove(first_enabled_state, key);
- xbt_free(key);
- MC_SET_STD_HEAP;
- }
-
/* Answer the request */
- SIMIX_simcall_pre(req, value);
+ SIMIX_simcall_handle(req, value);
/* Wait for requests (schedules processes) */
MC_wait_for_requests();
next_state = MC_state_new();
- if ((visited_state = is_visited_state()) == -1) {
+ if(_sg_mc_termination && is_exploration_stack_state(next_state)){
+ MC_show_non_termination();
+ return;
+ }
+
+ if ((visited_state = is_visited_state(next_state)) == NULL) {
/* Get an enabled process and insert it in the interleave set of the next state */
xbt_swag_foreach(process, simix_global->process_list) {
}
}
- if (_sg_mc_checkpoint
- && ((xbt_fifo_size(mc_stack) + 1) % _sg_mc_checkpoint == 0)) {
- next_state->system_state = MC_take_snapshot(next_state->num);
- }
-
if (dot_output != NULL)
- fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
- next_state->num, req_str);
+ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
} else {
if (dot_output != NULL)
- fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
- visited_state, req_str);
+ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
}
xbt_fifo_unshift(mc_stack, next_state);
- if (mc_reduce_kind == e_mc_reduce_dpor) {
- /* Insert in dict all enabled processes, if not included yet */
- xbt_swag_foreach(process, simix_global->process_list) {
- if (MC_process_is_enabled(process)) {
- char *key = bprintf("%lu", process->pid);
- if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) {
- char *data = bprintf("%d", xbt_fifo_size(mc_stack));
- xbt_dict_set(first_enabled_state, key, data, NULL);
- }
- xbt_free(key);
- }
- }
- }
-
if (dot_output != NULL)
xbt_free(req_str);
/* The interleave set is empty or the maximum depth is reached, let's back-track */
} else {
- if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached
- || visited_state != -1) {
+ if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != NULL) {
- if (user_max_depth_reached && visited_state == -1)
+ if (user_max_depth_reached && visited_state == NULL)
XBT_DEBUG("User max depth reached !");
- else if (visited_state == -1)
+ else if (visited_state == NULL)
XBT_WARN("/!\\ Max depth reached ! /!\\ ");
-
- if (mc_reduce_kind == e_mc_reduce_dpor) {
- /* Interleave enabled processes in the state in which they have been enabled for the first time */
- xbt_swag_foreach(process, simix_global->process_list) {
- if (MC_process_is_enabled(process)) {
- char *key = bprintf("%lu", process->pid);
- enabled =
- (int) strtoul(xbt_dict_get_or_null(first_enabled_state, key),
- 0, 10);
- xbt_free(key);
- int cursor = xbt_fifo_size(mc_stack);
- xbt_fifo_foreach(mc_stack, item, state_test, mc_state_t) {
- if (cursor-- == enabled) {
- if (!MC_state_process_is_done(state_test, process)
- && state_test->num != state->num) {
- XBT_DEBUG("Interleave process %lu in state %d",
- process->pid, state_test->num);
- MC_state_interleave_process(state_test, process);
- break;
- }
- }
- }
- }
- }
- }
+ else
+ XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
} else {
- XBT_DEBUG("There are no more processes to interleave. (depth %d)",
- xbt_fifo_size(mc_stack) + 1);
+ XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
}
/* Trash the current state, no longer needed */
xbt_fifo_shift(mc_stack);
- MC_state_delete(state);
- XBT_DEBUG("Delete state %d at depth %d", state->num,
- xbt_fifo_size(mc_stack) + 1);
+ MC_state_delete(state, !state->in_visited_states ? 1 : 0);
+ XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
MC_SET_STD_HEAP;
- visited_state = -1;
+ visited_state = NULL;
/* Check for deadlocks */
if (MC_deadlock_check()) {
if (mc_reduce_kind == e_mc_reduce_dpor) {
req = MC_state_get_internal_request(state);
xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
- if (MC_request_depend
- (req, MC_state_get_internal_request(prev_state))) {
+ if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
XBT_DEBUG("Dependent Transitions:");
prev_req = MC_state_get_executed_request(prev_state, &value);
break;
- } else if (req->issuer ==
- MC_state_get_internal_request(prev_state)->issuer) {
+ } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
- XBT_DEBUG("Simcall %d and %d with same issuer", req->call,
- MC_state_get_internal_request(prev_state)->call);
+ XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
break;
} else {
- XBT_DEBUG
- ("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
- req->call, req->issuer->pid, state->num,
- MC_state_get_internal_request(prev_state)->call,
- MC_state_get_internal_request(prev_state)->issuer->pid,
- prev_state->num);
+ XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
+ req->call, req->issuer->pid, state->num,
+ MC_state_get_internal_request(prev_state)->call,
+ MC_state_get_internal_request(prev_state)->issuer->pid,
+ prev_state->num);
}
}
}
- if (MC_state_interleave_size(state)
- && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
+ if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
/* We found a back-tracking point, let's loop */
- XBT_DEBUG("Back-tracking to state %d at depth %d", state->num,
- xbt_fifo_size(mc_stack) + 1);
- if (_sg_mc_checkpoint) {
- if (state->system_state != NULL) {
- MC_restore_snapshot(state->system_state);
- xbt_fifo_unshift(mc_stack, state);
- MC_SET_STD_HEAP;
- } else {
- pos = xbt_fifo_size(mc_stack);
- item = xbt_fifo_get_first_item(mc_stack);
- while (pos > 0) {
- restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
- if (restored_state->system_state != NULL) {
- break;
- } else {
- item = xbt_fifo_get_next_item(item);
- pos--;
- }
- }
- MC_restore_snapshot(restored_state->system_state);
- xbt_fifo_unshift(mc_stack, state);
- MC_SET_STD_HEAP;
- MC_replay(mc_stack, pos);
- }
- } else {
- xbt_fifo_unshift(mc_stack, state);
- MC_SET_STD_HEAP;
- MC_replay(mc_stack, -1);
- }
- XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num,
- xbt_fifo_size(mc_stack));
+ XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
+ xbt_fifo_unshift(mc_stack, state);
+ MC_replay(mc_stack);
+ XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
break;
} else {
- XBT_DEBUG("Delete state %d at depth %d", state->num,
- xbt_fifo_size(mc_stack) + 1);
- MC_state_delete(state);
+ XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
+ MC_state_delete(state, !state->in_visited_states ? 1 : 0);
}
}
MC_SET_STD_HEAP;
