From 5a4767e64e45de2c17e9bbdcdf9c8588dbce80b0 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Mon, 11 Feb 2013 09:01:36 +0100 Subject: [PATCH 1/1] model-checker : new simcall MC_RANDOM --- include/simgrid/simix.h | 1 + src/mc/mc_global.c | 7 ++++++- src/mc/mc_private.h | 2 ++ src/mc/mc_request.c | 17 +++++++++++++++-- src/mc/mc_state.c | 20 ++++++++++++++++++++ src/simix/smx_smurf_private.h | 3 ++- src/simix/smx_user.c | 6 ++++++ 7 files changed, 52 insertions(+), 4 deletions(-) diff --git a/include/simgrid/simix.h b/include/simgrid/simix.h index 7dfab37cda..8d3ed6b27f 100644 --- a/include/simgrid/simix.h +++ b/include/simgrid/simix.h @@ -478,6 +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); /************************** New API simcalls **********************************/ /* TUTORIAL: New API */ diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index f226c9cfe5..72714a3341 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -303,11 +303,16 @@ void MC_exit(void) xbt_abort(); } +int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max){ + + return simcall->mc_value; +} + int MC_random(int min, int max) { /*FIXME: return mc_current_state->executed_transition->random.value;*/ - return 0; + return simcall_mc_random(min, max); } /** diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 865e1cb04b..699a467a12 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -74,6 +74,8 @@ 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); + /********************************* Requests ***********************************/ int MC_request_depend(smx_simcall_t req1, smx_simcall_t req2); char* MC_request_to_string(smx_simcall_t req, int value); diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c index 1033bfcfde..4e12e96064 100644 --- a/src/mc/mc_request.c +++ b/src/mc/mc_request.c @@ -18,6 +18,9 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) { if (r1->issuer == r2->issuer) return FALSE; + if((r1->call == SIMCALL_MC_RANDOM) || (r2->call == SIMCALL_MC_RANDOM)) + return FALSE; + if(r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_IRECV) return FALSE; @@ -248,13 +251,22 @@ char *MC_request_to_string(smx_simcall_t req, int value) args = '\0'; break; + case SIMCALL_MC_RANDOM: + type = xbt_strdup("MC_RANDOM"); + args = '\0'; + break; + default: THROW_UNIMPLEMENTED; } - str = bprintf("[(%lu)%s] %s (%s)", req->issuer->pid ,req->issuer->name, type, args); + if(args != NULL){ + str = bprintf("[(%lu)%s] %s (%s)", req->issuer->pid ,req->issuer->name, type, args); + xbt_free(args); + }else{ + str = bprintf("[(%lu)%s] %s ", req->issuer->pid ,req->issuer->name, type); + } xbt_free(type); - xbt_free(args); xbt_free(p); xbt_free(bs); return str; @@ -281,6 +293,7 @@ int MC_request_is_visible(smx_simcall_t req) || req->call == SIMCALL_COMM_WAITANY || req->call == SIMCALL_COMM_TEST || req->call == SIMCALL_COMM_TESTANY + || req->call == SIMCALL_MC_RANDOM || req->call == SIMCALL_MC_SNAPSHOT || req->call == SIMCALL_MC_COMPARE_SNAPSHOTS; } diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c index 4d41ba1797..d43a6bc7a2 100644 --- a/src/mc/mc_state.c +++ b/src/mc/mc_state.c @@ -117,6 +117,11 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int valu simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm); break; + case SIMCALL_MC_RANDOM: + state->internal_req = *req; + simcall_mc_random__set__result(&state->internal_req, value); + break; + default: state->internal_req = *req; break; @@ -139,6 +144,13 @@ 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]; @@ -193,6 +205,14 @@ 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); + procstate->state = MC_DONE; + return &process->simcall; + break; + default: procstate->state = MC_DONE; *value = 0; diff --git a/src/simix/smx_smurf_private.h b/src/simix/smx_smurf_private.h index db8bf142d0..e4224a1ddd 100644 --- a/src/simix/smx_smurf_private.h +++ b/src/simix/smx_smurf_private.h @@ -367,7 +367,8 @@ ACTION(SIMCALL_SET_CATEGORY, set_category, WITH_ANSWER, TVOID(result), TSPEC(act #ifdef HAVE_MC #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_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 #else #define SIMCALL_LIST4(ACTION, sep) #endif diff --git a/src/simix/smx_user.c b/src/simix/smx_user.c index 6d8a67c947..ae4749f045 100644 --- a/src/simix/smx_user.c +++ b/src/simix/smx_user.c @@ -1161,6 +1161,12 @@ 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) +{ + return simcall_BODY_mc_random(min, max); +} + + #endif /* HAVE_MC */ /* ****************************************************************************************** */ -- 2.20.1