From: Marion Guthmuller Date: Wed, 13 Mar 2013 15:41:47 +0000 (+0100) Subject: model-checker : fix MC_RANDOM simcall X-Git-Tag: v3_9_90~446 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/4d27a92b07b781ad03da0848332a26c289358bc9 model-checker : fix MC_RANDOM simcall Time doesn't exist in model-checking. However, there are some protocols, such as Chord, with some periodics operations (random lookup, check predecessors, ...). If the model-checker is used with these examples, these operations are never executed because of the time which doesn't progress. With MC_RANDOM simcall, the model-checker will explore the two cases : the case in which the periodic operation is executed and the other case in which it is not executed. In this way, the verification is exhaustive whatever the period. --- diff --git a/examples/msg/chord/chord.c b/examples/msg/chord/chord.c index 14af6d0121..42b74caf8e 100644 --- a/examples/msg/chord/chord.c +++ b/examples/msg/chord/chord.c @@ -335,26 +335,42 @@ int node(int argc, char *argv[]) if (!MSG_comm_test(node.comm_receive)) { // no task was received: make some periodic calls - if (MSG_get_clock() >= next_stabilize_date) { - stabilize(&node); - next_stabilize_date = MSG_get_clock() + periodic_stabilize_delay; - } - else if (MSG_get_clock() >= next_fix_fingers_date) { - fix_fingers(&node); - next_fix_fingers_date = MSG_get_clock() + periodic_fix_fingers_delay; - } - else if (MSG_get_clock() >= next_check_predecessor_date) { - check_predecessor(&node); - next_check_predecessor_date = MSG_get_clock() + periodic_check_predecessor_delay; - } - else if (MSG_get_clock() >= next_lookup_date) { - random_lookup(&node); - next_lookup_date = MSG_get_clock() + periodic_lookup_delay; - } - else { - // nothing to do: sleep for a while - MSG_process_sleep(5); + + if(MC_is_active()){ + if(MC_random()){ + stabilize(&node); + }else if(MC_random()){ + fix_fingers(&node); + }else if(MC_random()){ + check_predecessor(&node); + }else if(MC_random()){ + random_lookup(&node); + }else{ + MSG_process_sleep(5); + } + }else{ + if (MSG_get_clock() >= next_stabilize_date) { + stabilize(&node); + next_stabilize_date = MSG_get_clock() + periodic_stabilize_delay; + } + else if (MSG_get_clock() >= next_fix_fingers_date) { + fix_fingers(&node); + next_fix_fingers_date = MSG_get_clock() + periodic_fix_fingers_delay; + } + else if (MSG_get_clock() >= next_check_predecessor_date) { + check_predecessor(&node); + next_check_predecessor_date = MSG_get_clock() + periodic_check_predecessor_delay; + } + else if (MSG_get_clock() >= next_lookup_date) { + random_lookup(&node); + next_lookup_date = MSG_get_clock() + periodic_lookup_delay; + } + else { + // nothing to do: sleep for a while + MSG_process_sleep(5); + } } + } else { // a transfer has occurred diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h index ae58a10401..18535fdefc 100644 --- a/include/simgrid/modelchecker.h +++ b/include/simgrid/modelchecker.h @@ -19,7 +19,7 @@ extern int _sg_do_model_check; /* please don't use directly: we inline MC_is_act #define MC_is_active() _sg_do_model_check XBT_PUBLIC(void) MC_assert(int); -XBT_PUBLIC(int) MC_random(int min, int max); +XBT_PUBLIC(int) MC_random(void); XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, void* fct); XBT_PUBLIC(void *) MC_snapshot(void); XBT_PUBLIC(int) MC_compare_snapshots(void *s1, void *s2); diff --git a/include/simgrid/simix.h b/include/simgrid/simix.h index 8d3ed6b27f..bd69b1909f 100644 --- a/include/simgrid/simix.h +++ b/include/simgrid/simix.h @@ -478,7 +478,7 @@ XBT_PUBLIC(xbt_dict_t) simcall_asr_get_properties(const char *name); /************************** MC simcalls **********************************/ XBT_PUBLIC(void *) simcall_mc_snapshot(void); XBT_PUBLIC(int) simcall_mc_compare_snapshots(void *s1, void *s2); -XBT_PUBLIC(int) simcall_mc_random(int min, int max); +XBT_PUBLIC(int) simcall_mc_random(void); /************************** New API simcalls **********************************/ /* TUTORIAL: New API */ diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index d67f00dadf..672765afd7 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -303,16 +303,16 @@ void MC_exit(void) xbt_abort(); } -int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max){ +int SIMIX_pre_mc_random(smx_simcall_t simcall){ return simcall->mc_value; } -int MC_random(int min, int max) +int MC_random(void) { /*FIXME: return mc_current_state->executed_transition->random.value;*/ - return simcall_mc_random(min, max); + return simcall_mc_random(); } /** diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 17e8c9a4bc..70b34dbd1f 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -72,8 +72,8 @@ void MC_wait_for_requests(void); 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); - -int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max); +void MC_init(void); +int SIMIX_pre_mc_random(smx_simcall_t simcall); /********************************* Requests ***********************************/ int MC_request_depend(smx_simcall_t req1, smx_simcall_t req2); @@ -91,6 +91,7 @@ int MC_process_is_enabled(smx_process_t process); typedef enum { MC_NOT_INTERLEAVE=0, /* Do not interleave (do not execute) */ MC_INTERLEAVE, /* Interleave the process (one or more request) */ + MC_MORE_INTERLEAVE, /* Interleave twice the process (for mc_random simcall) */ MC_DONE /* Already interleaved */ } e_mc_process_state_t; @@ -251,7 +252,6 @@ extern mc_global_t initial_state_safety; void MC_dpor_init(void); void MC_dpor(void); -void MC_init(void); typedef struct s_mc_safety_visited_state{ mc_snapshot_t system_state; diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c index 4e12e96064..ea801b5974 100644 --- a/src/mc/mc_request.c +++ b/src/mc/mc_request.c @@ -16,10 +16,7 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) { return TRUE; if (r1->issuer == r2->issuer) - return FALSE; - - if((r1->call == SIMCALL_MC_RANDOM) || (r2->call == SIMCALL_MC_RANDOM)) - return FALSE; + return FALSE; if(r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_IRECV) return FALSE; @@ -253,7 +250,7 @@ char *MC_request_to_string(smx_simcall_t req, int value) case SIMCALL_MC_RANDOM: type = xbt_strdup("MC_RANDOM"); - args = '\0'; + args = bprintf("%d", value); break; default: diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c index d43a6bc7a2..29621f18fa 100644 --- a/src/mc/mc_state.c +++ b/src/mc/mc_state.c @@ -64,7 +64,7 @@ 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->proc_status[i].state == MC_INTERLEAVE) + if((state->proc_status[i].state == MC_INTERLEAVE) || (state->proc_status[i].state == MC_MORE_INTERLEAVE)) size++; } @@ -79,6 +79,8 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int valu { state->executed_req = *req; state->req_num = value; + smx_process_t process = NULL; + mc_procstate_t procstate = NULL; /* The waitany and testany request are transformed into a wait or test request over the * corresponding communication action so it can be treated later by the dependence @@ -120,6 +122,15 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int valu case SIMCALL_MC_RANDOM: state->internal_req = *req; simcall_mc_random__set__result(&state->internal_req, value); + if(value == 0){ + xbt_swag_foreach(process, simix_global->process_list){ + procstate = &state->proc_status[process->pid]; + if(process->pid == req->issuer->pid){ + procstate->state = MC_MORE_INTERLEAVE; + break; + } + } + } break; default: @@ -127,7 +138,7 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int valu break; } } - + smx_simcall_t MC_state_get_executed_request(mc_state_t state, int *value) { *value = state->req_num; @@ -144,18 +155,11 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value) smx_process_t process = NULL; mc_procstate_t procstate = NULL; unsigned int start_count; - int min, max; - - static int first = 0; - if(first == 0){ - srand(987654321); - first = 1; - } xbt_swag_foreach(process, simix_global->process_list){ procstate = &state->proc_status[process->pid]; - if(procstate->state == MC_INTERLEAVE){ + if(procstate->state == MC_INTERLEAVE || procstate->state == MC_MORE_INTERLEAVE){ if(MC_process_is_enabled(process)){ switch(process->simcall.call){ case SIMCALL_COMM_WAITANY: @@ -206,9 +210,10 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value) break; case SIMCALL_MC_RANDOM: - min = simcall_mc_random__get__min(&process->simcall); - max = simcall_mc_random__get__max(&process->simcall); - *value = (int)((rand() % ((max-min)+1)) + min); + if(procstate->state == MC_INTERLEAVE) + *value = 0; + else + *value = 1; procstate->state = MC_DONE; return &process->simcall; break; diff --git a/src/simix/smx_smurf_private.h b/src/simix/smx_smurf_private.h index e4224a1ddd..c55fa360f2 100644 --- a/src/simix/smx_smurf_private.h +++ b/src/simix/smx_smurf_private.h @@ -368,7 +368,7 @@ ACTION(SIMCALL_SET_CATEGORY, set_category, WITH_ANSWER, TVOID(result), TSPEC(act #define SIMCALL_LIST4(ACTION, sep) \ ACTION(SIMCALL_MC_SNAPSHOT, mc_snapshot, WITH_ANSWER, TPTR(result)) sep \ ACTION(SIMCALL_MC_COMPARE_SNAPSHOTS, mc_compare_snapshots, WITH_ANSWER, TINT(result), TPTR(s1), TPTR(s2)) sep \ -ACTION(SIMCALL_MC_RANDOM, mc_random, WITH_ANSWER, TINT(result), TINT(min), TINT(max)) sep +ACTION(SIMCALL_MC_RANDOM, mc_random, WITH_ANSWER, TINT(result)) sep #else #define SIMCALL_LIST4(ACTION, sep) #endif diff --git a/src/simix/smx_user.c b/src/simix/smx_user.c index ae4749f045..a23e346f98 100644 --- a/src/simix/smx_user.c +++ b/src/simix/smx_user.c @@ -1161,9 +1161,9 @@ int simcall_mc_compare_snapshots(void *s1, void *s2){ return simcall_BODY_mc_compare_snapshots(s1, s2); } -int simcall_mc_random(int min, int max) +int simcall_mc_random(void) { - return simcall_BODY_mc_random(min, max); + return simcall_BODY_mc_random(); }