X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/82bebb568ecbca2bcac029c94e62e7e332743a58..db0a9953a8faae6543ea75f4f87a4ada0af4bd22:/src/mc/mc_global.c diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 1359cf3c3d..42a7127a79 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -30,7 +30,7 @@ e_mc_reduce_t mc_reduce_kind = e_mc_reduce_unset; int _sg_do_model_check = 0; int _sg_mc_checkpoint = 0; int _sg_mc_sparse_checkpoint = 0; -int _sg_mc_soft_dirty = 1; +int _sg_mc_soft_dirty = 0; char *_sg_mc_property_file = NULL; int _sg_mc_timeout = 0; int _sg_mc_hash = 0; @@ -145,6 +145,7 @@ void _mc_cfg_cb_comms_determinism(const char *name, int pos) ("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_reduce_kind = e_mc_reduce_none; } void _mc_cfg_cb_send_determinism(const char *name, int pos) @@ -154,6 +155,7 @@ void _mc_cfg_cb_send_determinism(const char *name, int pos) ("You are specifying a value to enable/disable the detection of send-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_send_determinism = xbt_cfg_get_boolean(_sg_cfg_set, name); + mc_reduce_kind = e_mc_reduce_none; } /* MC global data structures */ @@ -302,6 +304,9 @@ void MC_init() MC_ignore_global_variable("maestro_stack_start"); MC_ignore_global_variable("maestro_stack_end"); MC_ignore_global_variable("smx_total_comms"); + MC_ignore_global_variable("communications_pattern"); + MC_ignore_global_variable("initial_communications_pattern"); + MC_ignore_global_variable("incomplete_communications_pattern"); if (MC_is_active()) { MC_ignore_global_variable("mc_diff_info"); @@ -508,13 +513,12 @@ void MC_replay(xbt_fifo_t stack, int start) { int raw_mem = (mmalloc_get_current_heap() == mc_heap); - int value, i = 1, count = 1; + int value, i = 1, count = 1, call = 0, j; char *req_str; smx_simcall_t req = NULL, saved_req = NULL; xbt_fifo_item_t item, start_item; mc_state_t state; smx_process_t process = NULL; - int comm_pattern = 0; smx_action_t current_comm; XBT_DEBUG("**** Begin Replay ****"); @@ -537,7 +541,7 @@ void MC_replay(xbt_fifo_t stack, int start) MC_SET_MC_HEAP; - if ((mc_reduce_kind == e_mc_reduce_dpor) && !_sg_mc_comms_determinism && !_sg_mc_send_determinism) { + if (mc_reduce_kind == e_mc_reduce_dpor) { xbt_dict_reset(first_enabled_state); xbt_swag_foreach(process, simix_global->process_list) { if (MC_process_is_enabled(process)) { @@ -550,8 +554,12 @@ void MC_replay(xbt_fifo_t stack, int start) } if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { - xbt_dynar_reset(communications_pattern); - xbt_dynar_reset(incomplete_communications_pattern); + for (j=0; jissuer->pid); - xbt_dict_remove(first_enabled_state, key); + if(xbt_dict_get_or_null(first_enabled_state, key)) + xbt_dict_remove(first_enabled_state, key); xbt_free(key); MC_SET_STD_HEAP; } @@ -588,36 +597,34 @@ void MC_replay(xbt_fifo_t stack, int start) /* TODO : handle test and testany simcalls */ if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { if (req->call == SIMCALL_COMM_ISEND) - comm_pattern = 1; + call = 1; else if (req->call == SIMCALL_COMM_IRECV) - comm_pattern = 2; + call = 2; else if (req->call == SIMCALL_COMM_WAIT) - comm_pattern = 3; + call = 3; else if (req->call == SIMCALL_COMM_WAITANY) - comm_pattern = 4; + call = 4; } SIMIX_simcall_pre(req, value); if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { MC_SET_MC_HEAP; - if (comm_pattern == 1 || comm_pattern == 2) { - get_comm_pattern(communications_pattern, req, comm_pattern); - } else if (comm_pattern == 3 /* || comm_pattern == 4 */ ) { + if (call == 1) { /* Send */ + get_comm_pattern(communications_pattern, req, call); + } else if (call == 2) { /* Recv */ + get_comm_pattern(communications_pattern, req, call); + } else if (call == 3) { /* Wait */ current_comm = simcall_comm_wait__get__comm(req); - if (current_comm->comm.refcount == 1) { /* First wait only must be considered */ + if (current_comm->comm.refcount == 1) /* First wait only must be considered */ complete_comm_pattern(communications_pattern, current_comm); - } - } else if (comm_pattern == 4 /* || comm_pattern == 4 */ ) { - current_comm = - xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, - smx_action_t); - if (current_comm->comm.refcount == 1) { /* First wait only must be considered */ + } else if (call == 4) { /* WaitAny */ + current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t); + if (current_comm->comm.refcount == 1) /* First wait only must be considered */ complete_comm_pattern(communications_pattern, current_comm); - } } MC_SET_STD_HEAP; - comm_pattern = 0; + call = 0; } @@ -625,7 +632,7 @@ void MC_replay(xbt_fifo_t stack, int start) count++; - if ((mc_reduce_kind == e_mc_reduce_dpor) && !_sg_mc_comms_determinism && !_sg_mc_send_determinism) { + if (mc_reduce_kind == e_mc_reduce_dpor) { MC_SET_MC_HEAP; /* Insert in dict all enabled processes */ xbt_swag_foreach(process, simix_global->process_list) { @@ -893,6 +900,8 @@ void MC_dump_stack_liveness(xbt_fifo_t stack) void MC_print_statistics(mc_stats_t stats) { + xbt_mheap_t previous_heap = mmalloc_get_current_heap(); + if (stats->expanded_pairs == 0) { XBT_INFO("Expanded states = %lu", stats->expanded_states); XBT_INFO("Visited states = %lu", stats->visited_states); @@ -914,7 +923,7 @@ void MC_print_statistics(mc_stats_t stats) XBT_INFO("Send-deterministic : %s", !initial_global_state->send_deterministic ? "No" : "Yes"); } - MC_SET_STD_HEAP; + mmalloc_set_current_heap(previous_heap); } void MC_assert(int prop)