* a given model-checker stack.
* \param stack The stack with the transitions to execute.
* \param start Start index to begin the re-execution.
- *
- * If start==-1, restore the initial state and replay the actions the
- * the transitions in the stack.
- *
- * Otherwise, we only replay a part of the transitions of the stacks
- * without restoring the state: it is assumed that the current state
- * match with the transitions to execute.
*/
-void MC_replay(xbt_fifo_t stack, int start)
+void MC_replay(xbt_fifo_t stack)
{
int raw_mem = (mmalloc_get_current_heap() == mc_heap);
- int value, i = 1, count = 1, j;
+ int value, count = 1, j;
char *req_str;
smx_simcall_t req = NULL, saved_req = NULL;
xbt_fifo_item_t item, start_item;
mc_state_t state;
- smx_process_t process = NULL;
-
+
XBT_DEBUG("**** Begin Replay ****");
- if (start == -1) {
- /* Restore the initial state */
- MC_restore_snapshot(initial_global_state->snapshot);
- /* At the moment of taking the snapshot the raw heap was set, so restoring
- * it will set it back again, we have to unset it to continue */
+ /* Intermediate backtracking */
+ start_item = xbt_fifo_get_first_item(stack);
+ state = (mc_state_t)xbt_fifo_get_item_content(start_item);
+ if(state->system_state){
+ MC_restore_snapshot(state->system_state);
+ if(_sg_mc_comms_determinism || _sg_mc_send_determinism)
+ MC_restore_communications_pattern(state);
MC_SET_STD_HEAP;
+ return;
}
- start_item = xbt_fifo_get_last_item(stack);
- if (start != -1) {
- while (i != start) {
- start_item = xbt_fifo_get_prev_item(start_item);
- i++;
- }
- }
- MC_SET_MC_HEAP;
+ /* Restore the initial state */
+ MC_restore_snapshot(initial_global_state->snapshot);
+ /* At the moment of taking the snapshot the raw heap was set, so restoring
+ * it will set it back again, we have to unset it to continue */
+ MC_SET_STD_HEAP;
- if (mc_reduce_kind == e_mc_reduce_dpor) {
- xbt_dict_reset(first_enabled_state);
- xbt_swag_foreach(process, simix_global->process_list) {
- if (MC_process_is_enabled(process)) {
- char *key = bprintf("%lu", process->pid);
- char *data = bprintf("%d", count);
- xbt_dict_set(first_enabled_state, key, data, NULL);
- xbt_free(key);
- }
- }
- }
+ start_item = xbt_fifo_get_last_item(stack);
+
+ MC_SET_MC_HEAP;
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
- for (j=0; j<simix_process_maxpid; j++) {
- xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(communications_pattern, j, xbt_dynar_t));
- }
for (j=0; j<simix_process_maxpid; j++) {
xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
+ ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, j, mc_list_comm_pattern_t))->index_comm = 0;
}
}
state = (mc_state_t) xbt_fifo_get_item_content(item);
saved_req = MC_state_get_executed_request(state, &value);
-
- if (mc_reduce_kind == e_mc_reduce_dpor) {
- MC_SET_MC_HEAP;
- char *key = bprintf("%lu", saved_req->issuer->pid);
- if(xbt_dict_get_or_null(first_enabled_state, key))
- xbt_dict_remove(first_enabled_state, key);
- xbt_free(key);
- MC_SET_STD_HEAP;
- }
-
+
if (saved_req) {
/* because we got a copy of the executed request, we have to fetch the
real one, pointed by the request field of the issuer process */
}
/* TODO : handle test and testany simcalls */
- mc_call_type call = MC_CALL_TYPE_NONE;
- if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
+ e_mc_call_type_t call = MC_CALL_TYPE_NONE;
+ if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
call = mc_get_call_type(req);
- }
SIMIX_simcall_handle(req, value);
- if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
- MC_SET_MC_HEAP;
- mc_update_comm_pattern(call, req, value, communications_pattern);
- MC_SET_STD_HEAP;
- }
-
+ MC_SET_MC_HEAP;
+ if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
+ handle_comm_pattern(call, req, value, NULL, 1);
+ MC_SET_STD_HEAP;
+
MC_wait_for_requests();
count++;
-
- if (mc_reduce_kind == e_mc_reduce_dpor) {
- MC_SET_MC_HEAP;
- /* Insert in dict all enabled processes */
- 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", count);
- xbt_dict_set(first_enabled_state, key, data, NULL);
- }
- xbt_free(key);
- }
- }
- MC_SET_STD_HEAP;
- }
}
/* Update statistics */
}
-void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
+void MC_replay_liveness(xbt_fifo_t stack)
{
initial_global_state->raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
xbt_fifo_item_t item;
- int depth = 1;
+ mc_pair_t pair = NULL;
+ mc_state_t state = NULL;
+ smx_simcall_t req = NULL, saved_req = NULL;
+ int value, depth = 1;
+ char *req_str;
XBT_DEBUG("**** Begin Replay ****");
+ /* Intermediate backtracking */
+ item = xbt_fifo_get_first_item(stack);
+ pair = (mc_pair_t) xbt_fifo_get_item_content(item);
+ if(pair->graph_state->system_state){
+ MC_restore_snapshot(pair->graph_state->system_state);
+ MC_SET_STD_HEAP;
+ return;
+ }
+
/* Restore the initial state */
MC_restore_snapshot(initial_global_state->snapshot);
/* Traverse the stack from the initial state and re-execute the transitions */
for (item = xbt_fifo_get_last_item(stack);
- all_stack ? depth <= xbt_fifo_size(stack) : item != xbt_fifo_get_first_item(stack);
+ item != xbt_fifo_get_first_item(stack);
item = xbt_fifo_get_prev_item(item)) {
- mc_pair_t pair = (mc_pair_t) xbt_fifo_get_item_content(item);
+ pair = (mc_pair_t) xbt_fifo_get_item_content(item);
- mc_state_t state = (mc_state_t) pair->graph_state;
- smx_simcall_t req = NULL, saved_req = NULL;
- int value;
- char *req_str;
+ state = (mc_state_t) pair->graph_state;
- if (pair->requests > 0) {
+ if (pair->exploration_started) {
saved_req = MC_state_get_executed_request(state, &value);
- //XBT_DEBUG("SavedReq->call %u", saved_req->call);
if (saved_req != NULL) {
/* because we got a copy of the executed request, we have to fetch the
real one, pointed by the request field of the issuer process */
req = &saved_req->issuer->simcall;
- //XBT_DEBUG("Req->call %u", req->call);
/* Debug information */
if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
mc_stats->executed_transitions++;
depth++;
-
+
}
XBT_DEBUG("**** End Replay ****");
int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
MC_show_stack_safety(stack);
-
- if (!_sg_mc_checkpoint) {
-
- mc_state_t state;
-
- MC_SET_MC_HEAP;
- while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
- MC_state_delete(state);
- MC_SET_STD_HEAP;
-
- }
+
+ mc_state_t state;
+
+ MC_SET_MC_HEAP;
+ while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
+ MC_state_delete(state, !state->in_visited_states ? 1 : 0);
+ MC_SET_STD_HEAP;
if (raw_mem_set)
MC_SET_MC_HEAP;
char *req_str = NULL;
for (item = xbt_fifo_get_last_item(stack);
- (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
- : (NULL)); item = xbt_fifo_get_prev_item(item)) {
+ (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item))) : (NULL));
+ item = xbt_fifo_get_prev_item(item)) {
req = MC_state_get_executed_request(pair->graph_state, &value);
- if (req) {
- if (pair->requests > 0) {
- req_str = MC_request_to_string(req, value);
- XBT_INFO("%s", req_str);
- xbt_free(req_str);
- } else {
- XBT_INFO("End of system requests but evolution in Büchi automaton");
- }
+ if (req && req->call != SIMCALL_NONE) {
+ req_str = MC_request_to_string(req, value);
+ XBT_INFO("%s", req_str);
+ xbt_free(req_str);
}
}
}
+
void MC_dump_stack_liveness(xbt_fifo_t stack)
{
mc_pair_t p = NULL;
p = xbt_new0(s_mc_pair_t, 1);
p->num = ++mc_stats->expanded_pairs;
+ p->exploration_started = 0;
p->search_cycle = 0;
+ p->visited_pair_removed = _sg_mc_visited > 0 ? 0 : 1;
return p;
}
void MC_pair_delete(mc_pair_t p)
{
p->automaton_state = NULL;
- MC_state_delete(p->graph_state);
+ MC_state_delete(p->graph_state, p->visited_pair_removed);
xbt_dynar_free(&(p->atomic_propositions));
xbt_free(p);
p = NULL;
extern int user_max_depth_reached;
int MC_deadlock_check(void);
-void MC_replay(xbt_fifo_t stack, int start);
-void MC_replay_liveness(xbt_fifo_t stack, int all_stack);
+void MC_replay(xbt_fifo_t stack);
+void MC_replay_liveness(xbt_fifo_t stack);
void MC_show_deadlock(smx_simcall_t req);
void MC_show_stack_safety(xbt_fifo_t stack);
void MC_dump_stack_safety(xbt_fifo_t stack);
* */
uint64_t mc_hash_processes_state(int num_state, xbt_dynar_t stacks);
-/* *********** Snapshot *********** */
-
-#define MC_LOG_REQUEST(log, req, value) \
- if (XBT_LOG_ISENABLED(log, xbt_log_priority_debug)) { \
- char* req_str = MC_request_to_string(req, value); \
- XBT_DEBUG("Execute: %s", req_str); \
- xbt_free(req_str); \
- }
-
/** @brief Dump the stacks of the application processes
*
* This functions is currently not used but it is quite convenient
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
"Logging specific to MC safety verification ");
-xbt_dict_t first_enabled_state;
-
/**
* \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();
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;
mc_visited_state_t visited_state = NULL;
- int enabled = 0;
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 (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
&& (req = MC_state_get_request(state, &value)) && visited_state == NULL) {
- MC_LOG_REQUEST(mc_safety, req, value);
+ char* req_str = MC_request_to_string(req, value);
+ XBT_DEBUG("Execute: %s", req_str);
+ xbt_free(req_str);
if (dot_output != NULL) {
MC_SET_MC_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_handle(req, value);
next_state = MC_state_new();
- if ((visited_state = is_visited_state()) == NULL) {
+ 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->other_num == -1 ? visited_state->num : visited_state->other_num, 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 != NULL) {
+ if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != NULL) {
if (user_max_depth_reached && visited_state == NULL)
XBT_DEBUG("User max depth reached !");
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);
- 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("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;
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;
#include <simgrid_config.h>
#include <xbt/dict.h>
#include "mc_interface.h"
+#include "mc_state.h"
SG_BEGIN_DECL()
} e_mc_reduce_t;
extern e_mc_reduce_t mc_reduce_kind;
-extern xbt_dict_t first_enabled_state;
void MC_pre_modelcheck_safety(void);
void MC_modelcheck_safety(void);
}s_mc_visited_state_t, *mc_visited_state_t;
extern xbt_dynar_t visited_states;
-mc_visited_state_t is_visited_state(void);
+mc_visited_state_t is_visited_state(mc_state_t graph_state);
void visited_state_free(mc_visited_state_t state);
void visited_state_free_voidp(void *s);
state->proc_status = xbt_new0(s_mc_procstate_t, state->max_pid);
state->system_state = NULL;
state->num = ++mc_stats->expanded_states;
-
+ state->in_visited_states = 0;
+ state->incomplete_comm_pattern = NULL;
+ /* Stateful model checking */
+ if(_sg_mc_checkpoint > 0 && mc_stats->expanded_states % _sg_mc_checkpoint == 0){
+ state->system_state = MC_take_snapshot(state->num);
+ if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
+ copy_incomplete_communications_pattern(state);
+ copy_index_communications_pattern(state);
+ }
+ }
return state;
}
* \brief Deletes a state data structure
* \param trans The state to be deleted
*/
-void MC_state_delete(mc_state_t state)
-{
- if (state->system_state)
+void MC_state_delete(mc_state_t state, int free_snapshot){
+ if (state->system_state && free_snapshot){
MC_free_snapshot(state->system_state);
+ }
+ if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
+ xbt_free(state->index_comm);
+ xbt_free(state->incomplete_comm_pattern);
+ }
xbt_free(state->proc_status);
xbt_free(state);
}
multi-request like waitany ) */
mc_snapshot_t system_state; /* Snapshot of system state */
int num;
+ int in_visited_states;
+ xbt_dynar_t incomplete_comm_pattern; // comm determinism verification
+ xbt_dynar_t index_comm; // comm determinism verification
} s_mc_state_t, *mc_state_t;
mc_state_t MC_state_new(void);
-void MC_state_delete(mc_state_t state);
+void MC_state_delete(mc_state_t state, int free_snapshot);
void MC_state_interleave_process(mc_state_t state, smx_process_t process);
unsigned int MC_state_interleave_size(mc_state_t state);
int MC_state_process_is_done(mc_state_t state, smx_process_t process);
xbt_dynar_t visited_pairs;
xbt_dynar_t visited_states;
+static int is_exploration_stack_state(mc_visited_state_t state){
+ xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
+ while (item) {
+ if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){
+ ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0;
+ return 1;
+ }
+ item = xbt_fifo_get_prev_item(item);
+ }
+ return 0;
+}
+
void visited_state_free(mc_visited_state_t state)
{
if (state) {
- MC_free_snapshot(state->system_state);
+ if(!is_exploration_stack_state(state)){
+ MC_free_snapshot(state->system_state);
+ }
xbt_free(state);
}
}
return new_state;
}
-
-mc_visited_pair_t MC_visited_pair_new(int pair_num,
- xbt_automaton_state_t automaton_state,
- xbt_dynar_t atomic_propositions)
+mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_snapshot_t system_state)
{
mc_visited_pair_t pair = NULL;
pair = xbt_new0(s_mc_visited_pair_t, 1);
pair->graph_state = MC_state_new();
- pair->graph_state->system_state = MC_take_snapshot(pair_num);
+ pair->graph_state->system_state = (system_state == NULL) ? MC_take_snapshot(pair_num) : system_state;
pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
pair->nb_processes = xbt_swag_size(simix_global->process_list);
pair->automaton_state = automaton_state;
pair->acceptance_removed = 0;
pair->visited_removed = 0;
pair->acceptance_pair = 0;
+ pair->in_exploration_stack = 1;
pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
unsigned int cursor = 0;
int value;
return pair;
}
+static int is_exploration_stack_pair(mc_visited_pair_t pair){
+ xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
+ while (item) {
+ if (((mc_pair_t)xbt_fifo_get_item_content(item))->num == pair->num){
+ ((mc_pair_t)xbt_fifo_get_item_content(item))->visited_pair_removed = 1;
+ return 1;
+ }
+ item = xbt_fifo_get_prev_item(item);
+ }
+ return 0;
+}
+
void MC_visited_pair_delete(mc_visited_pair_t p)
{
p->automaton_state = NULL;
- MC_state_delete(p->graph_state);
+ MC_state_delete(p->graph_state, !is_exploration_stack_pair(p));
xbt_dynar_free(&(p->atomic_propositions));
xbt_free(p);
p = NULL;
while (start <= end) {
cursor = (start + end) / 2;
if (_sg_mc_liveness) {
- ref_test =
- (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
+ ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
} else {
- ref_test =
- (mc_visited_state_t) xbt_dynar_get_as(list, cursor,
- mc_visited_state_t);
+ ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, cursor, mc_visited_state_t);
nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
}
previous_cursor = cursor - 1;
while (previous_cursor >= 0) {
if (_sg_mc_liveness) {
- ref_test =
- (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor,
- mc_visited_pair_t);
+ ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_pair_t);
nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
- heap_bytes_used_test =
- ((mc_visited_pair_t) ref_test)->heap_bytes_used;
+ heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
} else {
- ref_test =
- (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor,
- mc_visited_state_t);
+ ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_state_t);
nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
- heap_bytes_used_test =
- ((mc_visited_state_t) ref_test)->heap_bytes_used;
+ heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
}
- if (nb_processes_test != nb_processes
- || heap_bytes_used_test != heap_bytes_used)
+ if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
break;
*min = previous_cursor;
previous_cursor--;
next_cursor = cursor + 1;
while (next_cursor < xbt_dynar_length(list)) {
if (_sg_mc_liveness) {
- ref_test =
- (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor,
- mc_visited_pair_t);
+ ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t);
nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
- heap_bytes_used_test =
- ((mc_visited_pair_t) ref_test)->heap_bytes_used;
+ heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
} else {
- ref_test =
- (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor,
- mc_visited_state_t);
+ ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, mc_visited_state_t);
nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
- heap_bytes_used_test =
- ((mc_visited_state_t) ref_test)->heap_bytes_used;
+ heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
}
- if (nb_processes_test != nb_processes
- || heap_bytes_used_test != heap_bytes_used)
+ if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
break;
*max = next_cursor;
next_cursor++;
MC_SET_MC_HEAP;
mc_visited_state_t new_state = visited_state_new();
+ graph_state->system_state = new_state->system_state;
+ graph_state->in_visited_states = 1;
+ XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
if (xbt_dynar_is_empty(visited_states)) {
return new_state->other_num;
} */
- cursor = min;
- while (cursor <= max) {
- state_test =
- (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor,
- mc_visited_state_t);
- if (snapshot_compare(state_test, new_state) == 0) {
- // The state has been visited:
-
- if (state_test->other_num == -1)
- new_state->other_num = state_test->num;
- else
- new_state->other_num = state_test->other_num;
- if (dot_output == NULL)
- XBT_DEBUG("State %d already visited ! (equal to state %d)",
- new_state->num, state_test->num);
- else
- XBT_DEBUG
- ("State %d already visited ! (equal to state %d (state %d in dot_output))",
- new_state->num, state_test->num, new_state->other_num);
-
- /* Replace the old state with the new one (with a bigger num)
- (when the max number of visited states is reached, the oldest
- one is removed according to its number (= with the min number) */
- xbt_dynar_remove_at(visited_states, cursor, NULL);
- xbt_dynar_insert_at(visited_states, cursor, &new_state);
-
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
- return state_test;
+ if(!partial_comm && initial_global_state->initial_communications_pattern_done){
+
+ cursor = min;
+ while (cursor <= max) {
+ state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
+ if (snapshot_compare(state_test, new_state) == 0) {
+ // The state has been visited:
+
+ if (state_test->other_num == -1)
+ new_state->other_num = state_test->num;
+ else
+ new_state->other_num = state_test->other_num;
+ if (dot_output == NULL)
+ XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
+ else
+ XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
+
+ /* Replace the old state with the new one (with a bigger num)
+ (when the max number of visited states is reached, the oldest
+ one is removed according to its number (= with the min number) */
+ xbt_dynar_remove_at(visited_states, cursor, NULL);
+ xbt_dynar_insert_at(visited_states, cursor, &new_state);
+ XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
+
+ if (!mc_mem_set)
+ MC_SET_STD_HEAP;
+ return state_test;
+ }
+ cursor++;
}
- cursor++;
}
-
- // The state has not been visited: insert the state in the dynamic array.
+
xbt_dynar_insert_at(visited_states, min, &new_state);
-
+ XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
+
} else {
// The state has not been visited: insert the state in the dynamic array.
- state_test =
- (mc_visited_state_t) xbt_dynar_get_as(visited_states, index,
- mc_visited_state_t);
+ state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
if (state_test->nb_processes < new_state->nb_processes) {
xbt_dynar_insert_at(visited_states, index + 1, &new_state);
} else {
xbt_dynar_insert_at(visited_states, index, &new_state);
}
+ XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
+
}
// We have reached the maximum number of stored states;
if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
+ XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
+
// Find the (index of the) older state (with the smallest num):
int min2 = mc_stats->expanded_states;
unsigned int cursor2 = 0;
// and drop it:
xbt_dynar_remove_at(visited_states, index2, NULL);
+ XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
}
if (!mc_mem_set)
/**
* \brief Checks whether a given pair has already been visited by the algorithm.
*/
-int is_visited_pair(mc_visited_pair_t pair, int pair_num,
- xbt_automaton_state_t automaton_state,
- xbt_dynar_t atomic_propositions)
-{
+int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
if (_sg_mc_visited == 0)
return -1;
MC_SET_MC_HEAP;
- mc_visited_pair_t new_pair = NULL;
+ mc_visited_pair_t new_visited_pair = NULL;
- if (pair == NULL) {
- new_pair =
- MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
+ if (visited_pair == NULL) {
+ new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state->system_state);
} else {
- new_pair = pair;
+ new_visited_pair = visited_pair;
}
if (xbt_dynar_is_empty(visited_pairs)) {
- xbt_dynar_push(visited_pairs, &new_pair);
+ xbt_dynar_push(visited_pairs, &new_visited_pair);
} else {
mc_visited_pair_t pair_test;
int cursor;
- index = get_search_interval(visited_pairs, new_pair, &min, &max);
+ index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
/*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
} */
cursor = min;
while (cursor <= max) {
- pair_test =
- (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor,
- mc_visited_pair_t);
- if (xbt_automaton_state_compare
- (pair_test->automaton_state, new_pair->automaton_state) == 0) {
- if (xbt_automaton_propositional_symbols_compare_value
- (pair_test->atomic_propositions,
- new_pair->atomic_propositions) == 0) {
- if (snapshot_compare(pair_test, new_pair) == 0) {
+ pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
+ if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
+ if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) {
+ if (snapshot_compare(pair_test, new_visited_pair) == 0) {
if (pair_test->other_num == -1)
- new_pair->other_num = pair_test->num;
+ new_visited_pair->other_num = pair_test->num;
else
- new_pair->other_num = pair_test->other_num;
+ new_visited_pair->other_num = pair_test->other_num;
if (dot_output == NULL)
- XBT_DEBUG("Pair %d already visited ! (equal to pair %d)",
- new_pair->num, pair_test->num);
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
else
- XBT_DEBUG
- ("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
- new_pair->num, pair_test->num, new_pair->other_num);
- xbt_dynar_remove_at(visited_pairs, cursor, NULL);
- xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
+ xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
+ xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
pair_test->visited_removed = 1;
if (pair_test->acceptance_pair) {
if (pair_test->acceptance_removed == 1)
}
if (!mc_mem_set)
MC_SET_STD_HEAP;
- return new_pair->other_num;
+ return new_visited_pair->other_num;
}
}
}
cursor++;
}
- xbt_dynar_insert_at(visited_pairs, min, &new_pair);
+ xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
} else {
- pair_test =
- (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index,
- mc_visited_pair_t);
- if (pair_test->nb_processes < new_pair->nb_processes) {
- xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
+ pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
+ if (pair_test->nb_processes < new_visited_pair->nb_processes) {
+ xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
} else {
- if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
- xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
+ if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
+ xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
else
- xbt_dynar_insert_at(visited_pairs, index, &new_pair);
+ xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
}
}
