From: cristianrosa Date: Wed, 5 Jan 2011 09:02:32 +0000 (+0000) Subject: Replace the setsets in the MC's states by malloced arrays. X-Git-Tag: v3.6_beta2~573 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/32df02dabc4562d5bb8dbd0e54fb026cd6534376 Replace the setsets in the MC's states by malloced arrays. In the case that a process has multiple transitions enabled (like when executing a waitany request) the process should be several times in the interleave set, so we need multisets, and the setsets are useless. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/simgrid/simgrid/trunk@9355 48e7efb5-ca39-0410-a469-dd3cf9ba447f --- diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index b4588480f6..1970b9cdf6 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -33,7 +33,7 @@ void MC_dpor_init() /* Get an enabled process and insert it in the interleave set of the initial state */ xbt_swag_foreach(process, simix_global->process_list){ if(SIMIX_process_is_enabled(process)){ - xbt_setset_set_insert(initial_state->interleave, process); + MC_state_add_to_interleave(initial_state, process); break; } } @@ -51,7 +51,8 @@ void MC_dpor_init() */ void MC_dpor(void) { - char *req_str, deadlock; + char *req_str; + char value; smx_req_t req = NULL; mc_state_t state = NULL, prev_state = NULL, next_state = NULL; smx_process_t process = NULL; @@ -59,65 +60,58 @@ void MC_dpor(void) while (xbt_fifo_size(mc_stack) > 0) { - DEBUG0("**************************************************"); - /* Get current state */ state = (mc_state_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack)); - /* If there are processes to interleave and the maximun depth has not been reached - then perform one step of the exploration algorithm */ - if (xbt_setset_set_size(state->interleave) > 0 - && xbt_fifo_size(mc_stack) < MAX_DEPTH) { + DEBUG0("**************************************************"); + DEBUG3("Exploration detph=%d (state=%p)(%u interleave)", + xbt_fifo_size(mc_stack), state, + MC_state_interleave_size(state)); - DEBUG3("Exploration detph=%d (state=%p)(%d interleave)", - xbt_fifo_size(mc_stack), state, - xbt_setset_set_size(state->interleave)); + /* Update statistics */ + mc_stats->visited_states++; - /* Update statistics */ - mc_stats->visited_states++; - mc_stats->executed_transitions++; + /* 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) < MAX_DEPTH && + (req = MC_state_get_request(state, &value))) { + + /* Debug information */ + if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){ + req_str = MC_request_to_string(req); + DEBUG1("Execute: %s", req_str); + xbt_free(req_str); + } - MC_SET_RAW_MEM; - /* Choose a request to execute from the the current state */ - req = MC_state_get_request(state); - MC_UNSET_RAW_MEM; + MC_state_set_executed_request(state, req); + mc_stats->executed_transitions++; - if(req){ - /* Answer the request */ - /* Debug information */ - if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){ - req_str = MC_request_to_string(req); - DEBUG1("Execute: %s", req_str); - xbt_free(req_str); - } + /* Answer the request */ + SIMIX_request_pre(req); /* After this call req is no longer usefull */ - MC_state_set_executed_request(state, req); + /* Wait for requests (schedules processes) */ + MC_wait_for_requests(); - SIMIX_request_pre(req); /* After this call req is no longer usefull */ - - /* Wait for requests (schedules processes) */ - MC_wait_for_requests(); + /* Create the new expanded state */ + MC_SET_RAW_MEM; + next_state = MC_state_new(); + xbt_fifo_unshift(mc_stack, next_state); - /* Create the new expanded state */ - MC_SET_RAW_MEM; - next_state = MC_state_new(); - xbt_fifo_unshift(mc_stack, next_state); - - /* Get an enabled process and insert it in the interleave set of the next state */ - xbt_swag_foreach(process, simix_global->process_list){ - if(SIMIX_process_is_enabled(process)){ - xbt_setset_set_insert(next_state->interleave, process); - break; - } + /* Get an enabled process and insert it in the interleave set of the next state */ + xbt_swag_foreach(process, simix_global->process_list){ + if(SIMIX_process_is_enabled(process)){ + MC_state_add_to_interleave(next_state, process); + break; } - MC_UNSET_RAW_MEM; - - /* FIXME: Update Statistics - mc_stats->state_size += - xbt_setset_set_size(next_state->enabled_transitions);*/ } + MC_UNSET_RAW_MEM; + + /* FIXME: Update Statistics + mc_stats->state_size += + xbt_setset_set_size(next_state->enabled_transitions);*/ + /* Let's loop again */ /* The interleave set is empty or the maximum depth is reached, let's back-track */ @@ -125,26 +119,11 @@ void MC_dpor(void) DEBUG0("There are no more processes to interleave."); /* Check for deadlocks */ - if(xbt_swag_size(simix_global->process_list)){ - deadlock = TRUE; - xbt_swag_foreach(process, simix_global->process_list){ - if(process->request.call != REQ_NO_REQ - && SIMIX_request_is_enabled(&process->request)){ - deadlock = FALSE; - break; - } - } - - if(deadlock){ - MC_show_deadlock(&process->request); - return; - } + if(MC_deadlock_check()){ + MC_show_deadlock(&process->request); + return; } - /* - INFO0("*********************************"); - MC_show_stack(mc_stack); */ - /* Trash the current state, no longer needed */ MC_SET_RAW_MEM; xbt_fifo_shift(mc_stack); @@ -170,15 +149,15 @@ void MC_dpor(void) xbt_free(req_str); } - if(!xbt_setset_set_belongs(prev_state->done, req->issuer)) - xbt_setset_set_insert(prev_state->interleave, req->issuer); + if(!MC_state_process_is_done(prev_state, req->issuer)) + MC_state_add_to_interleave(prev_state, req->issuer); else DEBUG1("Process %p is in done set", req->issuer); break; } } - if (xbt_setset_set_size(state->interleave) > 0) { + if (MC_state_interleave_size(state)) { /* We found a back-tracking point, let's loop */ xbt_fifo_unshift(mc_stack, state); DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack)); diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 9fa095a3e3..de02e74da1 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -14,7 +14,6 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, /* MC global data structures */ mc_snapshot_t initial_snapshot = NULL; xbt_fifo_t mc_stack = NULL; -xbt_setset_t mc_setset = NULL; mc_stats_t mc_stats = NULL; mc_state_t mc_current_state = NULL; char mc_replay_mode = FALSE; @@ -24,8 +23,6 @@ char mc_replay_mode = FALSE; */ void MC_init(void) { - smx_process_t process; - /* Check if MC is already initialized */ if (initial_snapshot) return; @@ -41,14 +38,6 @@ void MC_init(void) /* Create exploration stack */ mc_stack = xbt_fifo_new(); - /* Create the container for the sets */ - mc_setset = xbt_setset_new(20); - - /* Add the existing processes to mc's setset so they have an ID designated */ - /* FIXME: check what happen if there are processes created during the exploration */ - xbt_swag_foreach(process, simix_global->process_list){ - xbt_setset_elm_add(mc_setset, process); - } MC_UNSET_RAW_MEM; MC_dpor_init(); @@ -78,6 +67,47 @@ int MC_random(int min, int max) return 0; } +/** + * \brief Schedules all the process that are ready to run + */ +void MC_wait_for_requests(void) +{ + char *req_str = NULL; + smx_req_t req = NULL; + + do { + SIMIX_context_runall(simix_global->process_to_run); + while((req = SIMIX_request_pop())){ + if(!SIMIX_request_is_visible(req)) + SIMIX_request_pre(req); + else if(req->call == REQ_COMM_WAITANY) + THROW_UNIMPLEMENTED; + else if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){ + req_str = MC_request_to_string(req); + DEBUG1("Got: %s", req_str); + xbt_free(req_str); + } + } + } while (xbt_dynar_length(simix_global->process_to_run)); +} + +int MC_deadlock_check() +{ + int deadlock = FALSE; + smx_process_t process; + if(xbt_swag_size(simix_global->process_list)){ + deadlock = TRUE; + xbt_swag_foreach(process, simix_global->process_list){ + if(process->request.call != REQ_NO_REQ + && SIMIX_request_is_enabled(&process->request)){ + deadlock = FALSE; + break; + } + } + } + return deadlock; +} + /** * \brief Re-executes from the initial state all the transitions indicated by * a given model-checker stack. @@ -165,31 +195,20 @@ void MC_show_stack(xbt_fifo_t stack) } } -/** - * \brief Schedules all the process that are ready to run - */ -void MC_wait_for_requests(void) +void MC_show_deadlock(smx_req_t req) { char *req_str = NULL; - smx_req_t req = NULL; - - do { - SIMIX_context_runall(simix_global->process_to_run); - while((req = SIMIX_request_pop())){ - if(!SIMIX_request_is_visible(req)) - SIMIX_request_pre(req); - else if(req->call == REQ_COMM_WAITANY) - THROW_UNIMPLEMENTED; - else if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){ - req_str = MC_request_to_string(req); - DEBUG1("Got: %s", req_str); - xbt_free(req_str); - } - } - } while (xbt_dynar_length(simix_global->process_to_run)); + INFO0("**************************"); + INFO0("*** DEAD-LOCK DETECTED ***"); + INFO0("**************************"); + INFO0("Locked request:"); + req_str = MC_request_to_string(req); + INFO1("%s", req_str); + xbt_free(req_str); + INFO0("Counter-example execution trace:"); + MC_dump_stack(mc_stack); } -/****************************** Statistics ************************************/ void MC_print_statistics(mc_stats_t stats) { INFO1("State space size ~= %lu", stats->state_size); @@ -202,7 +221,6 @@ void MC_print_statistics(mc_stats_t stats) (double)stats->expanded_states / stats->state_size); */ } -/************************* Assertion Checking *********************************/ void MC_assert(int prop) { if (MC_IS_ENABLED && !prop) { @@ -216,16 +234,3 @@ void MC_assert(int prop) } } -void MC_show_deadlock(smx_req_t req) -{ - char *req_str = NULL; - INFO0("**************************"); - INFO0("*** DEAD-LOCK DETECTED ***"); - INFO0("**************************"); - INFO0("Locked request:"); - req_str = MC_request_to_string(req); - INFO1("%s", req_str); - xbt_free(req_str); - INFO0("Counter-example execution trace:"); - MC_dump_stack(mc_stack); -} diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c index f6ccb79637..4137ad30f4 100644 --- a/src/mc/mc_state.c +++ b/src/mc/mc_state.c @@ -12,8 +12,8 @@ mc_state_t MC_state_new(void) mc_state_t state = NULL; state = xbt_new0(s_mc_state_t, 1); - state->interleave = xbt_setset_new_set(mc_setset); - state->done = xbt_setset_new_set(mc_setset); + state->max_pid = simix_process_maxpid; + state->interleave = xbt_new0(char, state->max_pid); mc_stats->expanded_states++; return state; @@ -25,11 +25,31 @@ mc_state_t MC_state_new(void) */ void MC_state_delete(mc_state_t state) { - xbt_setset_destroy_set(state->interleave); - xbt_setset_destroy_set(state->done); + xbt_free(state->interleave); xbt_free(state); } +void MC_state_add_to_interleave(mc_state_t state, smx_process_t process) +{ + state->interleave[process->pid] = 1; +} + +unsigned int MC_state_interleave_size(mc_state_t state) +{ + unsigned int i, size=0; + + for(i=0; i < state->max_pid; i++){ + if(state->interleave[i] != 0 && state->interleave[i] != -1) + size++; + } + + return size; +} + +int MC_state_process_is_done(mc_state_t state, smx_process_t process){ + return state->interleave[process->pid] == -1 ? TRUE : FALSE; +} + void MC_state_set_executed_request(mc_state_t state, smx_req_t req) { state->executed = *req; @@ -40,16 +60,31 @@ smx_req_t MC_state_get_executed_request(mc_state_t state) return &state->executed; } -smx_req_t MC_state_get_request(mc_state_t state) +smx_req_t MC_state_get_request(mc_state_t state, char *value) { - smx_process_t process = NULL; - while((process = xbt_setset_set_extract(state->interleave))){ - if(SIMIX_process_is_enabled(process) - && !xbt_setset_set_belongs(state->done, process)){ - xbt_setset_set_insert(state->done, process); - return &process->request; + unsigned int i; + smx_process_t process = NULL; + + for(i=0; i < state->max_pid; i++){ + if(state->interleave[i] > 0){ + *value = state->interleave[i]--; + + /* If 0 was reached means that the process is done, so we + * set it's value to -1 (the "done" value) */ + if(state->interleave[i] == 0) + state->interleave[i]--; + + /* FIXME: SIMIX should implement a process table indexed by pid */ + /* So we should use that instead of traversing the swag */ + xbt_swag_foreach(process, simix_global->process_list){ + if(process->pid == i) + break; + } + + if(SIMIX_process_is_enabled(process)) + return &process->request; } } - + return NULL; } diff --git a/src/mc/private.h b/src/mc/private.h index 06af6e7c14..b5d91ac09d 100644 --- a/src/mc/private.h +++ b/src/mc/private.h @@ -14,7 +14,6 @@ #include "mc/mc.h" #include "mc/datatypes.h" #include "xbt/fifo.h" -#include "xbt/setset.h" #include "xbt/config.h" #include "xbt/function_types.h" #include "xbt/mmalloc.h" @@ -42,12 +41,13 @@ void MC_free_snapshot(mc_snapshot_t); /* Bound of the MC depth-first search algorithm */ #define MAX_DEPTH 1000 -void MC_show_stack(xbt_fifo_t stack); -void MC_dump_stack(xbt_fifo_t stack); +int MC_deadlock_check(void); void MC_replay(xbt_fifo_t stack); void MC_wait_for_requests(void); void MC_get_enabled_processes(); void MC_show_deadlock(smx_req_t req); +void MC_show_stack(xbt_fifo_t stack); +void MC_dump_stack(xbt_fifo_t stack); /********************************* Requests ***********************************/ int MC_request_depend(smx_req_t req1, smx_req_t req2); @@ -60,19 +60,21 @@ void MC_dpor_exit(void); /******************************** States **************************************/ typedef struct mc_state { - xbt_setset_set_t interleave; /* processes to interleave by the mc */ - xbt_setset_set_t done; /* already executed processes */ + char *interleave; /* processes to interleave by the mc */ + unsigned long max_pid; s_smx_req_t executed; } s_mc_state_t, *mc_state_t; extern xbt_fifo_t mc_stack; -extern xbt_setset_t mc_setset; mc_state_t MC_state_new(void); void MC_state_delete(mc_state_t state); +void MC_state_add_to_interleave(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); void MC_state_set_executed_request(mc_state_t state, smx_req_t req); smx_req_t MC_state_get_executed_request(mc_state_t state); -smx_req_t MC_state_get_request(mc_state_t state); +smx_req_t MC_state_get_request(mc_state_t state, char *value); /****************************** Statistics ************************************/ typedef struct mc_stats { diff --git a/src/simix/private.h b/src/simix/private.h index ee605a429b..b7978875d9 100644 --- a/src/simix/private.h +++ b/src/simix/private.h @@ -40,7 +40,7 @@ typedef struct s_smx_global { } s_smx_global_t, *smx_global_t; extern smx_global_t simix_global; - +extern unsigned long simix_process_maxpid; /*********************************** Time ************************************/ diff --git a/src/simix/smx_process.c b/src/simix/smx_process.c index 1fb254dc1b..85bd1ee631 100644 --- a/src/simix/smx_process.c +++ b/src/simix/smx_process.c @@ -14,7 +14,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_process, simix, "Logging specific to SIMIX (process)"); -static unsigned long simix_process_maxpid = 0; +unsigned long simix_process_maxpid = 0; /** * \brief Returns the current agent.