X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/984b8e1616cfd626c6244a34ccd42ee0b1e89bcd..ab23fd586c00bc3e9ea24f1dcd3d52dd0fc60bce:/src/mc/mc_global.c diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index f62e2f7230..bee23e103c 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -18,12 +18,48 @@ XBT_LOG_NEW_CATEGORY(mc, "All MC categories"); XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, "Logging specific to MC (global)"); +/* Configuration support */ +e_mc_reduce_t mc_reduce_kind=e_mc_reduce_unset; + +extern int _surf_init_status; +void _mc_cfg_cb_reduce(const char *name, int pos) { + if (_surf_init_status && !_surf_do_model_check) { + xbt_die("You are specifying a reduction strategy 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."); + } + char *val= xbt_cfg_get_string(_surf_cfg_set, name); + if (!strcasecmp(val,"none")) { + mc_reduce_kind = e_mc_reduce_none; + } else if (!strcasecmp(val,"dpor")) { + mc_reduce_kind = e_mc_reduce_dpor; + } else { + xbt_die("configuration option %s can only take 'none' or 'dpor' as a value",name); + } + xbt_cfg_set_int(_surf_cfg_set,"model-check",1); +} + +void _mc_cfg_cb_checkpoint(const char *name, int pos) { + if (_surf_init_status && !_surf_do_model_check) { + xbt_die("You are specifying a checkpointing value 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."); + } + _surf_mc_checkpoint = xbt_cfg_get_int(_surf_cfg_set, name); + xbt_cfg_set_int(_surf_cfg_set,"model-check",1); +} +void _mc_cfg_cb_property(const char *name, int pos) { + if (_surf_init_status && !_surf_do_model_check) { + xbt_die("You are specifying a property 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."); + } + _surf_mc_property_file= xbt_cfg_get_string(_surf_cfg_set, name); + xbt_cfg_set_int(_surf_cfg_set,"model-check",1); +} + + /* MC global data structures */ mc_state_t mc_current_state = NULL; char mc_replay_mode = FALSE; double *mc_time = NULL; mc_snapshot_t initial_snapshot = NULL; +int raw_mem_set; /* Safety */ @@ -35,11 +71,30 @@ mc_stats_t mc_stats = NULL; mc_stats_pair_t mc_stats_pair = NULL; xbt_fifo_t mc_stack_liveness = NULL; mc_snapshot_t initial_snapshot_liveness = NULL; +int compare; xbt_automaton_t _mc_property_automaton = NULL; static void MC_assert_pair(int prop); +void MC_do_the_modelcheck_for_real() { + if (!_surf_mc_property_file || _surf_mc_property_file[0]=='\0') { + if (mc_reduce_kind==e_mc_reduce_unset) + mc_reduce_kind=e_mc_reduce_dpor; + + XBT_INFO("Check a safety property"); + MC_modelcheck(); + + } else { + + if (mc_reduce_kind==e_mc_reduce_unset) + mc_reduce_kind=e_mc_reduce_none; + + XBT_INFO("Check the liveness property %s",_surf_mc_property_file); + MC_automaton_load(_surf_mc_property_file); + MC_modelcheck_liveness(); + } +} /** * \brief Initialize the model-checker data structures @@ -47,6 +102,8 @@ static void MC_assert_pair(int prop); void MC_init_safety(void) { + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + /* Check if MC is already initialized */ if (initial_snapshot) return; @@ -55,6 +112,7 @@ void MC_init_safety(void) /* Initialize the data structures that must be persistent across every iteration of the model-checker (in RAW memory) */ + MC_SET_RAW_MEM; /* Initialize statistics */ @@ -74,8 +132,17 @@ void MC_init_safety(void) MC_take_snapshot(initial_snapshot); MC_UNSET_RAW_MEM; + + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + } +void MC_compare(void){ + compare = 1; +} void MC_modelcheck(void) @@ -86,11 +153,16 @@ void MC_modelcheck(void) } void MC_modelcheck_liveness(){ + + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + /* init stuff */ XBT_DEBUG("Start init mc"); mc_time = xbt_new0(double, simix_process_maxpid); + compare = 0; + /* Initialize the data structures that must be persistent across every iteration of the model-checker (in RAW memory) */ @@ -111,8 +183,8 @@ void MC_modelcheck_liveness(){ /* We're done */ MC_print_statistics_pairs(mc_stats_pair); - //xbt_free(mc_time); - //MC_memory_exit(); + xbt_free(mc_time); + MC_memory_exit(); exit(0); } @@ -175,6 +247,8 @@ int MC_deadlock_check() */ void MC_replay(xbt_fifo_t stack, int start) { + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int value, i = 1; char *req_str; smx_simcall_t req = NULL, saved_req = NULL; @@ -228,10 +302,20 @@ void MC_replay(xbt_fifo_t stack, int start) mc_stats->executed_transitions++; } XBT_DEBUG("**** End Replay ****"); + + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + + } void MC_replay_liveness(xbt_fifo_t stack, int all_stack) { + + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int value; char *req_str; smx_simcall_t req = NULL, saved_req = NULL; @@ -331,6 +415,12 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) } XBT_DEBUG("**** End Replay ****"); + + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + } /** @@ -340,10 +430,12 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) */ void MC_dump_stack_safety(xbt_fifo_t stack) { + + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_show_stack_safety(stack); - if(!_surf_do_mc_checkpoint){ + if(!_surf_mc_checkpoint){ mc_state_t state; @@ -353,6 +445,12 @@ void MC_dump_stack_safety(xbt_fifo_t stack) MC_UNSET_RAW_MEM; } + + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + } @@ -415,12 +513,21 @@ void MC_show_stack_liveness(xbt_fifo_t stack){ } void MC_dump_stack_liveness(xbt_fifo_t stack){ + + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + mc_pair_stateless_t pair; MC_SET_RAW_MEM; while ((pair = (mc_pair_stateless_t) xbt_fifo_pop(stack)) != NULL) MC_pair_stateless_delete(pair); MC_UNSET_RAW_MEM; + + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + } @@ -486,49 +593,42 @@ double MC_process_clock_get(smx_process_t process) return 0; } -void MC_diff(void){ - - mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1); - MC_take_snapshot_liveness(sn); - - int i; - - XBT_INFO("Number of regions : %u", sn->num_reg); - - for(i=0; inum_reg; i++){ - - switch(sn->regions[i]->type){ - case 0: /* heap */ - XBT_INFO("Size of heap : %zu", sn->regions[i]->size); - mmalloc_display_info_heap(sn->regions[i]->data); - break; - case 1 : /* libsimgrid */ - XBT_INFO("Size of libsimgrid : %zu", sn->regions[i]->size); - break; - case 2 : /* data program */ - XBT_INFO("Size of data program : %zu", sn->regions[i]->size); - break; - case 3 : /* stack */ - XBT_INFO("Size of stack : %zu", sn->regions[i]->size); - XBT_INFO("Start addr of stack : %p", sn->regions[i]->start_addr); - break; - } +void MC_automaton_load(const char *file){ - } + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); -} - -void MC_automaton_load(const char *file){ MC_SET_RAW_MEM; + if (_mc_property_automaton == NULL) _mc_property_automaton = xbt_automaton_new(); + xbt_automaton_load(_mc_property_automaton,file); + MC_UNSET_RAW_MEM; + + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + } + void MC_automaton_new_propositional_symbol(const char* id, void* fct) { + + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + MC_SET_RAW_MEM; + if (_mc_property_automaton == NULL) _mc_property_automaton = xbt_automaton_new(); + xbt_new_propositional_symbol(_mc_property_automaton,id,fct); + MC_UNSET_RAW_MEM; + + if(raw_mem_set) + MC_SET_RAW_MEM; + else + MC_UNSET_RAW_MEM; + }