From: Marion Guthmuller Date: Tue, 18 Feb 2014 14:33:13 +0000 (+0100) Subject: model-checker : new configuration flag for the detection of determinism in communicat... X-Git-Tag: v3_11~199^2~2^2~28 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/c2086224c80533a59cd9df04879935b5803a98df?hp=5769c08dcefe3f52a7464ba24fb8a20d3ca06a46 model-checker : new configuration flag for the detection of determinism in communications schemes --- diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index 0cf9f2d17c..28f184b598 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -29,6 +29,7 @@ extern int _sg_mc_timeout; extern int _sg_mc_max_depth; extern int _sg_mc_visited; extern char* _sg_mc_dot_output_file; +extern int _sg_mc_comms_determinism; extern xbt_dynar_t mc_heap_comparison_ignore; extern xbt_dynar_t stacks_areas; @@ -43,6 +44,7 @@ void _mc_cfg_cb_timeout(const char *name, int pos); void _mc_cfg_cb_max_depth(const char *name, int pos); void _mc_cfg_cb_visited(const char *name, int pos); void _mc_cfg_cb_dot_output(const char *name, int pos); +void _mc_cfg_cb_comms_determinism(const char *name, int pos); XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void); diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c index f1e7de3483..a45cc5f31e 100644 --- a/src/mc/mc_dpor.c +++ b/src/mc/mc_dpor.c @@ -423,15 +423,15 @@ void MC_dpor(void) 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, restore_state=NULL; + mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restored_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; - int comm_pattern = 0; int interleave_size = 0; + int comm_pattern = 0; while (xbt_fifo_size(mc_stack_safety) > 0) { @@ -474,25 +474,28 @@ void MC_dpor(void) xbt_dict_remove(first_enabled_state, key); xbt_free(key); MC_UNSET_RAW_MEM; - - if(req->call == SIMCALL_COMM_ISEND) - comm_pattern = 1; - else if(req->call == SIMCALL_COMM_IRECV) - comm_pattern = 2; + + if(_sg_mc_comms_determinism){ + if(req->call == SIMCALL_COMM_ISEND) + comm_pattern = 1; + else if(req->call == SIMCALL_COMM_IRECV) + comm_pattern = 2; + } /* Answer the request */ SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */ - MC_SET_RAW_MEM; - if(comm_pattern != 0){ - if(!initial_state_safety->initial_communications_pattern_done) - get_comm_pattern(initial_communications_pattern, req, comm_pattern); - else - get_comm_pattern(communications_pattern, req, comm_pattern); + if(_sg_mc_comms_determinism){ + MC_SET_RAW_MEM; + if(comm_pattern != 0){ + if(!initial_state_safety->initial_communications_pattern_done) + get_comm_pattern(initial_communications_pattern, req, comm_pattern); + else + get_comm_pattern(communications_pattern, req, comm_pattern); + } + MC_UNSET_RAW_MEM; + comm_pattern = 0; } - MC_UNSET_RAW_MEM; - - comm_pattern = 0; /* Wait for requests (schedules processes) */ MC_wait_for_requests(); @@ -586,22 +589,24 @@ void MC_dpor(void) } MC_SET_RAW_MEM; - if(!initial_state_safety->initial_communications_pattern_done){ - //print_communications_pattern(initial_communications_pattern); - }else{ - if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */ - //print_communications_pattern(communications_pattern); - deterministic_pattern(initial_communications_pattern, communications_pattern); + + if(_sg_mc_comms_determinism){ + if(!initial_state_safety->initial_communications_pattern_done){ + //print_communications_pattern(initial_communications_pattern); + }else{ + if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */ + //print_communications_pattern(communications_pattern); + deterministic_pattern(initial_communications_pattern, communications_pattern); + } } + initial_state_safety->initial_communications_pattern_done = 1; } - initial_state_safety->initial_communications_pattern_done = 1; - MC_UNSET_RAW_MEM; /* Trash the current state, no longer needed */ - MC_SET_RAW_MEM; xbt_fifo_shift(mc_stack_safety); MC_state_delete(state); XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1); + MC_UNSET_RAW_MEM; /* Check for deadlocks */ @@ -667,15 +672,15 @@ void MC_dpor(void) pos = xbt_fifo_size(mc_stack_safety); item = xbt_fifo_get_first_item(mc_stack_safety); while(pos>0){ - restore_state = (mc_state_t) xbt_fifo_get_item_content(item); - if(restore_state->system_state != NULL){ + 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(restore_state->system_state); + MC_restore_snapshot(restored_state->system_state); xbt_fifo_unshift(mc_stack_safety, state); MC_UNSET_RAW_MEM; MC_replay(mc_stack_safety, pos); @@ -689,9 +694,11 @@ void MC_dpor(void) break; } else { req = MC_state_get_internal_request(state); - if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){ - if(!xbt_dynar_is_empty(communications_pattern)) - xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL); + if(_sg_mc_comms_determinism){ + if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){ + if(!xbt_dynar_is_empty(communications_pattern)) + xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL); + } } XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1); MC_state_delete(state); diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 930098f814..a72abfea07 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -35,6 +35,7 @@ int _sg_mc_timeout=0; int _sg_mc_max_depth=1000; int _sg_mc_visited=0; char *_sg_mc_dot_output_file = NULL; +int _sg_mc_comms_determinism=0; int user_max_depth_reached = 0; @@ -93,6 +94,13 @@ void _mc_cfg_cb_dot_output(const char *name, int pos) { _sg_mc_dot_output_file= xbt_cfg_get_string(_sg_cfg_set, name); } +void _mc_cfg_cb_comms_determinism(const char *name, int pos) { + if (_sg_cfg_init_status && !_sg_do_model_check) { + xbt_die("You are specifying a value to enable/disable the detection of determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry."); + } + _sg_mc_comms_determinism= xbt_cfg_get_boolean(_sg_cfg_set, name); +} + /* MC global data structures */ mc_state_t mc_current_state = NULL; char mc_replay_mode = FALSE; @@ -1262,7 +1270,8 @@ void MC_replay(xbt_fifo_t stack, int start) xbt_free(key); } } - xbt_dynar_reset(communications_pattern); + if(_sg_mc_comms_determinism) + xbt_dynar_reset(communications_pattern); MC_UNSET_RAW_MEM; @@ -1293,20 +1302,23 @@ void MC_replay(xbt_fifo_t stack, int start) } } - if(req->call == SIMCALL_COMM_ISEND) - comm_pattern = 1; - else if(req->call == SIMCALL_COMM_IRECV) + if(_sg_mc_comms_determinism){ + if(req->call == SIMCALL_COMM_ISEND) + comm_pattern = 1; + else if(req->call == SIMCALL_COMM_IRECV) comm_pattern = 2; - + } + SIMIX_simcall_pre(req, value); - MC_SET_RAW_MEM; - if(comm_pattern != 0){ - get_comm_pattern(communications_pattern, req, comm_pattern); + if(_sg_mc_comms_determinism){ + MC_SET_RAW_MEM; + if(comm_pattern != 0){ + get_comm_pattern(communications_pattern, req, comm_pattern); + } + MC_UNSET_RAW_MEM; + comm_pattern = 0; } - MC_UNSET_RAW_MEM; - - comm_pattern = 0; MC_wait_for_requests(); @@ -1588,7 +1600,7 @@ void MC_print_statistics(mc_stats_t stats) fprintf(dot_output, "}\n"); fclose(dot_output); } - if(initial_state_safety != NULL){ + if(initial_state_safety != NULL && _sg_mc_comms_determinism){ XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes"); XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes"); } diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c index b812c87d55..0d904ae5a8 100644 --- a/src/simgrid/sg_config.c +++ b/src/simgrid/sg_config.c @@ -574,6 +574,12 @@ void sg_config_init(int *argc, char **argv) xbt_cfgelm_string, 0, 1, _mc_cfg_cb_property, NULL); xbt_cfg_setdefault_string(_sg_cfg_set, "model-check/property", ""); + /* do determinism model-checking */ + xbt_cfg_register(&_sg_cfg_set, "model-check/communications_determinism", + "Enable/disable the detection of determinism in the communications schemes", + xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_comms_determinism, NULL); + xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/communications_determinism", "no"); + /* Specify the kind of model-checking reduction */ xbt_cfg_register(&_sg_cfg_set, "model-check/reduction", "Specify the kind of exploration reduction (either none or DPOR)",